OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems

Boudjadar, Abdeldjalil and Vaandrager, Frits and Bodeveix, Jean-Paul and Filali, Mamoun Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems. (2013) In: 5th International Conference on Fundamentals of Software Engineering (FSEN 2013), 24 April 2013 - 26 April 2013 (Tehran, Iran, Islamic Republic Of).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/978-3-642-40213-5_8


Dynamic real-time systems, where the number of processes is not constant and new processes can be created on the fly like in object-based systems and ad-hoc networks, are still lacking a formal framework enabling their verification. Different toolboxes like Uppaal [21], Tina [10], Red [28] and Kronos [29] have been designed to deal with the modeling and analysis of real-time systems. Nevertheless, a shortcoming of these tools is that they can only describe static topologies. Other tools like Spin [18] allow the dynamic creation of processes, but do not consider time aspects. This paper presents a formal framework for modeling and verifying dynamic real-time systems. We introduce callable timed automata as a simple but powerful extension of standard timed automata in which processes may call each other. We show that the semantics of each call event can be interpreted either as an activation of the existing instance of the corresponding automaton (static instantiation), or a creation of a new concurrent instance (dynamic instantiation). We explore both semantical interpretations, static and dynamic, and give for each one the motivation and benefits with illustrating examples. Finally, we report on experiments with a prototype tool, which translates (a subset of) callable timed automata to UPPAAL systems.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 8161 Lecture Notes in Computer Science ISSN : 0302-9743. ISBN: 978-3-642-40212-8. The original PDF is available at : http://link.springer.com/chapter/10.1007%2F978-3-642-40213-5_8
HAL Id:hal-01231765
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Aalborg University (DENMARK)
Other partners > Radboud University (NETHERLANDS)
Laboratory name:
Deposited By: IRIT IRIT
Deposited On:28 Oct 2015 09:09

Repository Staff Only: item control page