Ali Ebnenasir
July, 2007
To facilitate incremental modeling and analysis of fault-tolerant embedded systems, we introduce an object analysis pattern, called the {\it detector} pattern, that provides a reusable strategy for capturing the requirements of failsafe fault-tolerance in an existing conceptual model, where a failsafe system is expected to preserve its safety requirements even when faults occur~\cite{Detector-Pattern-TR}. We also present a method that (i) uses the detector pattern to help create a behavioral model of a failsafe fault-tole rant system in UML, (ii) generates and model checks formal models of UML state diagrams of the fault-tolerant system, and (iii) visualizes the model checking results in terms of the UML diagrams to facilitate model refinement. We demonstrate our analysis method in the context of an industrial automotive application.
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format.