面向测试和模型检测需求的程序建模技术研究  

Procedures modeling for testing and model checking needs

作　　者：孙晶[1] 张学娜[1] 

机构地区：[1]北方工业大学计算机学院,北京100144

出　　处：《计算机应用研究》2015年第9期2693-2696,2701,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(61070030;61370051);北京市教委学术创新团队项目(4062012)

摘　　要：由于同时支持软件测试和模型检测需求的程序建模比较少,为此提出了一种程序建模技术,该技术主要包括物理存储模型、可视化模型和代数模型。利用程序流图的思想建立物理存储模型和可视化模型,并通过建立在严格数学基础上的代数模型验证可视化模型的正确性。实验结果表明,建立的程序模型为后续的模型检测工作提供了基本路径等可用信息,在一定程度上抑制了模型检测状态空间爆炸的问题。同时为后续的TTCN-3抽象测试套的自动生成提供了基本路径、数据类型等信息。该程序模型为最终实现建模与检测自动一体化,提高效率奠定了基础。Because of relatively few modeling support software testing and model checking needs, for the demand of testing and model checking procedures proposed a modeling technique that included physical storage model, visual model and algebra- ic model. Using the idea of the establishment of a program flow graph to create physical storage model and visual model, and verified the correctness of the visual model by algebra model which based on establishing rigorous mathematics. Program model provided basic path information available for subsequent model testing work, suppressed model checking the state space explo- sion problem to some extent. Meanwhile, for TTCN-3 automatic generation of abstract test suite provided the basic path, data type and other information. Modeling systems improve the efficiency of the model checking and testing automatic integration.

关 键 词：模型检测 软件测试 模型代数 程序建模 程序流图 

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