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