Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ

Takahiro SEINO  Kazuhiro OGATA  Kokichi FUTATSUGI  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E84-A   No.6   pp.1471-1478
Publication Date: 2001/06/01
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Papers Selected from 2000 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2000))
CafeOBJ,  formal method,  railroad signaling,  

Full Text: PDF(413KB)>>
Buy this Article

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 operations 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.