CPOT-SM – Complete Property-oriented Testing with Symbolic Methods

• Applicant: Professor Dr. Jan Peleska
• Subject Area: Software Engineering and Programming Languages ; Security and Dependability, Operating-, Communication- and Distributed Systems ; Theoretical Computer Science
• Term: from 2019 to 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 407708394

Complete testing methods provide test suite generation techniques with guaranteed fault coverage under certain hypotheses about the system under test (SUT). While they have always been considered as an interesting research field, their practical applicability has often been questioned, due to the unmanageable test suite sizes to be applied when wishing to achieve full fault coverage under realistic hypotheses. This situation has changed during the last years, since it could be shown that equivalence class partition techniques could be applied to industrial-size SUTs.In this project, we plan to exploit these recent results in the context of property-oriented testing (POT). In contrast to general model-based testing (MBT), POT focuses on the thorough test of single SUT requirements only. As a consequence, POT does not require complete models describing the expected behavior of the SUT but can be based on (1) specifications stated in temporal logics, (2) partial models, or (3) abstracted models. Therefore, the costs for enabling SUT verification by POT are usually lower than the costs for a full MBT approach. On the downside, there is currently no comprehensive theory of completeness for testing against properties. It is therefore a main objective of this project to elaborate new approaches to POT allowing to generate test suites with guaranteed fault coverage. This will be achieved by means of a mixed approach involving both models and temporal logics specifications. To cope with the state space complexity of the models, symbolic methods will be applied, where concrete inputs, outputs, and SUT states are replaced by first-order formulas identifying input, output, and state classes. As an additional challenge, we will investigate POT in the context of autonomous systems. Since POT has close links to MBT, a supporting work package will focus on complete model-based testing theories for systems with infinite domains for inputs, internal states, and outputs. A further work package will investigate the problem of configurable systems as in product line testing and extend the existing equivalence class theory to configuration parameters. The CPOT-SM research results will be implemented as an experimental prototype in an existing industrial-strength MBT tool. The elaborated methods will be validated in this tool framework in case studies to be conducted with international research partners. The case studies cover the fields avionics, railways, autonomous vehicles, and robotics.

• DFG Programme: Research Grants