作成者 |
|
|
|
|
|
|
本文言語 |
|
出版者 |
|
|
発行日 |
|
収録物名 |
|
巻 |
|
号 |
|
開始ページ |
|
終了ページ |
|
出版タイプ |
|
アクセス権 |
|
JaLC DOI |
|
関連DOI |
|
関連URI |
|
関連情報 |
|
概要 |
The verification of safety requirements is a fundamental problem in railway signalling system design. Especially, specification of railway inter-locking systems, which control railway signals and poin...ts in a station in a safety-critical manner, becomes very complex and hard to verify. Recently in this fields, formal verification is expected to be a promising technique for verifying safety requirements. This paper describes how to verify a railway inter-locking specifications by the model checker SPIN which is a formal verification tool. In this method, a railway inter-locking system is described as a finite state machine and safety requirements are given by temporal logic formulas. Then, SPIN checks that the state machine satisfies the requirements.続きを見る
|