An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF Language

Jan Stoecker

Thèse de doctorat en informatique de Grenoble INP (Institut National Polytechnique de Grenoble), December 2009.

Abstract:

The validation of real-life critical systems raises the challenge of being able to formally model and verify complex data, asynchronous concurrency, and real-time aspects simultaneously. High-level languages, 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. In 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-level languages. 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 illustrate along an example.

306 pages

PDF

PostScript