Automatic Synthesis of Real Time Systems

Jørgen H. Andersen
Kåre J. Kristoffersen
Kim G. Larsen
Jesper Niedermann

In 6th NWPT, pages 448-464

Abstract:

This paper presents a method for automatically constructing real time systems directly from their specifications. The model-construction problem is considered for implicit specifications of the form:

where is a real time (logical) specification, are given (regular) timed agents and the problem is to decide whether there exists (and if possible exhibit) a real time agent which when put in parallel with will yield a network satisfying . The method presented proceeds in two steps: first, the implicit specification of is transformed into an equivalent direct specification of ; second, a model for this direct specification is constructed (if possible) using a direct model construction algorithm. A prototype implementation of our method has been added to the real time verification tool EPSILON.

Comments
BRICS, Department of Math. & Comp. Sc., Aalborg University.

Available as PostScript.

BRICS WWW home page