For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2001/06/01
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)>>
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.