Detecting Architectural Mismatches in Process Algebraic Description of Software Systems

Formalizing the description of software systems helps to de-tect the presence of architectural mismatches that can arise when assembling software components together. In this pa-per we identify three causes of architectural mismatches: incompatibility between two components due to a single in-teraction, incompatibility between two components due to the combination of several interactions, and lack of interop-erability among a set of components forming a cyclic topol-ogy. We then show how to deal with all of them within a uniform, process algebraic framework. We begin with the first two causes by strengthening a previously defined archi-tectural compatibility check based on observational equiv-alences, in order to achieve a deadlock freedom result for the set of components interacting via a certain connection. We subsequently concentrate on the third cause by defining a novel architectural interoperability check based on obser-vational equivalences, which guarantees absence of dead-lock within a set of interacting components forming a cyclic topology. We finally assess the adequacy of our architec-tural interoperability check by applying it to the description of a cruise control system. 1