Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time SystemsReport as inadecuate

Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems - Download this document for free, or read online. Document in PDF available to download.

1 Radboud university Nijmegen 2 Aalborg University Denmark 3 IRIT - Institut de recherche en informatique de Toulouse

Abstract : 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.

Keywords : Callable timed automata Timed automata Dynamic real-time systems

Author: Abdeldjalil Boudjadar - Frits Vaandrager - Jean-Paul Bodeveix - Mamoun Filali -

Source: https://hal.archives-ouvertes.fr/


Related documents