「信号装置仕様の検証を通じたBメソッドにおける仕様記述法の検討」

［情報処理学会論文誌 プログラミング Vol.7, No.2, pp.20-35］
［論文概要］

　単線区間の運転方向を制御する自動閉そく装置について，形式手法の1つであるBメソッドによりモデル化を行い，定理証明による検証を行った．3つの仕様について検証を行ったが，仕様が複雑になるにつれ，証明責務が急激に増えていった．そこで証明責務や対話証明の命令列の数（User Pass）と仕様記述の関係を考察し，証明責務の生成数が増える要因を示した．さらに証明責務やUser Passの数を減らすための仕様記述法を検討し，この手法を単線区間向け閉そく装置の仕様記述に対して適用した結果，証明作業の負担を軽減することができた．

［推薦理由］

　当該論文は、鉄道の信号保安制御に関わる自動閉そく装置について、形式手法Bメソッドによる検証と、証明作業の負担軽減につながる仕様記述法を検討した結果について報告したものである。Bメソッドのツールは証明責務を生成するが、それらのうち自動証明されないものはユーザが対話的に定理証明する必要がある。論文では、同じ意味の仕様であっても、その記述法が証明責務全体や自動証明されないものの個数に影響を与えることに着目しており、新規性が見られる。また、扱った3種類の自動閉そく装置のうち、まず比較的仕様が小規模なものについて詳細に分析することで仕様記述法の指針を与え、その指針を仕様が複雑な装置に適用して実際に証明作業の負担軽減につながることを示しており、手法の有効性を裏付ける論文構成となっている。高信頼性が求められる実際の装置に対する、定理証明を伴う形式手法の適用事例としても意義深い。以上の理由により、論文賞として推薦する。