Abstract
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.
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.
| Original language | English |
|---|---|
| Publication date | Oct 2018 |
| Publication status | Published - Oct 2018 |
| Event | Formal Methods in Computer-Aided Design - Austin, United States Duration: 30. Oct 2018 → 2. Nov 2018 |
Conference
| Conference | Formal Methods in Computer-Aided Design |
|---|---|
| Country/Territory | United States |
| City | Austin |
| Period | 30/10/2018 → 02/11/2018 |