↓Skip to main content

A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica

Verification Fiacre Safety
Table of Contents

Alexandre Albore, Silvano Dal Zilio, Guillaume Infantes, Christel Seguin, Pierre Virelizier
In IMBSA 2017 — 18th International Conference on Formal Engineering Methods, sep 2017.

conference paper

 PDF  DOI〈10.1007/978-3-319-64119-5_10〉  HAL-01693391

Abstract
#

The design of complex safety critical systems raises new technical challenges for the industry. As systems become more complex—and include more and more interacting functions—it becomes harder to evaluate the safety implications of local failures and their possible propagation through a whole system. That is all the more true when we add time to the problem, that is when we consider the impact of computation times and delays on the propagation of failures. We describe an approach that extends models developed for Safety Analysis with timing information and provide tools to reason on the correctness of temporal safety conditions. Our approach is based on an extension of the AltaRica language where we can associate timing constraints with events and relies on a translation into a realtime model-checking toolset. We illustrate our method with an example that is representative of safety architectures found in critical systems.

Citation
#


@InProceedings{DalzilioS:imbsa2017altarica,
   author    = {Albore, Alexandre and {Dal Zilio}, Silvano and Infantes, Guillaume and Seguin, Christel and Virelizier, Pierre},
   title     = {{A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica}},
   booktitle = {IMBSA 2017 -- 18th International Conference on Formal Engineering Methods},
   series    = {Lecture Notes in Computer Science},
   volume    = {10437},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-319-64119-5_10},
   pages     = {147--162},
   month     = sep, 
   year      = 2017
}