进程调度模型的Spin验证分析与改进  

Verification and improvement of process scheduling model by Spin

作　　者：翁立晨[1] 汪学明[1] 

机构地区：[1]贵州大学计算机学院,贵阳550025

出　　处：《计算机应用》2009年第B12期158-160,共3页journal of Computer Applications

基　　金：贵州省自然科学基金资助项目(20052110);贵州大学引进人才科研项目(2009)

摘　　要：Spin不仅可以用于通信协议的正确性验证,也可以对其进行有效的安全性分析。对用Promela语言描述的进程调度模型进行分析研究,并对其存在的不足加以改进。增加了LTL公式描述,用Spin进行模型检测验证,使用Xspin得到了反例状态迁移轨迹图。Spin can not only be used to verify the correctness of communication protocols, it can also be used for effective safety analysis. A model of process scheduling by using Promela was analyzed. Its deficiencies were improved. Its property was described by using LTL, and the track of the state of counter-examples were obtained by using Spin and Xspin.

关 键 词：模型检测 SPIN Promela语言 LTL 进程调度 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]