Verification of Replication Architectures in AADL

An established approach to achieve fault tolerance is to deploy multiple copies of the same functionality on multiple processors to ensure that if one processor fails another can provide the same functionality. This approach is known as replication. In spite of the number of studies on the topic, designing a replication pattern is still error prone. This is due to the fact that its final behavior is the result of the combination of design decisions that involves reasoning about a collection of non-deterministic events such as hardware failures and parallel computations. In this paper we present an approach to model replication patterns in the architecture analysis and design language (AADL) and analyze potentially unintended behaviors. Such an approach takes advantage of the strong semantics of AADL to model replication patterns at the architecture level. The approach involves developing two AADL models. The first one defines the intended behavior in synchronous call sequences. And the second model describes the replication architecture. These two models are then compared using a differential model in Alloy where the requirements of the first model and the concurrency and potential failure of the second are combined. The additional behaviors discovered in this model are presented to the designer as potential errors in the design. The designer then has the opportunity to modify the replication architecture to correct these behaviors or qualify them as valid behaviors. Finally, we validated our approach by recreating the verification experiment presented in but limiting ourselves to the AADL syntax.