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

A signaling system for a single-track railroad has been specified in CafeOB J. In this paper, we describe the specification of arbitrary two adjacent s tations connected by a single line that is called a two-station system. The system consists of two stations, a railroad line (between the stations) th at 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 operations the whole specification has been described. A safety property that more than one train never enter a same se ction simultaneously has also been verified with CafeOBJ.