Skip to Main content Skip to Navigation
Reports

NTIF: A General Symbolic Model for Communicating Sequential Processes with Data

Hubert Garavel 1 Frédéric Lang 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG [2007-2015] - Laboratoire d'Informatique de Grenoble [2007-2015]
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 report, we draw attention to the limitations of this paradigm and propose a better model named (New Technology Intermediate Form), which is well-adapted to compiling high-level, concurrent languages (such as the recent ELOTOS 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.
Document type :
Reports
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071919
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:15:31 PM
Last modification on : Friday, July 17, 2020 - 11:10:25 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:44:34 PM

Identifiers

  • HAL Id : inria-00071919, version 1

Collections

Citation

Hubert Garavel, Frédéric Lang. NTIF: A General Symbolic Model for Communicating Sequential Processes with Data. [Research Report] RR-4666, INRIA. 2002. ⟨inria-00071919⟩

Share

Metrics

Record views

361

Files downloads

349