In order to facilitate incremental modeling and analysis of fault-tolerant embedded systems, we introduce an object analysis pattern, called the detector pattern, that provides a reusable strategy for capturing the requirements of failsafe fault-tolerance in an existing conceptual model, where a failsafe system satisfies its safety requirements even when faults occur. We also present a method that (i) uses the detector pattern to help create a behavioral model of a failsafe fault-tolerant system in UML, (ii) generates and model checks formal models of UML state diagrams of the faulttolerant 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.
Ali Ebnenasir, Betty H. C. Cheng