Property-based support for verification and validation - EV2
Final Report Abstract
Before IC production, substantial effort is spent for its verification, as functionally erroneous hardware cannot be fixed after production. In contrast, Programmable Logic Controllers (PLCs), as used in industrial control systems, are field-reprogrammable as often as needed to fix any problems. However, this leads to the situation that verification of these systems is neglected, which is potentially dangerous for safety-critical systems. This is were this project EV² starts. Based on a specification, which must be present in formal form, test cases are auto-generated in order to test an existing system in field regarding any erroneous functional behaviour. Each formal property describes one (test) aspect of the whole system. Multiple properties can be concatenated, expressing sequential behaviour, or might be overlapping, resulting in parallelity in the system. The formal properties are now analysed regarding temporal overlap, which is used to build an abstract automaton, consisting of states and transitions. The formal specification is then used to generate multiple test cases for each automaton state, covering multiple scenarios of the input signals. Finally, an optimal path through all states is determined, which visits all test cases. At the same time, stimulation patterns are generated, which will force the system under test into the desired concrete state at all times. This pattern is applied to the existing, real system and its response is recorded. Furthermore, a Golden Model is created, which reacts to all test cases in the desired way. If the output of the Golden Model matches the recorded data of the system under test, the whole test can be treated as successful. If the test was successful, we can make the statement that the system under test returned correct results for at least one test case of every formal property. This method is not related to formal verification, however, it contributes to Constrained Random Verification by using formal methods for test case generation.
Publications
-
A Verification Approach for Programmable Logic Controllers. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV) 2020, 19. bis 20. März 2020, Stuttgart.
Elfatih, Braah; Sauppe, Matthias & Heinkel, Ulrich
-
Closed-Loop Approach on Formal Specification for Semiconductor Test, MikroSystemTechnik Congress 2021, 8.-10. Nov. 2021, Stuttgart-Ludwigsburg.
Schott, Christian; Mayer, Franziska; Billich, Enrico; Yazdani, Saeid; Sauppe, Matthias; Wolz, Werner & Heinkel, Ulrich
