# SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems

## TL;DR

This paper presents an SMT-based method for probabilistic analysis of timing constraints in cyber-physical systems, integrating EAST-ADL, SIMULINK/STATEFLOW, and PrCCSL for safety-critical embedded system design.

## Contribution

It introduces an automatic transformation from SIMULINK/STATEFLOW models to SMT formulas for probabilistic timing analysis in EAST-ADL systems, extending prior work with a practical approach.

## Key findings

- Successfully applied to a cooperative automotive system case study.
- Enables formal probabilistic analysis of timing constraints.
- Reduces analysis to SMT validity checking.

## Abstract

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.