Falsification of Signal-Based Specifications for Cyber-Physical Systems

Sammanfattning: In the development of software for modern Cyber-Physical Systems, testing is an integral part that is rightfully given a lot of attention. Testing is done on many different abstraction levels, and especially for large-scale industrial systems, it can be difficult to know when the testing should conclude and the software can be considered correct enough for making its way into production. This thesis proposes new methods for analyzing and generating test cases as a means of being more certain that proper testing has been performed for the system under test. For analysis, the proposed approach includes automatically finding how much a given test suite has executed the physical properties of the simulated system. For test case generation, an up-and-coming approach to find errors in Cyber-Physical Systems is simulation-based falsification. While falsification is suitable also for some large-scale industrial systems, sometimes there is a gap between what has been researched and what problems need to be solved to make the approach tractable in the industry. This thesis attempts to close this gap by applying falsification techniques to real-world models from Volvo Car Corporation, and adapting the falsification procedure where it has shortcomings for certain classes of systems. Specifically, the thesis includes a method for automatically transforming a signal-based specification into a formal specification in temporal logic, as well as a modification to the underlying optimization problem that makes falsification more viable in an industrial setting. The proposed methods have been evaluated for both academic benchmark examples and real-world industrial models. One of the main conclusions is that the proposed additions and changes to analysis and generation of tests can be useful, given that one has enough information about the system under test. It is difficult to provide a general solution that will always work best -- instead, the challenge lies in identifying which properties of the given system should be taken into account when trying to find potential errors in the system.