Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 From I/O Automata to Timed I/O Automata
From I/O Automata to
Timed I/O Automata
A solution to the `Generalized Railroad Crossing' in
Isabelle/HOLCF
The model of timed I/O automata represents an extension
of the model of I/O automata with the aim of reasoning
about real-time systems. A number of case studies
using timed I/O automata has been carried out, among them
a treatment of the so-called
Generalized Railroad Crossing (GRC). An already existing formalization
of the meta-theory of I/O automata within Isabelle/HOLCF
allows for fully formal tool-supported verification using
I/O automata. We present a modification of this formalization
which accomodates for reasoning about timed I/O automata.
The guiding principle in choosing the parts of the meta-theory
of timed I/O automata to formalize has been to provide all
the theory necessary for formalizing the solution to the
GRC. This leads to a formalization of
the GRC, in which not only
the correctness proof itself has been formalized, but also the
underlying meta-theory
of timed I/O automata, on which the correctness proof is based.
The paper appeared in Y. Bertot, G. Dowek, Ch. Paulin-Mohring, and
L. Théry, editors, Proceedings of the 12th International
Conference on Theorem Proving in Higher Order
Logics, TPHOLs'99, Lecture Notes in Computer
Science, Nice, France, 1999, pages 273-290. Springer Verlag.