面向UML的形式化测试技术

The project has investigated formal techniques for automated testing and model.checking. The main contributions include, the operational semantics for UML.Statecharts, which serves as a common model of object dynamic behaviors for.both of verification and testing; the test case generation method for UML.Statecharts according to its hierarchy and concurrency; the approach of model.checking UML Statecharts associated with the state space reduction methods.based on slicing; and the improved method for path-wise automatic generation of.test data. Based on the above results, the prototype tool and system have been.designed and implemented for experiments. The achievements of the project are.expected to promote the combination of automated testing and model checking.for system validation, which is essential in the development of safety critical.systems.

基于形式化验证技术，研究面向UML的软件自动测试技术，包括：UML的形式化语义；测试Oracle的自动生成；测试用例的自动生成；以及相应的测试自动化工具。研究将推进软件测试技术在依托程序理论的基础上走向系统化、自动化，对于保障和提高软件可靠性有重要的科学意义和广泛的应用价值。