摘要
针对谓词/变迁网缺乏有效的形式化验证分析技术,基于代数规约测试谓词/变迁网方法,给出谓词/变迁网转换成代数规约语言CASOCC-WS表示的基调的规则,提出基于测试充分性准则深度优先遍历谓词/变迁网生成变迁触发序列的算法和由变迁触发序列构造公理等式的启发式规则.案例研究表明:该方法可以有效地解决测试Pr/T网时自动生成测试用例和自动判定测试结果和可行路径的问题.
Aim to the problem of being not valid formal means to verify the Predicate/Transition net, the roles are given for translating Predicate/Transition net into signature defined by an algebraic specification CASOCC-WS based on presented method for testing Ptedicate/Transition net based on algebraic specification. Then, the algorithm is presented for deriving the transition fired sequences from Predicate/Transition net according to the test adequacy criterion, and the heuristic rules are defined for constructing axiom equations based on the derived sequences. The case study shows that the method is valid for generating test data automatically and solving the problems to determine the test output and feasible path when testing Predicate/Transition net.
出处
《小型微型计算机系统》
CSCD
北大核心
2011年第9期1804-1809,共6页
Journal of Chinese Computer Systems
基金
国家"九七三"重点基础研究发展计划项目(2005CB321802)资助
湖南省教育厅高校教学改革项目(2010-495)资助
关键词
代数规约
可行路径
谓词/变迁网
变迁触发序列
测试充分性准则
algebraic specification
feasible path
predicate/transition net
transition fired sequence
test adequacy criterion
