PostScript
NTIF: A General Symbolic Model for Communicating Sequential Processes
with Data
Hubert Garavel, Frédéric Lang
Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal
Techniques for Networked and Distributed Systems FORTE'2002 (Houston, Texas,
USA), November 2002
Full version available as INRIA Research Report RR-4666.
Abstract:
One central problem in the computer-aided verification of concurrent systems consisting of communicating sequential processes with data is to find suitable symbolic models. Such models should provide a compact computer representation for control and data flows, and should be appropriate for mainstream verification techniques such as model checking and theorem proving. A number of symbolic models have been proposed, many of which based on the guarded commands (also known as condition/action) paradigm. In this paper, we draw attention to the limitations of this paradigm and propose a better model named NTIF (New Technology Intermediate Form), which is well-adapted to compiling high-level, concurrent languages (such as the recent E-LOTOS standard). Finally, we present two software tools developed for NTIF and report about the use of NTIF for modeling two embedded applications in smart cards.
| 30 pages | |
PostScript |
| Cumulated slides (in English) about NTIF by H. Garavel and F. Lang | |
| Cumulated slides (in French) about NTIF by H. Garavel and F. Lang | |