SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems
This addresses the need for formal verification of timing constraints in safety-critical embedded systems, but it is incremental as it builds on existing PrCCSL and SMT methods.
The paper tackles the problem of analyzing timing constraints in cyber-physical systems by proposing an SMT-based approach that transforms SIMULINK/STATEFLOW models into SMT formulas for probabilistic analysis, demonstrating it on an automotive case study.
Modeling and analysis of timing constraints is crucial in cyber-physical systems (CPS). EAST-ADL is an architectural language dedicated to safety-critical embedded system design. SIMULINK/STATEFLOW (S/S) is a widely used industrial tool for modeling and analysis of embedded systems. In most cases, a bounded number of violations of timing constraints in systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). We have previously defined a probabilistic extension of Clock Constraint Specification Language (CCSL), called PrCCSL, for formal specification of EAST-ADL timing constraints in the context of WH. In this paper, we propose an SMT-based approach for probabilistic analysis of EAST-ADL timing constraints in CPS modeled in S/S: an automatic transformation from S/S models to the input language of SMT solver is provided; timing constraints specified in PrCCSL are encoded into SMT formulas and the probabilistic analysis of timing constraints is reduced to the validity checking of the resulting SMT encodings. Our approach is demonstrated a cooperative automotive system case study.