空间完备性理论及其测试  

Theory of Space Completion and Its Test

作　　者：高晓雷[1] 缪淮扣[2] 

机构地区：[1]东莞理工学院计算机学院,东莞523808 [2]上海大学计算机工程与科学学院,上海201800

出　　处：《计算机工程》2009年第9期72-73,76,共3页Computer Engineering

基　　金：广东省自然科学基金资助项目"基于Z规格说明的软件测试自动化方法研究"(06301204)

摘　　要：证明和测试是验证规格说明是否正确的2种方法,两者互为补充。针对软件规格说明难以证明的问题,提出对状态空间进行完备性测试的理论。采用构造函数和受限状态空间的概念,讨论用于测试Z规格说明语言初始状态存在性的方法,通过实例证明该方法的可行性。Proof and test are two ways to check specification, and they are complementary. Aiming at the problem that specification is difficult to be proofed, this paper proposes the theory of completeness test of states space. The concepts of constructed function and constrained states space are used. The test approach used to detect the existing of initial state in Z specifications language is discussed, and the feasibility of this approach is proved by application example.

关 键 词：Z规格说明 受限状态空间 初始状态 不变式 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]