Our second contribution is a framework, developed with the Coq proof assistant, for reasoning on software architectures: Mefresa. This encompasses the mechanization of the GCM specification, and the means to reason about reconfigurable GCM architectures. Further, we address behavioural concerns by formalizing a semantics based on execution traces of synchronized transition systems. Overall, it provides the first steps towards a complete specification and verification platform addressing both architectural and behavioural properties.
Finally, our third contribution is a new Architecture Description Language (ADL), denominated Painless. Moreover, we discuss its proof-of-concept integration with ProActive — a Java middleware for concurrent and distributed programming, and the de facto reference implementation of the GCM. Painless allows to specify parametrized GCM architectures, along with their structural reconfigurations, in a declarative-like language. Compliance with the GCM specification is evaluated by certified functional code extracted from Mefresa. This permits the safe deployment and reconfiguration of GCM applications.
