Verifying Architectural Variabilities in Software Fault Tolerance Techniques

This paper considers the representation of different software fault tolerance techniques as a product line architecture (PLA) for promoting the reuse of software artifact. The proposed PLA enables to specify a series of closely related architectural applications, which is obtained by identifying variation points associated with design decisions regarding software fault tolerance. These decisions are used to choose the appropriate technique depending on the features selected, e.g, the number of redundant resources, or the type of adjudicator. The proposed approach also comprises the formalisation of the PLA, using B-method and CSP, for systematising the verification of fault-tolerant software systems at the architectural level. The properties verified cover two complementary contexts: the selection of the correct architectural variabilities for instantiating the PLA, and also the properties of the chosen fault tolerance techniques.