Promela行为模型的自动抽象  

Automatic Abstraction for Promela Behavioral Model

作　　者：支小莉[1] 陆鑫达[2] 戎璐[2] 

机构地区：[1]上海大学计算机学院,上海200072 [2]上海交通大学电信学院,上海200030

出　　处：《计算机工程》2004年第16期7-8,44,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60173103)

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]