| 基于SPIN的系统建模研究 |
| |
| 引用本文： | 徐小丽.基于SPIN的系统建模研究[J].计算机与现代化,2012(9):209-214. |
| |
| 作者姓名： | 徐小丽 |
| |
| 作者单位： | 北京航空航天大学计算机学院,北京100191 |
| |
| 摘 要： | 模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型,并对实验结果进行分析。
|
| 关 键 词： | 模型检测 建模 SPIN Promela |
Research on System Modeling Based on SPIN |
| |
| XU Xiao-li.Research on System Modeling Based on SPIN[J].Computer and Modernization,2012(9):209-214. |
| |
| Authors: | XU Xiao-li |
| |
| Affiliation: | XU Xiao-li (School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China) |
| |
| Abstract: | 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. |
| |
| Keywords: | model checking modeling SPIN Promela |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
