基于SPIN的系统建模研究  

Research on System Modeling Based on SPIN

作　　者：徐小丽[1] 

机构地区：[1]北京航空航天大学计算机学院

出　　处：《计算机与现代化》2012年第9期209-214,共6页Computer and Modernization

摘　　要：模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型,并对实验结果进行分析。Because of the high degree of automation, model checking technology has become one of the most popular way to en- sure correctness in the formal verification field. To use the model checker, the user should model the verification-needed system. This paper summarizes the basic principles of model checking technology and explores the Promela modeling with model checker SPIN. Finally, a simple bus operation prototype model is given, and the experimental results are analyzed.

关 键 词：模型检测 建模 SPIN PROMELA 

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