Verification of design models of cyber-physical systems specified in Simulink

Recent advances in cyber-physical systems (CPS) have allowed highly available and approachable technologies with interconnected systems between the physical assets and the computational software components. This has resulted in more complex systems with wider capabilities. For example, they can be applied in various domains such as safe transport, efficient medical devices, integrated systems, critical infrastructure control and more. The development of such critical systems requires advanced new models, algorithms, methods and tools to verify and validate the software components and the entire system. The verification of cyber-physical systems has become challenging: (1) The complex and dynamical behaviour of systems requires resilient automated monitors and test oracles that can cope with time-varying variables of CPS. (2) Given the wide range of existing verification and testing techniques from formal to empirical methods, there is no clear guidance as to how different techniques fare in the context of CPS. (3) Due to serious issues when applying exhaustive verification to complex systems, a common practice is
needed to verify system components separately. This requires adding implicit assumptions about the operational environment of system components to ensure correct verification. However, identifying environment assumptions for cyber-physical systems with complex, mathematical behaviors is not trivial. In this dissertation, we focus on addressing these challenges. In this dissertation, we propose a set of effective approaches to verify design models of CPS. The work presented in this dissertation is motivated by ESAIL maritime micro-satellite system, developed by LuxSpace, a leading provider of space systems, applications and services in Luxembourg. In addition to ESAIL, we use a benchmark of eleven public-domain Simulink models provided by Lockheed Martin, which are representative of different categories of CPS models in the aerospace and defence sector. To address the aforementioned challenges, we propose (1) an automated approach to translate CPS requirements specified in a logic-based language into test oracles specified in Simulink. The generated oracles are able to deal with CPS
complex behaviours and interactions with the system environment; (2) An empirical study to evaluate the fault-finding capabilities of model testing and model checking techniques for Simulink models. We also provide a categorization of model types and a set of common logical patterns for CPS requirements; (3) An automated approach to synthesize environment assumptions for a component under analysis by combining search-based testing, machine learning and model checking procedures. We also propose a novel technique to guide the test generation based on the feedback received from the machine learning process; and (4) An extension of (3) to learn more complex assumptions with arithmetic expressions over multiple signals and numerical variables.