论文部分内容阅读
模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。该文从语义角度研究了PROMELA语义引擎问题。首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述了PROMELA指称语义。