|
CPOT-SM Complete Property-oriented Testing with Symbolic Methods (2019-10-01 - 2022-09-30)
CPOT-SM
is funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation)
project number 407708394.
Abstract
Complete testing methods provide test suite generation techniques with guaranteed fault coverage under certain hypotheses about the system under test (SUT). Typical hypotheses refer to the assumed number of internal states or the granularity of input equivalence classes required to capture every possible SUT behavior. Complete testing methods are typically investigated and applied in the context of model-based black-box conformance testing. 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: the introduction of equivalence classes significantly reduces the test suite size, while still preserving the suite's completeness. Moreover, it could be shown by means of comprehensive experiments that the test strength of suites constructed by means of these complete methods outperforms that of naive testing approaches, even if the true SUT behavior does not conform to the underlying hypotheses.
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. First results recently achieved with POT based on abstracted models indicate that this approach will be quite effective. 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, where configuration updates and behavioral changes due to evolving requirements or changed environmental conditions are admissible and expected. Since property-oriented testing 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. Both supporting activities are essential for the successful realization of the main objective. 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 at the University of Bremen and with international research partners in the United Kingdom and in Denmark. The case studies cover the fields avionics, railways, autonomous vehicles, and robotics.
Detailed Description
CPOT-SM - Detailed project description
Publications
Initial publications related to CPOT-SM can be found
here.
A detailed project-specific publication list will be published here after
the project has started.
|
|