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 S 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 X which when put in parallel with will yield a network satisfying S. The method presented proceeds in
two steps: first, the implicit specification of X is transformed into an
equivalent direct specification of X; 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.
Available as PostScript, PDF.