Integer Parameter Synthesis for Real-Time Systems

We provide a subclass of parametric timed automata (PTA) that we can actually and efficiently analyze, and we argue that it retains most of the practical usefulness of PTA for the modeling of real-time systems. The currently most useful known subclass of PTA, L/U automata, has a strong syntactical r...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on software engineering 2015-05, Vol.41 (5), p.445-461
Main Authors: Jovanovic, Aleksandra, Lime, Didier, Roux, Olivier H.
Format: Article
Language:English
Subjects:
Algorithms
Automata
Automation
Clocks
Computer Science
Cost accounting
Delays
Formal Languages and Automata Theory
Radiation detectors
Real time
Real-time systems
Software engineering
Studies
Upper bound
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We provide a subclass of parametric timed automata (PTA) that we can actually and efficiently analyze, and we argue that it retains most of the practical usefulness of PTA for the modeling of real-time systems. The currently most useful known subclass of PTA, L/U automata, has a strong syntactical restriction for practical purposes, and we show that the associated theoretical results are mixed. We therefore advocate for a different restriction scheme: since in classical timed automata, real-valued clocks are always compared to integers for all practical purposes, we also search for parameter values as bounded integers. We show that the problem of the existence of parameter values such that some TCTL property is satisfied is PSPACE-complete. In such a setting, we can of course synthesize all the values of parameters and we give symbolic algorithms, for reachability and unavoidability properties, to do it efficiently, i.e., without an explicit enumeration. This also has the practical advantage of giving the result as symbolic constraints between the parameters. We finally report on a few experimental results to illustrate the practical usefulness of our approach.
ISSN:0098-5589
1939-3520
DOI:10.1109/TSE.2014.2357445