Specification and verification of a single-track railroad signaling in CafeOBJ

概要

論文の詳細を見る
A signaling system for a single-track railroad has been specified in CafeOBJ. In this paper, we describe the specification of arbitrary two adjacent stations connected by a single line that is called a two-station system. The system consists of two stations, a railroad line (between the stations) that is also divided into some contiguous sections, signals and trains. Each object has been specified in terms of their behavior, and by composing the specifications with projection the whole specification has been described. A safety property that more than one train never enter a same section simultaneously has also been verified with CafeOBJ.
社団法人電子情報通信学会の論文
2001-06-01