参数化系统二维抽象的理论基础  

Two-dimension Abstraction Theory for Parameterized System

作　　者：庞征斌[1] 屈婉霞[1] 郭阳[1] 杨晓东[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机科学》2011年第4期295-298,共4页Computer Science

基　　金：国家自然科学基金项目(60773025;61070036)资助

摘　　要：模型之间的等价关系和抽象模型的性质保持是保证验证正确的必要条件,参数化系统二维抽象从构成系统状态空间的二维方向分别进行抽象,证明了此抽象方法的正确性和合理性,即TDA模型与原始模型存在模拟关系,而且在TDA模型中成立的只对单个变量进行全称量化的单索引ACTL*公式,在任意规模的原始模型中也成立,为简化参数化系统验证提供了理论依据。In order to preserve interesting properties of a system under consideration during verification,it is necessary to establish an equivalent relation between models.Two-dimension Abstraction for parameterized system,where the size of the state transition graph for individual process is decreased independently at first,and the whole system composed of reduced processes is then Abstracted based on the design principle of parameterized systems,thus avoiding the construction of the complete state space that might be too big to fit into memory.The paper gave the correctness and soundness proofs of two-dimension Abstraction.It was shown that simulation relation exists between TDA mo-del and concrete model,and TDA model is weak preserved with respect to ACTL＊ formula.Importantly,a single-indexed ACTL＊ formula satisfied by TDA model,is also satisfied by concrete models with arbitrary replicated（and a constant number of non-replicated） processes.This work lays the theoretical basis for simplifying parameterized system verification.

关 键 词：参数化系统验证 二维抽象 模拟 性质保持 

分 类 号：TP391.72[自动化与计算机技术—计算机应用技术]