文献

J-GLOBAL ID：202002280902659703   整理番号：20A0117900

Event-Bに基づいた鉄道システムの実践的な形式化と検証

Practical formalization and verification of railway system based on Event-B

著者 (2件)： 太田十字光 (北陸先端科学技術大学院大) ,  青木利晃 (北陸先端科学技術大学院大)
資料名： 情報処理学会研究報告(Web)  (IPSJ Technical Report (Web))
巻： 2019  号： SE-203  ページ： Vol.2019-SE-203,No.6,1-8 (WEB ONLY)  発行年： 2019年12月05日 
JST資料番号： U0451A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 地方の鉄道路線で一般的な単線路線の運行計画が危険を含むかどうかの判定を支援する形式化に基づいた手法を提示する.提示手法は単線路線一般で共通する性質を抽出して路線のモデルとそれを元に記述するスケジュール,そして安全性確保のため安全制約からなる参照モデルでありEvent-Bで記述する.参照モデル上に検証したい具体的な路線を記述して危険が含まれるかどうか検証する.具象路線を含めた参照モデル全体の証明責務を証明することで検証対象路線に危険が含まれないことを言う.提示手法は具体的な路線を個別に形式化するより少ないコストで実現できることを示し,コスト的な問題から形式化の導入が遅れている地方路線への形式手法導入に貢献することを示す.(著者抄録)

シソーラス用語： *鉄道 ,  *運行管理 ,  *スケジューリング ,  経路 ,  鉄道駅 ,  制約条件 ,  安全性 ,  形式的手法【計算機】 ,  規範モデル ,  階層構造 ,  鉄道信号 ,  モデリング ,  Event-B ,  鉄道路線
準シソーラス用語： 安全生制約 ,  参照モデル ,  *鉄道システム

分類 (2件)： 輸送と業務  (TC01030N) ,  ネットワーク法  (KA03040X)

引用文献 (13件)：

• Robert Abo, Laurent Voisin, The Unreasonable Effectiveness of B for Data Validation and Modelling of Railway Systems, LNCS 10598, 2017
• Jean-Raymond Abrial, Modeling in Event-B. CAMBRIDGE UNIVERSITY PRESS 2010.
• Jean-Raymond Abrial, The B-Book, CAMBRIDGE UNIVERSITY PRESS 1996.
• Zakaryae Boudi, Rahma Ben-Ayed, El Miloudi El Koursi, Simon Collart-Dutilleul, Thomas Nolasco, Mohamed Haloua, A CPN/B method transformation framework for railway safety rules formal validation, Eur. Transp. Res. Rev, 2017M. Butler1, D. Dghaym1, T. Fischer, T.S. Hoang1, K. Reichl, C. Snook1,and P. Tummeltshammer, Formal Modelling Techniques for Efficient Development of Railway Control Products, LNCS10598, 2017
• Anne E. Haxthausen and Jan Peleska, Formal Development and Verification of a Distributed Railway Control System, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL. 26, NO. 8, AUGUST 2000

タイトルに関連する用語 (4件)： Event-B ,  鉄道システム ,  形式化 ,  検証