CTL
21 janvier 2011 - 10h30
Design, verification and implementation of systems of components (Phd Defense)
par Sophie Quinton de Verimag / UJF
Abstract: In this thesis, we have studied how component-based systems are designed, verified and then implemented. We have focused in particular on formalisms involving complex interactions, where connectors are not only used to transfer data but also play a role in the synchronization of components.
1. DESIGN AND VERIFICATION
Contracts are emerging as a concept of choice when systems are designed by teams working independently. They are design constraints for implementations which are maintained throughout the
development and life cycle of the system, thus being also useful for verification. Our goal is not to propose a new design framework but rather to define a minimal set of properties which a given contract theory should satisfy to offer some reasoning rules. In that sense, we aim at a separation of concerns between framework-dependent properties and generic proof rules. We have focused on finding definitions expressive enough to encompass a great variety of existing specification formalisms, and in particular those in which interaction is complex, like Reo and BIP. For those, reasoning about the structure of the system is essential and this is why our contracts have a structural part. We show how so-called circular reasoning entails a rule for proving dominance (refinement between contracts) without composing contracts and how it can be relaxed by combining several refinement relations. Our work has a practical motivation in the component frameworks HRC L0
and L1 defined in the SPEEDS IP project.
2. IMPLEMENTATION
The problem of synthesizing a distributed controller that imposes some global constraint on a system is, in general, undecidable. One can achieve decidability at the expense of reducing concurrency: we propose a method that synchronizes processes temporarily. In Basu et al., distributed control is achieved by first using model checking to precalculate the knowledge of each process, which reflects in a given local state all the possible situations of the other processes. Then, at runtime, the local controller of a process decides whether an action of that process can
be executed without violating the imposed constraint. We use model checking techniques as well to precalculate a minimal set of synchronization points, where joint knowledge, i.e., knowledge common to several processes, can be achieved during short coordination phases. After each synchronization, the participating processes can again progress independently until a further synchronization is called for. One practical motivation for this work is the distributed implementation of BIP systems.
Jury composé de :
- Albert Benveniste (IRISA/INRIA), Rapporteur
- Roberto Passerone (Université de Trente), Rapporteur
- Kim Larsen (Université d'Aalborg), Examinateur
- Jean-Bernard Stefani (INRIA Rhône-Alpes), Examinateur
- Stavros Tripakis (Cadence Research Labs), Examinateur
- Susanne Graf, (Verimag/CNRS), Directrice de thèse
