Formal specification and verification of distributed component systems
Spécification et vérification formelles des systèmes de composants répartis
Résumé
A component is a self contained entity that interacts with its environment through well-defined interfaces. The component library Fractive provides high level primitives and semantics for programming Java applications with distributed, asynchronous and hierarchical components. It also provides a separation between functional and non-functional aspects, the latter allows the execution control of a component and its dynamic evolution. In this thesis, we provided a formal framework to ensure that the applications built from Fractive components are safe. Safe, in the sense that each component must be adequate to its assigned role within the system, and the update or replacement of a component should not cause deadlocks or failures to the system. We introduced a new intermediate format extending the networks of communicating automata, by adding parameters to their communication events and processes. Then, we used this intermediate format to give behavioural specifications of Fractive applications. We assumed the models of the primitive components as known (given by the user or via static analysis). Using the component description, we built a controller describing the component´s non-functional behaviour. The semantics of a component is then generated as the synchronisation product of: its LTSs sub-components and the controller. The resulting system can be checked against requirements expressed in a set of temporal logic formulas, as illustrated in the thesis report.
Un composant est une entité autonome qui interagit avec son environnement par des interfaces correctement spécifiées. Fractive est une implantation du modèle de composants Fractal qui propose des primitives de haut niveau et une sémantique pour la programmation à base de composants Java distribués, asynchrones et hiérarchiques. Fractive propose également une séparation entre aspects fonctionnels et non-fonctionnels, ces derniers permettant un contrôle de l´exécution d´un composant et de son évolution dynamique. Dans cette thèse, nous proposons un outillage formel pour la vérification d´applications construites avec Fractive. Cela permet de vérifier que chaque composant remplit correctement le rôle qui lui a été assigné au sein du système, et que la mise à jour ou le remplacement d´un composant n´engendre pas d´interblocage ou de panne du système. Nous avons défini un nouveau format intermédiaire qui étend les réseaux d´automates communicants, en paramétrisant leurs événements de communication et de traitement. Nous avons ensuite utilisé ce format intermédiaire pour définir les spécifications comportementales d´applications Fractive. Nous considérons que les modèles des composants primitifs sont connus (donnés par l´utilisateur ou par analyse statique). En utilisant la description des composants, nous construisons un contrôleur décrivant le comportement non fonctionnel du composant. La sémantique d´un composant est ensuite générée comme le produit de synchronisation des LTSs de ses sous-composants et du contrôleur. Le système résultant peut être vérifié par rapport aux besoins exprimés dans un ensemble de formules de logique temporelle, comme illustré dans le manuscrit.
Loading...