TY - JOUR
AU - Jørgen Andersen
PY - 1994/12/11
Y2 - 2019/09/17
TI - Automatic Synthesis of Real Time Systems
JF - BRICS Report Series
JA - BRICS
VL - 1
IS - 45
SE - Articles
DO - 10.7146/brics.v1i45.21597
UR - https://tidsskrift.dk/brics/article/view/21597
AB - 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: (A_1 | . . . | A_n | X) sat S where S is a real time (logical) specification, A_1, ... , A_n 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 A_1, ..., A_n 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.
ER -