Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format

Abstract. To model real-life critical systems, one needs“high-level”languages to express three important concepts: complex data structures, concurrency, and real-time. So far, the verification of timed systems has been successfully applied to “low-level” models, such as timed extensions of automata or of Petri nets. To bridge the gap between high-level languages, which allow a concise modeling of systems, and low-level models, for which efficient algorithms and tools have been designed, intermediate models are needed. In this paper, we propose the Atlantif intermediate model, an extension with real-time and concurrency of the Ntif (New Technology Intermediate Format) intermediate model. We define the formal semantics of Atlantif and present a translator from Atlantif to timed automata (for verification using Uppaal), and to time Petri nets (for verification using Tina).

• Type: Conference
• Year: 2009
• Where: IFM
• Authors: Jan Stöcker, Frédéric Lang, Hubert Garavel
• Keywords: Formal Methods, IFM 2009, Intermediate Model, Petri Nets, Real-life Critical Systems