| LINUX进程间通信的模型检测 |
| |
| 引用本文： | 姜玉蓉,缪力,张大方,刘潇潇.LINUX进程间通信的模型检测[J].计算机科学,2008,35(10):295-299. |
| |
| 作者姓名： | 姜玉蓉 缪力 张大方 刘潇潇 |
| |
| 作者单位： | 1. 湖南大学计算机与通信学院,长沙,410082
2. 湖南大学软件学院,长沙,410082;湖南大学计算机与通信学院,长沙410082 |
| |
| 基金项目： | 国家自然科学基金，国防科技应用基础研究基金 |
| |
| 摘 要： | 模型检测是一种强大的自动分析验证技术.分析了LINUX进程间通信的部分源代码并进行手工形式化建模,使用有限状态自动机描述模型,继而转换成SPIN的输入语言PROMELA,对其进行模型检测,验证了系统的有界性和可终止性,并就进程间通信中容易发生的问题提出了改进方案.
|
| 关 键 词： | 模型检测 进程间通信 系统验证 |
Model Checking for LINUX Interprocess Communication |
| |
| JIANG Yu-rong,MIAO Li,ZHANG Da-fang,LIU Xiao-xiao.Model Checking for LINUX Interprocess Communication[J].Computer Science,2008,35(10):295-299. |
| |
| Authors: | JIANG Yu-rong MIAO Li ZHANG Da-fang LIU Xiao-xiao |
| |
| Affiliation: | JIANG Yu-rong1 MIAO Li1 ZHANG Da-fang1,2 LIU Xiao-xiao1(Department of Software Engineering,Hunan University,Changsha 410082,China)1(Department of Computer , Communication,China)2 |
| |
| Abstract: | Model checking is a powerful technique to analyse and verify system automatically.Part of the source code of Linux interprocess communication was chosen to be analysed and formalized modeled,then these models were translated into PROMELA,the input language to SPIN,to be model checked.Boundedness and terminability were verified and an improved method to the problem in interprocess communication was worked out. |
| |
| Keywords: | LINUX SPIN |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
