A Model-Based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems

1. Introduction

In safety critical domains like aviation, automotive and robotics, autonomous cyber-physical systems interact with each other in the same physical space. To avoid damage and injuries, the control software of the systems has to guarantee spatiotemporal properties like collision avoidance or the cooperation of several units that carry a heavy workpiece together. A popular way for the creation of functionally correct and safe system software is the application of integrated modeling and verification tools like MATLAB/Simulink (Tyagi, 2012). Our contribution is the combination of such a tool with efficient provers allowing to verify that the coordinated behavior of multiple controlled cyber-physical systems fulfills relevant spatial safety properties. We introduce a toolchain combining the model-based engineering tool-set Reactive Blocks¹ (Kraemer, Slåtten, & Herrmann, 2009) with the verification tool BeSpaceD (Blech & Schmidt, 2013). In particular, we use a development workflow starting with the collection of requirements for a cyber-physical system and its architecture followed by the steps listed below:

• 1.

  Spatiotemporal properties of components are described in the input language of BeSpaceD;

• 2.

  A model of the system controller is created in Reactive Blocks. We compose it with a simulator model of the continuous system parts which is created using the BeSpaceD model developed in step 1;

• 3.

  The built-in model checker of Reactive Blocks is used to check the combined controller and simulator model for general design errors (Kraemer, Slåtten, & Herrmann, 2009);

• 4.

  If the checks in step 3 are passed, the software model is transformed to the input language of BeSpaceD;

• 5.

  Assuming certain maximum reaction times of the discrete controller, it is verified with BeSpaceD that the model resulting from the transformation in step 3 fulfills the spatiotemporal properties defined in step 1;

• 6.

  The model checker UPPAAL (Bengtsson, et al., 1996) is applied to prove that the real-time properties assumed in the proofs of step 5 are indeed kept by the Reactive Blocks model created in step 2 (Han & Herrmann, 2013), (Han, Herrmann, & Le, 2013);

• 7.

  By using the code generator from Reactive Blocks (Kraemer & Herrmann, 2007), (Kraemer, Herrmann, & Bræk, 2006) executable Java code of the controller and, if desired, of the simulator of the continuous behavior is created. The generated code can be deployed on the system components running the control software of the embedded system.

Figure 1.

Layout of the moving robot

Our approach has to guarantee that a model developed with Reactive Blocks indeed fulfills the desired safety properties if the verifications in steps 5 and 6 succeed. Formally, that proof is merely trivial: Be S the logical formula corresponding to a system model in Reactive Blocks according to (Kraemer & Herrmann, 2010), P the conjoined spatial behavioral properties to be fulfilled by S, and R(t) a statement describing that the controller always guarantees a maximum reaction time t. Using BeSpaceD, we verify in step 5 that the system fulfills the safety properties if t is kept, i.e., S ∧ R(t) ⇒ P. In step 6, we prove with UPPAAL that the system guarantees the maximum reaction time, i.e., S ⇒ R(t). It is evident that the combination of the two proofs implies S ⇒ P such that the Reactive Blocks model created in step 2 effectively fulfills the spatial properties defined in step 1.