On Falsification of Large-Scale Cyber-Physical Systems

Sammanfattning: In the development of modern Cyber-Physical Systems, Model-Based Testing of the closed-loop system is an approach for finding potential faults and increasing quality of developed products. Testing is done on many different abstraction levels, and for large-scale industrial systems, there are several challenges. Executing tests on the systems can be time-consuming and large numbers of complex specifications need to be thoroughly tested, while many of the popular academic benchmarks do not necessarily reflect on this complexity. This thesis proposes new methods for analyzing and generating test cases as a means for being more certain that proper testing has been performed on the system under test. For analysis, the proposed approach can automatically find out how much of the physical parts of the system that the test suite has executed. For test case generation, an approach to find errors is optimization-based falsification. This thesis attempts to close the gap between academia and industry 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 main contributions of this thesis are (i) a method for automatically transforming a signal-based specification into a formal specification allowing an optimization-based falsification approach, (ii) a new collection of specifications inspired by large-scale specifications from industry, (iii) an algorithm to perform optimization-based falsification for such a large set of specifications, and (iv) a new type of coverage criterion for Cyber-Physical Systems that can help to assess when testing can be concluded. 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 the analysis and generation of tests can be useful, given that one has enough information about the system under test. The methods presented in this thesis have been applied to realworld models in a way that allows for higher-quality products by finding more faults in early phases of development.