Abstract lattices for the verification of systèmes with stacks and queues

Titre non disponible

Tristan Le Gall (1)

1 VERTECS - Verification models and techniques applied to testing and control of reactive systems

Many scientific studies analysed the FIFO channel systems, but none offered a fully satisfying solution. We propose to tackle this problem within the abstract interpretation framework, by defining some abstract lattices adapted to this kind of systems. We first consider systems with a finite alphabet of messages, then we consider more complex systems, with an infinite alphabet of messages. This leads us to define and to study a new kind of automata: the lattice automata. Those automata are also useful for the analysis of programs with a call stack.

L'analyse des systèmes communiquant par file a fait l'objet d'études scientifiques nombreuses mais qui n'ont pu offrir des solutions totalement satisfaisantes. Nous proposons d'aborder ce problème dans le cadre de l'interprétation abstraite, en définissant des treillis abstraits adaptés à ce type de systèmes. Nous considérons d'abord le cas où les messages échangés sont assimilables à un alphabet fini, puis nous nous attaquons au cas, plus difficile, des messages portant des valeurs entières ou réelles. Ce problème nous amène à définir et à étudier un nouveau type d'automate, les automates de treillis. Ces automates de treillis peuvent également être utilisés pour l'analyses des programmes utilisant une pile d'appels.

Mots clés: treillis abstrait; vérification; automates communiquants

Domaines: Génie logiciel [cs.SE]

Tristan Le Gall. Abstract lattices for the verification of systèmes with stacks and queues. Software Engineering [cs.SE]. Université Rennes 1, 2008. English. ⟨NNT : ⟩. ⟨tel-00424552⟩