Modeling Faults of Distributed, Reactive Systems

Formal methods can improve the development of systems with high quality requirements, since they usually o er a precise, nonambiguous speci cation language and allow rigorous veri cation of syserties. Usually, these mainly abstract speci cations are idealistic and do not re ect faults, so that faulty behavior - if treated at all - must be speci ed as part of the normal behavior, increasing the complexity of the system. It is more desirable to distinguish normal and faulty behavior, making it possible to reason about faults and their e ects. In this paper the notions of faults, errors, failures, error detection, error messages, error correcting components and fault tolerance are discussed, based on a formal model that represents systems as composition of interacting components that communicate asynchronously. The behavior of the components is described by black-box properties and state transition systems, with faults being modeled by modi cations of the properties or transitions.

• Type: Conference
• Year: 2000
• Where: FTRTFT
• Authors: Max Breitling
• Keywords: Cations, Faulty Behavior, Formal Methods, FTRTFT 2000, Speci Cations