IEICE TRANSACTIONS on Fundamentals
Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E84-A No.6 pp.1471-1478
- Publication Date
- 2001/06/01
- Publicized
- Online ISSN
- DOI
- 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))
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Takahiro SEINO, Kazuhiro OGATA, Kokichi FUTATSUGI, "Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ" in IEICE TRANSACTIONS on Fundamentals,
vol. E84-A, no. 6, pp. 1471-1478, June 2001, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e84-a_6_1471/_p
Copy
@ARTICLE{e84-a_6_1471,
author={Takahiro SEINO, Kazuhiro OGATA, Kokichi FUTATSUGI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ},
year={2001},
volume={E84-A},
number={6},
pages={1471-1478},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={June},}
Copy
TY - JOUR
TI - Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1471
EP - 1478
AU - Takahiro SEINO
AU - Kazuhiro OGATA
AU - Kokichi FUTATSUGI
PY - 2001
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E84-A
IS - 6
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - June 2001
AB - 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.
ER -
English
