Timed Automaton RVT-Grammar for Workflow Translating

MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS

International Journal of Foundations of Computer Science ◽

10.1142/s0129054112400382 ◽

2012 ◽

Vol 23 (04) ◽

pp. 831-851 ◽

Cited By ~ 2

Author(s):

GUOQIANG LI ◽

XIAOJUAN CAI ◽

SHOJI YUEN

Keyword(s):

Real Time ◽

Timed Automata ◽

Expressive Power ◽

Behavioral Model ◽

Parallel Composition ◽

Real Time Systems ◽

Modeling And Analysis ◽

Compositional System ◽

Time Systems ◽

Timed Automaton

Timed automata are commonly recognized as a formal behavioral model for real-time systems. For compositional system design, parallel composition of timed automata as proposed by Larsen et al. [22] is useful. Although parallel composition provides a general method for system construction, in the low level behavior, components often behave sequentially by passing control via communication. This paper proposes a behavioral model, named controller automata, to combine timed automata by focusing on the control passing between components. In a controller automaton, to each state a timed automaton is assigned. A timed automaton at a state may be preempted by the control passing to another state by a global labeled transition. A controller automaton properly extends the expressive power because of the stack, but this can make the reachability problem undecidable. Given a strict partial order over states, we show that this problem can be avoided and a controller automaton can be faithfully translated into a timed automaton.

Download Full-text

Model Checking via Reachability Testing for Timed Automata

BRICS Report Series ◽

10.7146/brics.v4i29.18955 ◽

1997 ◽

Vol 4 (29) ◽

Cited By ~ 3

Author(s):

Luca Aceto ◽

Augusto Burgueno ◽

Kim G. Larsen

Keyword(s):

Model Checking ◽

Timed Automata ◽

Reachability Problem ◽

Liveness Properties ◽

Time Logic ◽

Definition Of ◽

Reachability Testing ◽

Time Systems ◽

Timed Automaton ◽

Theoretical Side

In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S. <br />The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version of<br />the ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.

Download Full-text