Promela行为模型的自动抽象

摘要：

提出并实现了一个自动抽象算法,可从详细系统的Promela行为模型中导出抽象系统的行为模型.抽象模型与原模型迹等价,且具有状态变量最少、状态空间最小的特点.它可代替详细模型用作环境模型或参与全局性质检查,减小模型检查的状态空间以提高验证效率.

关键词：抽象算法、行为分析、Promela

所属期刊栏目：30

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金60173103

在线出版日期：2004-09-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：7-8,44