Architectural Concurrency Equivalence with Chaotic Models

During its lifetime, embedded systems go through multiple changes to their runtime architecture. That is, threads, processes, and processor are added or removed to/from the software and hardware. These additions can have multiple motivations such as adding tolerance to failures or changes in the hardware architecture for new releases of the system. During these modifications, one of the big challenges is ensuring that no new error is introduced. This verification tends to be difficult given that modifying the concurrency structure of an application has multiple side effects difficult to discover. In this paper we propose a model-based technique to compare the concurrency structures of two architectural models. This exhaustive comparison is based on the semantics of AADL, an architecture description language, and its model in Alloy, a formal verification language. This verification guides the designer to fully define the desired behaviors as well as the side effects that can be tolerated. We demonstrate the use of the modeling with a simple model from the automotive industry.