Formal Analysis of Hybrid-Dynamic Timing Behaviors in Cyber-Physical Systems

TL;DR

This paper introduces an SMT-based formal verification method for analyzing hybrid-dynamic timing behaviors in cyber-physical systems modeled with Simulink and Stateflow, demonstrated on an unmanned surface vessel.

Contribution

It presents a novel translation algorithm that converts hierarchical Stateflow models into SMT encodings for formal timing verification.

Findings

Successfully verified timing constraints in a case study

Effective translation of Stateflow models into SMT formulas

Demonstrated applicability on an unmanned surface vessel

Abstract

Ensuring correctness of timed behaviors in cyber-physical systems (CPS) using closed-loop verification is challenging due to the hybrid dynamics in both systems and environments. Simulink and Stateflow are tools for model-based design that support a variety of mechanisms for modeling and analyzing hybrid dynamics of real-time embedded systems. In this paper, we present an SMT-based approach for formal analysis of the hybrid-dynamic timing behaviors of CPS modeled in Simulink blocks and Stateflow states (S/S). The hierarchically interconnected S/S are flattened and translated into the input language of SMT solver for formal verification. A translation algorithm is provided to facilitate the translation. Formal verification of timing constraints against the S/S models is reduced to the validity checking of the resulting SMT encodings. The applicability of our approach is demonstrated on an unmanned surface vessel case study.