一种Ada并发程序的模型检测方法

›› 2012, Vol. 25 ›› Issue (3): 44-.

一种Ada并发程序的模型检测方法

黄超,江国华

(南京航空航天大学计算机科学与技术学院,江苏南京 210016)

出版日期:2012-03-15 发布日期:2012-03-21
作者简介:黄超(1987—),男,硕士研究生。研究方向:软件测试。江国华(1963—),男,副教授,硕士生导师。研究方向:软件工程,软件测试。

A Model Checking Method for Ada Concurrent Program

HUANG Chao, JIANG Guo-Hua

(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

Online:2012-03-15 Published:2012-03-21

摘要/Abstract

摘要：

提出了一种针对Ada并发程序的模型提取方法,使用模型检测工具SPIN对生成的模型进行自动化验证,发现Ada语言编写的程序中并发错误。通过实例对提取方法进行验证,实验结果表明,此方法能够成功检测出Ada并发程序中存在的错误,并给出相应的错误路径。

关键词: 模型检测, Ada, 并发程序, 模型提取, SPIN

Abstract:

A model extraction method for Ada concurrent programs is proposed.The model checker SPIN is used to validate the model generated automatically,and it is found that concurrent errors such as deadlock exist in programs written with Ada language.Finally,the extraction method is verified through examples.The experimental results show that this method can successfully detect errors existing in Ada concurrent programs,and give the corresponding error path.

Key words: model checking;Ada;concurrent program;model extraction;SPIN

中图分类号:

TP311.562

黄超, 江国华. 一种Ada并发程序的模型检测方法[J]. , 2012, 25(3): 44-.

HUANG Chao, JIANG Guo-Hua. A Model Checking Method for Ada Concurrent Program[J]. , 2012, 25(3): 44-.

[1]	宿晓航,王立华,陈佳明. 基于多体动力学与有限元的油缸系统疲劳寿命研究[J]. 电子科技, 2022, 35(1): 40-44.
[2]	陈佳明,王立华,宿晓航. 基于ADAMS的铁路桥梁有砟道床力学特性研究[J]. 电子科技, 2022, 35(1): 53-59.
[3]	朱斌,刘子龙. 基于新型初始模块的卷积神经网络图像分类方法[J]. 电子科技, 2021, 34(2): 52-56.
[4]	杨思燕,苗凯彬,王锋,苗启广. 视频图像中人脸自动检测与统计算法[J]. 电子科技, 2020, 33(8): 1-9.
[5]	王春江,张猛,张建飞. 基于网络摄像头的活体人脸识别系统设计[J]. 电子科技, 2020, 33(6): 63-68.
[6]	陈久朋,伞红军,张道义,胡琼琼,张凯翔,熊彬州. 一种四足机器人对角步态仿真分析[J]. 电子科技, 2020, 33(5): 33-38.
[7]	张道义,伞红军,陈久朋,李鹏飞,熊彬州. 5-DOF混联雕刻机速度运动学分析及仿真[J]. 电子科技, 2020, 33(4): 42-49.
[8]	汪欣,吴薇,曾照. 基于视频的人脸检测算法研究[J]. 电子科技, 2020, 33(2): 25-31.
[9]	田雄,吴薇,刘晓尚,吴秀. 多人脸跟踪与最佳人脸提取[J]. 电子科技, 2019, 32(9): 32-37.
[10]	陈久朋,伞红军,李鹏飞,张道义,熊彬州. 5-DOF并串联机器人运动学分析及仿真[J]. 电子科技, 2019, 32(12): 37-43.
[11]	殷涛,崔佳冬. 视频监控行人流量统计系统的设计[J]. 电子科技, 2019, 32(12): 48-52.
[12]	朱呈祥，沈景凤. 基于Matlab和Adams的超速机柔性轴系仿真[J]. , 2017, 30(4): 98-.
[13]	姜俊剑，杨丽红. 基于ADAMS的X光机俯仰机构设计仿真[J]. , 2017, 30(4): 107-.
[14]	于世强，应捷. 基于Android平台的实时人脸检测与跟踪[J]. , 2016, 29(7): 78-.
[15]	肖儿良,韩超. 应用于人脸自动实时跟踪的改进Struck算法[J]. , 2016, 29(3): 42-.