Railroad Crossing
and Continuous Time Semantics

Citation: Danièle Beauquier and Anatol Slissenko, "On Semantics of Algorithms with Continuous Time". Technical Report 97-15, Department of Informatics, Universite Paris-12, October 1997.
Summary: The authors consider a class of algorithms with explicit continuous time (a modified version of ASMs), a logic which suffices to write requirements specifications close to natural language, and the corresponding verification problem, all in a single logic. An enhanced logic from that used in the paper is presented and used to give a proof of correctness of the railroad crossing problem.
Subjects: Benchmark Examples, Distributed Systems, Real-Time Systems, Verification
Download: PostScript, PDF, Compressed PostScript.
Notes: See also the original paper on the railroad crossing problem, as well as a prior paper.