Approaches to cyber-physical (model) model-checking

Abstract

Formal verification of complex systems like cyber-physical systems (CPS) is a major challenge. The reason is, among other things, state space explosion, i.e., the phenomenon that the number of possible states is exponential to the number of variables used to specify the system for the purpose of verification through model-checking. In addition to software models to be verified, for CPS verification models of the physical environment have to be included as well, but they are significantly different from software models. This entails further problems with CPS verification through model-checking. Hence, the main challenge addressed in this thesis has been the creation of cyber-physical models for model-checking. In particular, it was challenging to provide models that contain all the necessary information for proving or disproving a given property and still have a reasonable size for efficient verification. More specifically, this thesis dealt with three research questions that are all related to this challenge. However, each of them emphasizes a different aspect and was dealt with in a different domain. The first research question asks whether and how formal verification may help to improve models in a top-down design process of CPS. During the design of a CPS, often the challenge arises of verifying a system model against certain properties. In an early design stage, however, the system model may not include sufficient detail. The physical environment is often described initially by formulas, like Newton’s law. In this thesis, a top-down design approach is proposed and evaluated (in the automotive domain) that starts with an abstract (qualitative) model of the system – including the physical parts – and refines it systematically while including both verification and validation. The second research question asks how to formally check consistency between process-oriented models and models of the environment as early as possible in the course of CPS development. This thesis presents an approach to verifying consistency between UML Activity diagrams modeling processes, object life cycles modeling the environment, and context-dependent semantic action specifications. It is evaluated in the domain of charging electric vehicles. The third research question asks how the runtime efficiency of the formal verification of certain robot applications using structural abstractions based on a voxel representation can be improved. Due to the complexity of robot applications and their complex work environment modeled as a voxel grid, the formal verification of such applications is usually time-consuming. This thesis presents and evaluates an approach that uses selective refinement of structural abstractions to improve the runtime efficiency of model-checking. Summarizing, this thesis addresses certain limitations of model-checking CPS models and proposes new approaches for improvements especially with regard to models of the environment.