SPIN语义引擎执行方式研究  

Research on Execution Patterns of SPIN Semantics Engine

作　　者：黎升洪[1] 冯艳清[1] 

机构地区：[1]江西财经大学信息管理学院,江西南昌330013

出　　处：《计算机与现代化》2009年第11期112-115,共4页Computer and Modernization

基　　金：国家自然科学基金资助项目(60673115)

摘　　要：模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。本文从语义角度研究PROMELA语义引擎问题,首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述PROMELA指称语义。最后针对SPIN中atomic序列和同步通信等复杂问题给出解决方法。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 de- notational semantics of PROMELA are described by the mapping between syntax of PROMELA and the model, and discusses the specific issues such as atomic sequence, rendezvous channel, and their solutions. Finally a case study demonstrates PROMELA working principle.

关 键 词：模型检查 SPIN PROMELA 语义 

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