TY - GEN
T1 - Continuous real time models in practice
AU - Weise, Carsten
AU - Margaria, Tiziana
PY - 1993
Y1 - 1993
N2 - We present a method for the automatic verification of observational equivalence for real lime processes over a continuous time domain. The method allows us to prove the behavioural compatibility of two systems from, the communication point of view by means of an efficient local partitioning algorithm, which must be applied to an appropriate model of the system: the timer region graphs. We concentrate here on the derivation of this model, and only informally explain the subsequent partitioning algorithm by applying it to an example.
AB - We present a method for the automatic verification of observational equivalence for real lime processes over a continuous time domain. The method allows us to prove the behavioural compatibility of two systems from, the communication point of view by means of an efficient local partitioning algorithm, which must be applied to an appropriate model of the system: the timer region graphs. We concentrate here on the derivation of this model, and only informally explain the subsequent partitioning algorithm by applying it to an example.
UR - http://www.scopus.com/inward/record.url?scp=84884625798&partnerID=8YFLogxK
U2 - 10.1109/EMWRT.1993.638859
DO - 10.1109/EMWRT.1993.638859
M3 - Conference contribution
AN - SCOPUS:84884625798
SN - 081864110X
SN - 9780818641107
T3 - Proceedings - Euromicro Conference on Real-Time Systems
SP - 8
EP - 13
BT - Proceedings - 5th Euromicro Workshop on Real-Time Systems, ECRTS 1993
T2 - 5th Euromicro Workshop on Real-Time Systems, ECRTS 1993
Y2 - 22 June 1993 through 24 June 1993
ER -