SPIN语义引擎执行方式研究

• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 模型检查 SPIN PROMELA 语义
• 年，卷（期）: 2009,（11）
• 所属期刊栏目: 软件设计
• 页码范围: 112-115
• 页数: 4页
• 分类号: TP301
• 字数: 3103字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2009.11.032

摘要

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