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. The proposed methodology is based on the use of formal modeling tools and formal methods for verification of fault tolerance requirements and failure coverage assessments. Safety assessment of a by-wire system is based on a set of requirements and a system model that includes both nominal as well as failed modes of operation. The focus is on the modeling and analysis of the failure recovery decision and control logic in the bywire system.
An integrated methodology for model checking and failure coverage of fault tolerant architectures for by-wire systems
Integrierte Methodenentwicklung für Modellüberprüfung und Fehlfunktionsbehandlung der fehlertoleranten Architekturen für automatische Fahrzeugführungssysteme
2007
6 Seiten, 4 Bilder, 8 Quellen
Aufsatz (Konferenz)
Englisch
Validating requirements for fault tolerant systems using model checking
Tema Archiv | 1998
|Fault Tolerant Avionics Systems Architectures Study
NTIS | 1974
|