Railroad Crossing and Model Checking

Citation: Danièle Beauquier and Anatol Slissenko, "The Railroad Crossing Problem: Towards Semantics of Timed Algorithms and their Model-Checking in High-Level Languages", in M. Bidoit and M. Dauchet, eds., "Proceedings of TAPSOFT'97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE", Springer Lecture Notes in Computer Science 1214, 202-212.
Summary: The ASM specification of the railroad crossing problem is analyzed to create an appropriate timed transition system, suitable for algorithmic model checking.
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. An extension paper is also available.