Soutenance de thèse de Nuno GASPAR // PhD defense on the 16th December 2014 at I3S(Algorithmes) at 1.30 pm

Title: Mechanized support for the formal specification, verification and deployment of component-based applications.
Jury composition:
Advisors:  Eric Madelaine (INRIA)
                  Ludovic Henrio (CNRS)
reviewers: Frédéric Loulergue (Université d’Orléans)
                  Alan Schmitt (INRIA)
examiners: Luis Barbosa (Universidade do Minho)      
                   Yves Bertot (INRIA)
                   Denis Caromel (Activéon)
In this thesis we address the formal specification, verification and deployment of distributed and reconfigurable GCM applications. Our first contribution is an industrial case study on the behavioural specification and verification of a reconfigurable distributed application: The HyperManager. This promotes the use of formal methods in an industrial context, but also puts in evidence the necessity for alternative and/or complementary approaches in order to better address such undertakings.

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.

Leave a Reply