Verifying bigraphical models of architectural reconfigurations

Abstract

ARCHERY is an architectural description language for modelling and reasoning about distributed, heterogeneous and dynamically reconfigurable systems. This paper proposes a structural semantics for ARCHERY, and a method for deriving labelled transition systems (LTS) in which states and transitions represent configurations and reconfiguration operations, respectively. Architectures are modelled by bigraphs and their dynamics by parametric reaction rules. The resulting LTSs can be regarded as Kripke frames, appropriate for verifying reconfiguration constraints over architectural patterns expressed in a modal logic. The derivation method proposed here applies Leifer's approach twice, and combines the results of each application to obtain a label representing a reconfiguration operation and its actual parameters. Labels obtained in this way are minimal and yield LTSs in which bisimulation is a congruence.