LINUX进程间通信的模型检测  

Model Checking for LINUX Interprocess Communication

作　　者：姜玉蓉[1] 缪力[1] 张大方[1,2] 刘潇潇[1] 

机构地区：[1]湖南大学软件学院,长沙410082 [2]湖南大学计算机与通信学院,长沙410082

出　　处：《计算机科学》2008年第10期295-299,共5页Computer Science

基　　金：国家自然科学基金项目(60673155;60703097);国防基础科研"十一五"项目资助(A1420060162)

摘　　要：模型检测是一种强大的自动分析验证技术。分析了LINUX进程间通信的部分源代码并进行手工形式化建模,使用有限状态自动机描述模型,继而转换成SPIN的输入语言PROMELA,对其进行模型检测,验证了系统的有界性和可终止性,并就进程间通信中容易发生的问题提出了改进方案。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.

关 键 词：模型检测 LINUX 进程间通信 SPIN 系统验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论] TP316.81[自动化与计算机技术—计算机科学与技术]