Modeling of Time-Dependent Behavior in Fault-Tolerant Systems

Abstract

Ensuring the correct operation of safety-critical systems often relies on model-driven engineering at design time and fault-tolerant solutions at operation time. Modeling and analyzing fault-tolerant systems is a challenging task: designing the complex control is tedious and we also need special modeling constructs to be able to represent the many aspects of operation. On the other hand, we need efficient algorithms to be able to verify the desired functionalities. In this paper, we extend our former work and develop time-dependent extensions to the modeling approach used in an automotive case study. Based on our case study, we evaluate the applicability of various model checking algorithms for the verification of systems with timedependent behavior.