Conception d'un outil de débogage formel pour systèmes logiciels et matériels selon l'approche "Debug as Design"
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
In order to reduce the time required to validate critical complex Systems, all information available during the classical V-Model should be used as soon as possible to check every system aspect. Further, two evolutions have to be taken into account. On the one hand, the size of complex Systems increases. On the other hand, designers must also consider the diversity of used components and the mixing of hardware and software aspects. It may imply to manage different levels of abstraction in sizeable Systems. To address this industrial and theoretical challenge, we present a new hierarchical model which is refinable and modular. It enables both simulating and analyzing a complex System. We then adapt two techniques of static analysis to this model: abstract interpretation and symbolic execution. Their joint use allows us to extract the abstract behavior of a system or a component, in order to check whether it respects a specification with adhoc tool.
Abstract FR:
Afin de réduire les délais de validation des systèmes complexes critiques, toutes les informations disponibles à chaque phase du traditionnel cycle en V devraient être utilisées pour valider le plus tôt possible chaque aspect du système. Par ailleurs, il faut également prendre en compte deux évolutions. D'un côté, la taille des systèmes augmente de manière continue. D'un autre côté, les concepteurs doivent désormais composer avec la diversité des composants utilisés et le mélange des aspects matériels et logiciels, ce qui peut les amener à gérer de multiples abstractions au sein de systèmes de grande taille. Pour relever ce défi, tant industriel que théorique, nous proposons un nouveau modèle hiérarchique raffinable et modulaire, qui permet à la fois de simuler et d'analyser un système complexe. Nous adaptons ensuite deux techniques d'analyse statique à ce modèle: l'interprétation abstraite et l'exécution symbolique. Enfin, leur utilisation conjointe nous a permis d'extraire le comportement abstrait d'un système ou de ses composants, afin d'effectuer une validation de spécification à l'aide d'outils adaptés.