Statechart描述的测试语义和测试用例自动生成

Testing Semantics and Automatic Test Cases Generation for Statechart Specification

研究了Statechart描述的测试语义和测试用例自动生成.基于Tretmans的从标记转换系统描述自动生成测试用例的方法,我们研究如何从Statechart描述自动生成测试用例.建立了基于Statechart描述的一致性测试和测试用例生成的形式化基础.为Statechart描述建立了形式化测试语义,测试语义和传统的验证语义不同,强调可观察性和内部细节隐藏.基于形式化测试语义和测试假设,形式化定义了系统描述和系统实现之间的一致性关系/实现关系.然后给出了基于图遍历的测试用例生成算法,对于无环测试语义该算法可以生成完全测试集,而对于带环测试语义该算法可以生成高效率的宽泛测试集.

Applying Tretmans approach to generate test cases for I/O automata from labeled transition systems,we provide a solid mathematical basis for conformance testing and automatic test case generation for Statechart specification.We introduce formal testing semantics of Statechart specification that go beyond semantics presented for formal verification.These observable testing semantics can be used for general application,critical application and real-time application.We also propose a formal conformance testing relation based on presented formal semantics and test hypothesis and provide an algorithm which,for a Statechart specification,generates a test suite.For finite-runs semantics the algorithm can generate a complete test suite,and for infinite-runs semantics only sound test suite can be generated.