| PROMELA语义引擎执行研究 |
| |
| 作者单位： | 江西财经大学信息管理学院 |
| |
| 摘 要： | 模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。该文从语义角度研究了PROMELA语义引擎问题。首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述了PROMELA指称语义。
|
| 关 键 词： | 模型检查 SPIN PROMELA 语义 |
Research on execution patterns of SPIN Semantics Engine |
| |
| Authors: | FENG Yan-qing |
| |
| Abstract: | The PROMELA language, whose commitment manners decide system executions, plays crucial role in model checking tool SPIN. This paper studies semantic engines of PROMELA. Firstly, a formal model of PROMELA is given. Secondly, the denotational semantics of PROMELA are described by the mapping between syntax of PROMELA and the model. We discuss the specific issues such as atomic sequence, rendezvous channel, and their solutions. Finally a case study demonstrates PROMELA working principle. |
| |
| Keywords: | model checking SPIN PROMELA semantics |
| 本文献已被 CNKI 等数据库收录！ |
|
