CPOT-SM – Complete Property-oriented Testing with Symbolic Methods
Security and Dependability, Operating-, Communication- and Distributed Systems
Theoretical Computer Science
Final Report Abstract
The main objective of this project was to provide complete testing methods (these methods provide correctness guarantees for implementations passing the tests) to verify that implementations under test (IuT) fulfil their specified properties (so-called property-oriented testing (POT)). Automating POT and, at the same time, ensuring completeness guarantees is of considerable importance for the verification of safety-critical systems, where the strength of the testing methods applied needs to be justified, and test campaigns with conventional means become unacceptably costly. The complexity problem often limiting the practical applicability of complete test suites has been mitigated in this project by the creation of symbolic system representations based on several novel types of equivalence classes. With the help of these classes, the behavioural model of an IuT can be abstracted to a manageable size, but without losing the capability to uncover all violations of the specified properties. For two complementary POT approaches, novel complete methods have been developed, each of them able to cope with realistic IuT complexity, as found in airbag controllers, speed monitors, or train protection systems. The first approach is applicable for developments following the model-based systems and software engineering paradigm, where design models are created in addition to the required properties. The existence of a model that is already known to fulfil the required property allows to ensure property fulfilment with significantly fewer test cases. The second approach is specialised on software module testing and applies machine learning techniques for automated internal model creation and subsequent model checking, so that test engineers only have to specify the required properties. An open source software ecosystem has been created implementing both POT approaches. The test generation and execution software is runnable in a cloud server farm and can be accessed freely for research and evaluation purposes.
Publications
-
New Distribution Paradigms for Railway Interlocking. Lecture Notes in Computer Science, 434-448. Springer International Publishing.
Peleska, Jan
-
Efficient data validation for geographical interlocking systems. Formal Aspects of Computing, 33(6), 925-955.
Peleska, Jan; Krafczyk, Niklas; Haxthausen, Anne E. & Pinger, Ralf
-
Exhaustive Property Oriented Model-Based Testing with Symbolic Finite State Machines. Lecture Notes in Computer Science, 84-102. Springer International Publishing.
Krafczyk, Niklas & Peleska, Jan
-
Effective grey‐box testing with partial FSM models. Software Testing, Verification and Reliability, 32(2).
Sachtleben, Robert & Peleska, Jan
-
libfsmtest An Open Source Library for FSM-Based Testing. Lecture Notes in Computer Science, 3-19. Springer International Publishing.
Bergenthal, Moritz; Krafczyk, Niklas; Peleska, Jan & Sachtleben, Robert
-
Model-Based Conformance Testing and Property Testing With Symbolic Finite State Machines - Technical Report. October 2022
Wen-ling Huang, Niklas Krafczyk & Jan Peleska
-
An Optimised Complete Strategy for Testing Symbolic Finite State Machines. Lecture Notes in Computer Science, 55-71. Springer Nature Switzerland.
Huang, Wen-ling; Krafczyk, Niklas & Peleska, Jan
-
Complete Property-Oriented Module Testing. Lecture Notes in Computer Science, 183-201. Springer Nature Switzerland.
Brüning, Felix; Gleirscher, Mario; Huang, Wen-ling; Krafczyk, Niklas; Peleska, Jan & Sachtleben, Robert
-
Efficient Gray Box Checking for C/C ++ Modules - Technical Report. Publisher: Zenodo, March 2024.
Felix Brüning, Mario Gleirscher, Wen-ling Huang, Krafczyk Niklas, Jan Peleska & Robert Sachtleben
-
Exhaustive property oriented model-based testing with symbolic finite state machines. Science of Computer Programming, 231, 103005.
Huang, Wen-ling; Krafczyk, Niklas & Peleska, Jan
