Développement formel de systèmes temps réel à l'aide de SDL et IF ( Compilation pour système temps réel )
Institution:
Lyon, INSADisciplines:
Directors:
Abstract EN:
Real Time system (RTS) is a system which interacts strongly with a physical process. It is subject to strong reliability and real time constraints and to ensure the respect of the real time constraints, it is necessary o use formal languages and techniques. SDL seems to be a good candidate for the RTS development: it is a formal standardized language dedicated to distribute systems. Moreover, several works have been done to extend its use for Real Time and dedicated systems. On the basis of the SDL language, this thesis proposed a framework for the specification, design and behavioural validation of a Real-Time System supported by multitasking real-time operating systems. The specification and a design stages are formalized on the basis of the SDL specialization. To explicit the real time constraints, a precise semantic is given thanks to the IF language. Afterwards, it is shown how the correctness of an application can be formally checked.
Abstract FR:
Un système temps réel est un système qui interagit avec un environnement physique en remplissant souvent des missions critiques (une faute du système peut avoir des conséquences graves). Il sera dit correct s'il possède les bonnes fonctionnalités réalisées à temps (contraintes temporelles imposées par l’environnement ou par l’utilisateur). La validation fonctionnelle et temporelle de ces systèmes est une nécessité forte (fournisse des résultats fiables). Dans le cadre des implémentations à base d’exécutifs multitâche temps réel, le travail présenté dans cette thèse tente d’apporter une approche complète formelle de la suite spécification, conception et implémentation. Dans ce cadre, il porte aussi un intérêt particulier à une méthode de validation de la transformation entre le modèle de contraintes et le modèle d'exécution. Nous formalisons plus particulièrement des phases de spécification et la conception en utilisant le langage formel SDL. Ensuite, nous précisons explicitement les contraintes temps réel à nos modèles en utilisant le langage IF. Enfin, nous montrons formellement comment la correction du développement d’une application est prouvée