| 一种Ada并发程序的模型检测方法 |
| |
| 引用本文： | 黄超,江国华. 一种Ada并发程序的模型检测方法[J]. 电子科技, 2012, 25(3): 44-47 |
| |
| 作者姓名： | 黄超 江国华 |
| |
| 作者单位： | (南京航空航天大学 计算机科学与技术学院,江苏 南京 210016) |
| |
| 摘 要： | 提出了一种针对Ada并发程序的模型提取方法,使用模型检测工具SPIN对生成的模型进行自动化验证,发现Ada语言编写的程序中并发错误。通过实例对提取方法进行验证,实验结果表明,此方法能够成功检测出Ada并发程序中存在的错误,并给出相应的错误路径。
|
| 关 键 词： | 模型检测 Ada 并发程序 模型提取 SPIN |
A Model Checking Method for Ada Concurrent Program |
| |
| HUANG Chao,JIANG Guohua. A Model Checking Method for Ada Concurrent Program[J]. Electronic Science and Technology, 2012, 25(3): 44-47 |
| |
| Authors: | HUANG Chao JIANG Guohua |
| |
| Affiliation: | (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China) |
| |
| 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. |
| |
| Keywords: | model checking Ada concurrent program model extraction SPIN |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《电子科技》浏览原始摘要信息 |
|
点击此处可从《电子科技》下载全文 |
|
