A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata

Gomez, Rodolfo (2009) A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata. In: Proc. of the 7th Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS'09), 14-16 September, Budapest, Hungary, SEP 14-16, 2009, Budapest, HUNGARY. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)

Abstract

Timed Automata with Deadlines (TAD) are a form of timed automata that admit a more natural representation of urgent actions, with the additional advantage of avoiding the most common form of timelocks. We offer a compositional translation of a practically useful subset of TAD to timed safety automata (the well-known variant of timed automata where time progress conditions are expressed by invariants). More precisely, we translate networks of TAD to the modeling language of UPPAAL, a state-of-the-art verification tool for timed automata. We also describe an implementation of this translation, which allows UPPAAL to aid the design and analysis of TAD models.

Item Type: Conference or workshop item (Paper)
Additional information: (to appear)
Uncontrolled keywords: Urgent actions, Timed Automata with Deadlines, Uppaal
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 29 Mar 2010 12:16
Last Modified: 16 Jun 2014 15:29
Resource URI: http://kar.kent.ac.uk/id/eprint/24130 (The current URI for this page, for reference purposes)
  • Depositors only (login required):