Architectural-Based Validation of Fault-Tolerant Software

Many architecture-centred approaches have been proposed for constructing dependable component-based systems. However, few of them provide an integrated solution for their development that combines fault prevention, fault removal, and fault tolerance techniques. This paper proposes a rigorous development approach based on an architectural abstraction, which combines formal methods and robustness testing. The architectural abstraction assumes a crash failure semantics, and when it is instantiated as an architectural element provides the basis for architecting fault tolerant systems. The architecture is formally specified using the B-method and CSP. Assurances that the software system is indeed dependable are obtained by combining formal specification for removing ambiguities from the architectural representation, and robustness testing for validating the source code against its software architecture. The feasibility of the proposed approach is illustrated in the context of a financial critical system.