  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.
