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

Formal analysis of timing constraints is crucial
in safety-critical cyber-physical systems (CPS). EAST-ADL is
an architectural language dedicated to safety-critical embedded
system design. SIMULINK/STATEFLOW (S/S) is an industrial tool
widely used for modeling and analysis of CPS. In most cases, a
bounded number of violations of timing constraints in CPS would
not lead to system failures when the results of the violations are
negligible, called Weakly-Hard (WH). In the context of WH,
this paper presents an SMT-based approach to support formal
probabilistic analysis of timing constraints in CPS modeled in
EAST-ADL and S/S. Our approach is demonstrated on two
automotive systems case studies.