An integrated methodology for model checking and failure coverage of fault tolerant architectures for by-wire systems
Mira Supal, Rami Debouk · international conference on Modelling and simulation · 2007
In an effort to generate a safety assessment of various fault tolerant architectures for by-wire systems, we developed a methodology integrating system model checking including exercising all redundant aspects of the fault tolerant design. The system model definition includes both normal and failed modes of operation. The nominal behaviour operation and the failed mode of operation are checked via formal verification of some fault tolerance requirements. The comparison of the architectures can consist of several measures: fault recovery latency, fault tolerance to single point failures, fault tolerance to multiple point failures, and the complexity of the verification property observers. Failure coverage comparison of the designs can be facilitated by a proposed systematic management of verification of recovery properties for a set of failure modes.