Etude de l'analyse automatique des règles de conception des systèmes multitâches temps réel
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
The works presented in this thesis propose a novel method to verify the application of design rules based on the analysis of the source code. Design rules allow to guarantee the presence of sound properties on the final program. Therefore, verifying their presence allows to guarantee the presence of the associated properties. On the opposite, if a particular rule is not found to be applied upon the final program, no judgment may be given regarding the quality of the source code, but the fact that the developer didn’t follow the rule is significant in itself. The verifications are particularly aimed towards the problems specific to multitask systems. The introduction of a dynamic non-deterministic scheduling between the tasks renders the analyses by classical proof of programs inefficient or even useless. This led us to propose a new program analysis technique, based on multiple levels analysis and program slicing. The technique proposed is based on the study of the source code only. The analyses must be performed on this element only, if no other element regarding the system’s design is available.
Abstract FR:
Les travaux présentés dans cette thèse ont pour objectif de proposer une méthode permettant l’analyse de l’application de règles de conception à partir du code source d’une application. Les règles de conception permettent de garantir des propriétés intéressantes sur le programme final. Aussi, vérifier leur application permet-il de garantir la présence de ces propriétés. Au contraire, si la règle ne se trouve pas appliquée dans le programme final, alors il n’est pas possible d’émettre un avis quant à la qualité du code source, mais le fait que le développeur ait ignoré la règle est significatif. Les vérifications s’intéressent particulièrement aux problèmes liés aux systèmes multitâches. L’introduction d’un ordonnancement non-déterministe entre les tâches rend les analyses par les méthodes classiques de preuve de programme peu ou pas efficaces. C’est pourquoi une technique de décomposition de programme est proposée, ainsi que des méthodes de vérification à plusieurs niveaux. La technique développée se base sur l’étude du code source seul. Les analyses doivent n’être possibles qu’à partir de cet élément, en l’absence de tout autre élément de conception.