Note publique d'information : La validation des systèmes critiques réalistes nécessite d'être capable de modéliser
et de vérifier formellement des données complexes, du parallélisme asynchrone, et
du temps-réel simultanément. Des langages de haut-niveau ont une syntaxe concise et
une grande expressivité pour représenter ces aspects. Cependant, ils disposent de
peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking.
Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas,
tels que les automates temporisés et les réseaux de Petri temporisés. Les modèles
intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles
graphiques. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui
enrichit le modèle NTIF de constructions temps-réel et de compositions parallèles
de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et
intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable
d'exprimer les constructions principales des langages de haut-niveau. Nous présentons
aussi des traducteurs d'ATLANTIF vers des modèles graphiques. Ainsi, ATLANTIF étend
la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que
nous illustrons par un exemple.
Note publique d'information : The validation of real-life critical systems raises the challenge of being able to
formally model and verify complex data, synchronous concurrency, and real-time aspects
simultaneously. High-Ievellanguages, such as those inheriting from the theoretical
foundations of process algebras, provide a concise syntax and a high expressive power
regarding these aspects. Yet, they lack software tools enabling the application of
efficient model checking algorithms. On the other hand, such tools exist for graphical,
lower level, models such as timed automata (e.g., UPPAAL) and time Petri nets (e.g.,
TINA). Intermediate models are a key to bridge the gap between languages and graphical
models. For instance, NTIF (New Technology Intermediate Format) was proposed to represent
untimed sequential processes that handle complex data. ln this thesis, we propose
a new model named ATLANTIF, which extends NTIF with real-time constructs and parallel
compositions of sequential processes. Their synchronization is expressed in a simple
and intuitive way using the new notion of synchronizers. We show that ATLANTIF is
capable of expressing the main constructs of high-Ievellanguages. We also present
translators from ATLANTIF to timed automata (for verification using UPPAAL) and to
time Petri nets (for verification using TINA). Thus, ATLANTIF extends the class of
systems that can practically be formally verified, which we iIIustrate along an example.
paprika.idref.fr
data.idref.fr
Documentation
