Spécification et vérification des ordonnanceurs temps réel en B
Institution:
Toulouse 3Disciplines:
Directors:
Abstract EN:
The purpose of this thesis is to propose a methodology for specifying and verifying of real time schedulers. The model to be analyzed and the scheduling policies are expressed using the Cotre language. This one can be considered as an architecture description language allowing the formal description of the system's behavior, as well as the constraints to be respected. The verification of the scheduled system relies on the translation of the model to timed automata. Our modeling of the preemptive schedulers to be translated into Uppaal, should manage time only through clocks. We then seek to validate our modeling using the B method. For that, we begin with an abstract specification of the schedulers, and we refined it by successive steps in order to take into account the characteristics of timed automata. We then verified the refinements hierarchy by proving the various generated proof obligations. In order to translate the B modeling of the schedulers into Uppaal, we defined a B0_Uppaal language and rules to be respected for the transformation. This translation is finally checked by schedulability properties expressed in the CTL logic.
Abstract FR:
L'objectif de cette thèse est de proposer une démarche de spécification et de validation des ordonnanceurs temps réel. Le modèle à analyser et les politiques d'ordonnancement sont exprimés à l'aide du langage Cotre. Ce dernier peut être considéré comme un langage de description d'architecture permettant la description formelle du comportement d'un système, ainsi que les contraintes à respecter. La vérification du système ordonnancé repose sur la traduction du modèle en automates temporisés. Notre modélisation des ordonnanceurs préemptifs devant être traduite en Uppaal, ne doit gérer le temps qu'à travers des horloges. Nous cherchons ensuite à valider notre modélisation en utilisant la méthode B. Pour cela, nous avons débuté par une spécification abstraite des ordonnanceurs, et nous l'avons raffiné par étapes successives afin de prendre en compte les caractéristiques des automates temporisés. Nous avons ensuite vérifié la hiérarchie des raffinements en prouvant les différentes obligations de preuve générées. Afin de traduire la modélisation B des ordonnanceurs en Uppaal, nous avons défini un langage B0_Uppaal et des règles à respecter lors de la transformation. Cette traduction est enfin vérifiée par des propriétés d'ordonnançabilité exprimées en logique CTL.