Abstract: This paper proposes an automatic abstraction algorithm for constructing a trace equivalent abstract model from the detailed Promela model. The abstract model has a minimum of state variables and the smallest state space. It can be used in place of the detailed model when building environmental model or checking global property to improve the efficiency of model checking .

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

关键词: 抽象算法, 行为分析, Promela

CLC Number: 

• TP391.7