信号設備の安全性に関する仕様検証手法の適用検討

摘要

フォーマルメソッドを用いて信号装置の仕様を数学的に検証する手法について，単線区間向けの閉そく装置を例として行った。具体的には1.一旦方向回線が設定されると，着駅で方向てこを扱っても設定が保持される。2.両駅での方向回線の設定が同時に列車を出発させる条件にならない。