(57)【要約】【課題】連動図表に従って列車制御を行った場合に、デッドロック回避など、鉄道保安に関する列車の要件を満たすことを、効率的に検証する。【解決手段】連動仕様検証装置は、連動図表を、鉄道路線上を運行する列車の在線位置を表わす形式言語仕様に変換し、形式言語仕様に、鉄道路線上を運行する列車情報である列車運行を設定し、列車運行を設定した形式言語仕様に対応する、鉄道路線上を運行する列車の要件を表す列車要件を生成し、、形式言語仕様のグラフ構成に関する性質として作成し、列車運行を設定した形式言語仕様が、生成した列車要件を満たすかを検証する。【選択図】図１
2011131812.tif 000002
【特許請求の範囲】
【請求項１】
鉄道路線に設置される連動装置の仕様を表す連動仕様を検証する連動仕様検証装置であって、
前記連動仕様、及び鉄道保安のための列車に関する要件種別である列車要件種別を格納する記憶部と、
前記連動仕様を、前記鉄道路線上を運行する列車の在線位置を表わす、グラフ形式の形式言語仕様に変換する変換部と、
前記形式言語仕様に、前記鉄道路線上を運行する列車情報である列車運行を設定した列車設定済み形式言語仕様を出力する設定部と、
前記記憶部に格納されている前記列車要件種別に基づいて、前記列車設定済み形式言語仕様に対応する、前記鉄道路線上を運行する列車の要件を表す列車要件を生成する生成部、
前記列車設定済み形式言語仕様が、前記列車要件を満たすかを検証する検証部とを有することを特徴とする連動仕様検証装置。
【請求項２】
前記列車要件種別が、少なくとも列車のデッドロック回避の要件種別を含むことを特徴とする請求項１に記載の連動仕様検証装置。
【請求項３】
前記記憶部は、さらに検証済みの前記列車設定済み形式言語仕様の検証結果、及び前記検証済みの前記列車設定済み形式言語仕様の検証結果から未検証の前記列車設定済み形式言語仕様の検証結果を推論するための推論規則を格納し、
前記設定部は、前記検証済みの前記列車設定済み形式言語仕様の検証結果を前記記憶部から取得し、前記推論規則に従って、前記検証済みの前記列車設定済み形式言語仕様の検証結果から前記未検証の前記列車設定済み形式言語仕様の検証結果を推論し、推論した前記検証結果を、前記記憶部に登録することを特徴とする請求項１または請求項２に記載の連動仕様検証装置。
【請求項４】
前記記憶部は、さらに検証済みの前記列車設定済み形式言語仕様の検証結果を格納し、
前記生成部は、前記記憶部に格納されている前記検証済みの前記列車設定済み形式言語仕様の検証結果に基づいて、前記列車要件種別から検証すべき要件種別を選別し、選別した前記列車要件種別に基づいて、前記列車設定済み形式言語仕様に対応する前記列車要件を生成することを特徴とする請求項１または請求項２に記載の連動仕様検証装置。
【請求項５】
前記設定部は、前記列車運行に関する条件である列車運行条件を受け付け、前記列車運行が、受け付けた前記列車運行条件を満たす場合に、前記列車運行を設定した前記列車設定済み形式言語仕様を出力することを特徴とする請求項１〜４のいずれか１項に記載の連動仕様検証装置。
【請求項６】
前記記憶部が、前記連動図表と前記形式言語仕様との変換情報を格納し、
前記検証済みの列車設定済み形式言語仕様の検証結果のうち、前記列車要件を満たさない検証結果は、前記列車要件を満たさない状況に達するまでの前記列車設定済み形式言語仕様の動作系列を表す反例を含み、
前記検証済みの列車設定済み形式言語仕様の検証結果から、前記反例を取得し、前記記憶部に格納されている前記変換情報に基づいて、前記反例を、前記連動図表の動作系列に変換し、前記動作系列に基づく動作を、前記連動図表上で実行した結果を出力する反例逆変換表示部を有することを特徴とする請求項１〜５のいずれか１項に記載の連動仕様検証装置。
【請求項７】
鉄道路線に設置される連動装置の仕様を表す連動仕様を検証する連動仕様検証装置における連動仕様検証方法であって、前記連動仕様検証装置は、前記連動仕様、及び鉄道保安のための列車に関する要件種別である列車要件種別を格納する記憶部を有し、
前記連動仕様を、前記鉄道路線上を運行する列車の在線位置を表わす、グラフ形式の形式言語仕様に変換し、
前記形式言語仕様に、前記鉄道路線上を運行する列車情報である列車運行を設定した列車設定済み形式言語仕様を出力し、
前記記憶部に格納されている前記列車要件種別に基づいて、前記列車設定済み形式言語仕様に対応する、前記鉄道路線上を運行する列車の要件を表す列車要件を生成し、
前記列車設定済み形式言語仕様が、前記列車要件を満たすかを検証することを特徴とする連動仕様検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、鉄道保安装置の一種である連動装置の連動仕様を規定する連動図表の検証技術に関し、特に、連動図表に従って列車制御を行った場合の、列車の安全性を事前に検証する技術に関する。
【背景技術】
【０００２】
連動装置とは、鉄道保安機能を有する装置であり、列車が安全に運行できるように、信号機や転てつ器などの設備を、所定の関係を保ちながら制御する。このように、所定の関係を保ちながら設備を動作させることを連動という。中でも、連動関係にある一方の設備が、他方の設備の動作を制限することを、鎖錠と呼ぶ。最も簡単な鎖錠の例は、信号機とその進路上の転てつ器の例であり、転てつ器がその進路を構成する向きに転換できない場合は、信号機の現示を進行現示に制御できないように鎖錠する。仮に、進路を構成せずに信号機を進行現示にしてしまうと、列車は脱線するか、想定外の場所に進入してしまう。
【０００３】
連動装置は、このような連動関係を保持するための装置であり、連動装置の仕様の誤りは、重大事故に繋がる恐れがある。そこで従来から、連動装置の連動仕様や、実装した連動装置そのものの挙動を事前に検証する技術がある。
【０００４】
連動装置の仕様は、連動仕様と呼ばれる。連動仕様は、連動図表と呼ばれる形式で記述する。連動図表は、配線略図と連動表から構成される。
【０００５】
特許文献１では、連動装置の連動仕様を、数学的な理論に基づく検証手法である形式的検証手法を用いて検証する方法を開示している。形式的検証手法を用いることで、連動仕様で規定されたいかなる連動が行われた場合でも、信号機や転てつ器などの設備が、鉄道保安に関する所定の要件を満たすか否かを検証できる。
【０００６】
また、特許文献２では、特許文献１の方法を拡張し、信号機や転てつ器などの設備を操作するてこ取り扱い者がいかなる操作を行った場合でも、それらの設備が、鉄道保安に関する要件を満たすかを検証する方法を開示している。
【０００７】
同様に、特許文献３では、特許文献１の方法を拡張し、予め進路設定した列車が運行する場合でも、信号機や転てつ器などの設備が、鉄道保安に関わる要件を満たすかを検証する方法を開示している。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開平１０−１６７７６号公報
【特許文献２】特開２０００−１２７９７１号公報
【特許文献３】特開２０００−１３７６２４号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
特許文献１、特許文献２、及び特許文献３が開示する検証方法は、連動仕様に従って設備が動作する場合に、設備が、鉄道保安のための設備の要件を満たすかを検証する方法である。鉄道保安とは、列車の衝突や脱線の防止などを指す。つまり、鉄道保安のための設備の要件とは、列車の衝突や脱線防止など、鉄道保安のための列車の要件を満たすために、設備が満たすべき要件である。
【００１０】
この鉄道保安のための設備の要件は、設備の設置位置や線路構成を記述した配線略図に依存する。しかし、配線略図は駅ごとに異なるため、鉄道保安のための設備の要件は、配線略図を参照しながら、駅ごとに人手で作成することになる。より詳細には、設備がどのような要件を満たせば、鉄道保安のための列車の要件を満たすか（列車の衝突や脱線が発生しないか）を、人が配線略図を参照しながら判断し、鉄道保安のための設備の要件を導出する必要がある。
【００１１】
このように従来技術では、鉄道保安のための設備の要件を人手で導出するため、誤りや、抜け漏れが生じないようにする必要がある。特に、複数路線の乗り入れがあるような駅の場合、配線略図は複雑になるため、誤りや、抜け漏れの防止への注意が要求される。したがって、人手作業に、多大な時間や人件費がかかるという問題が生じる。よって、鉄道保安のための設備の要件の誤りや抜け漏れを防止するとともに、鉄道保安の設備要件の作成の人手作業を削減することが課題となる。
【００１２】
また従来技術では、上述の通り、鉄道保安のための要件として設備の要件を作成し、検証するが、この方法では、鉄道保安の要件の１つである、列車のデッドロックについて検証することができない。列車のデッドロックとは、２本以上の列車が、お互いの在線位置の影響により停車を余儀なくされ、行き詰まりの状態になること指す。列車の衝突を回避するために停車し、デッドロック状態になることから、衝突事故の因子を含む危険な現象と言える。また、デッドロック状態から回復するためには、該当路線の列車運行を休止し、人手によって安全を確認して列車をバックさせる必要があるため、回復にかかる時間や列車運行休止のコストも少なくない。
【００１３】
このように、列車のデッドロック回避は、鉄道保安に関わる重要な要件と言えるが、設備の要件として表現することはできない。その理由を以下に説明する。
【００１４】
列車のデッドロック状態は、列車の進路に設定されたある信号機の内方に、当該列車が進入できなくなる状態である。列車の在線は軌道回路によって検知できるため、「ある軌道回路が落下した場合、対応する信号機はいずれ進行現示になる」という設備の要件が、デッドロック回避の要件を表している。しかし、仮にデッドロックが発生しない連動仕様を与えていたとしても、想定した進路と逆方向の進路を列車が走行した場合、軌道回路は落下するが、信号機は進行現示になるとは限らないため、デッドロック回避の要件としての前記設備の要件は満たさない。つまり、前記設備の要件は、デッドロック回避の要件の十分条件に過ぎない。
【００１５】
以上より、デッドロック回避の要件は設備の要件として表すことはできないため、従来技術では、列車のデッドロック回避を検証できないという問題がある。そこで、列車のデッドロック回避を検証できるようにすることが課題となる。
【００１６】
また、従来技術では、列車の運行計画から予め列車の進路や運行する本数を設定し、設定した範囲内で検証する。そのため、設定した範囲を超える進路・本数の列車を運行させた場合は、鉄道保安の要件を満たす保証はないという問題がある。つまり、連動仕様の正しさを保証するためには、あらゆる進路・本数の列車を運行させた場合（列車ダイヤに乱れがあるとき、その乱れを回復するときなど、列車の運行計画を超えて想定される範囲又はそれ以上の範囲で、進路・本数の列車を運行させた場合）について検証できるようにすることが課題となる。特に、デッドロック発生の有無は、運行する列車の本数に依存するため、設定を広げた進路・本数の列車を運行させた場合について検証すべきである。
【００１７】
さらに同様の理由から、従来技術では、鉄道保安の要件を満たさないような列車の進路・本数設定（以下、列車運行設定と呼ぶ）が存在した場合に、その列車運行設定を把握することができないという問題がある。特に、デッドロックについては、連動装置でデッドロックを回避するのではなく、この連動装置においてデッドロックが発生するような列車運行設定を把握し、そのような列車運行を行わないように、列車運行管理システム等の他の鉄道保安装置を設計する場合もある。つまり、連動仕様において、鉄道保安の要件を満たさない列車運行設定を網羅的に把握することは、連動装置以外の鉄道保安装置を設計する上での課題になる。
【００１８】
また、従来技術では、設定した列車運行設定範囲内では網羅的な検証を行うが、その際に、結果が明らかな検証や、結果が不要な（結果を使用しない）検証まで行うという問題がある。例えば、ある列車運行設定においてデッドロックが発生した場合は、その列車運行設定の任意の進路に運行する列車を追加した場合でも、デッドロックが発生することは明らかである。あるいは、ある列車運行設定において列車が衝突することが判明した場合、当該連動仕様に誤りがあり、修正を要することが判明しているため、他の列車運行設定や、デッドロックなどの他の要件について、当該連動仕様を検証する必要はない。
【００１９】
検証対象の連動仕様や、列車運行設定の規模にもよるが、検証には一定の時間がかかるため、これらの無駄な検証を行うことによる時間の損失は無視できない。
【００２０】
よって、結果が明らかな検証や、結果が不要な検証を検証前に判別し、それらの無駄な検証を行わないようにすることが課題となる。
【００２１】
本発明の目的は、これらの課題に対処し、連動仕様が鉄道保安の要件、特にデッドロック回避の要件を満たすかを、誤りや抜け漏れなく網羅的に検証するための、人手作業を削減する技術を提供することである。
【課題を解決するための手段】
【００２２】
そのため、本発明は、鉄道路線に設置される連動装置の仕様を表す連動仕様を検証する連動仕様検証装置であって、連動仕様、及び鉄道保安のための列車に関する要件種別である列車要件種別を記憶し、連動仕様を、鉄道路線上を運行する列車の在線位置を表わす、グラフ形式の形式言語仕様に変換する変換部、形式言語仕様に、鉄道路線上を運行する列車情報である列車運行設定を追加して列車設定済み形式言語仕様を得る設定部、列車要件種別に基づいて、列車設定済み形式言語仕様に対応する、鉄道路線上を運行する列車の要件を表す列車要件を生成する生成部、及び形式言語仕様のグラフ構成に関する性質として作成し、列車設定済み形式言語仕様が、列車要件を満たすかを検証する検証部とを有する。
【発明の効果】
【００２３】
本発明の一形態によれば、連動仕様が、列車のデッドロック回避を初めとする鉄道保安のための列車の要件を満たすことを、各列車運行の設定について、効率的に検証できると同時に、鉄道保安のための列車の要件を満たさないような列車運行の設定を、効率的に把握できる。
【図面の簡単な説明】
【００２４】
【図１】連動仕様検証装置の構成例を示すブロック図である。
【図２】連動仕様検証装置のハードウェア構成例を示す図である。
【図３】連動仕様検証装置の入力となる連動図表の構成要素である、配線略図の例を示す図である。
【図４】連動仕様検証装置の入力となる連動図表の構成要素である、連動表の例を示す図である。
【図５】連動図表変換部が作成する列車未設定形式仕様の、グラフデータの例を示す図である。
【図６】形式仕様保持部が保持する列車設定済み形式仕様の、グラフデータの例を示す図である。
【図７】本発明の実施の一形態の形式仕様保持部が保持する列車設定済み形式仕様の、変数データの例を示す図である。
【図８】列車要件保持部が保持する、列車要件のデータの例を示す図である。
【図９】変換情報保持部が保持する、連動図表変換情報のデータの例を示す図である。
【図１０】形式検証結果保持部が保持する、形式検証結果のデータの例を示す図である。
【図１１】列車運行設定部、列車要件生成部、及び形式検証部によって、列車設定済み形式仕様の検証の手順例を示すフローチャートである。
【図１２】本発明の実施の一形態の列車運行設定部によって、列車未設定形式仕様に列車運行情報を設定する手順例を示すフローチャートである。
【図１３】列車要件生成部によって、列車要件を生成する手順例を示すフローチャートである。
【図１４】反例逆変換・表示部によって、形式検証結果を画面出力する手順例を示すフローチャートである。
【発明を実施するための形態】
【００２５】
連動仕様検証装置は、連動仕様が、鉄道保安のための要件を満たすかを検証する装置である。本実施形態の連動仕様検証装置は、配線略図と連動表とで構成される連動図表によって連動仕様を記述し、この連動仕様に従った連動装置を用いて列車の制御を行った場合に、列車が、衝突の回避、脱線の回避、及びデッドロックの回避といった、鉄道保安のための列車の要件を満たすかを検証する装置である。
【００２６】
本実施形態の連動仕様検証装置は、連動仕様を、列車の在線位置を表わす形式言語仕様に変換する。この形式言語仕様に、鉄道路線上を運行する列車情報である列車運行を設定した列車設定済み形式言語仕様を出力する。列車設定済み形式言語仕様は、列車の在線位置を表す仕様上に列車を在線させたものとなる。一方、鉄道保安のための列車要件種別に基づいて、列車設定済み形式言語仕様に対応する、列車の要件を表す列車要件を生成し、列車設定済み形式言語仕様が列車要件を満たすかを検証する。
【００２７】
このように、従来の連動仕様検証装置が、連動仕様から得られる設備仕様と列車要件を基にして人手で生成する設備要件とを対比して検証するのに対して、本実施形態の連動仕様検証装置は、連動仕様と列車運行から列車仕様（列車設定済み形式言語仕様）を得て、この列車仕様と列車要件とを対比して検証する。
【００２８】
以下、図面を参照しながら詳細に説明する。図１は、本実施形態の連動仕様検証装置２０１の構成例を示すブロック図である。連動仕様検証装置２０１は、入力部１０１、連動図表保持部１０２、連動図表変換部１０３、変換情報保持部１０４、推論規則保持部１１４、列車運行設定部１０５、列車要件生成部１０６、形式仕様保持部１０７、列車要件保持部１０８、列車要件種別保持部１０９、形式検証部１１０、形式検証結果保持部１１１、反例逆変換・表示部１１２、出力部１１３を含む。
【００２９】
入力部１０１は、検証対象となる連動図表の入力を受け付け、入力した連動図表を連動図表保持部１０２に登録する。
【００３０】
連動図表変換部１０３は、連動図表保持部１０２から連動図表を取得し、取得した連動図表を列車未設定形式仕様に変換すると共に、連動図表変換情報を作成する。そして、変換した列車未設定形式仕様は列車運行設定部１０５へ出力し、作成した連動図表変換情報は変換情報保持部１０４に登録する。
【００３１】
列車運行設定部１０５は、連動図表変換部１０３から列車未設定形式仕様を取得する。取得した列車未設定形式仕様に対して、未検証の列車運行（列車の進路や運行する列車本数）を設定し、列車設定済み形式仕様を作成する。作成した列車設定済み形式仕様は、形式仕様保持部１０７に登録する。登録した列車設定済み形式仕様は、形式検証部１１０によって検証され、その形式検証結果は形式検証結果保持部１１１に登録される。その後、列車運行設定部１０５は、形式検証結果保持部１１１から形式検証結果を、推論規則保持部１１４から検証結果推論のための推論規則を取得し、取得した形式検証結果及び推論規則に基づいて、列車未設定形式仕様に未検証の列車運行を設定した列車設定済み形式仕様の形式検証結果を推論する。得られた形式検証結果は、形式検証結果保持部１１１に登録する。さらに、未検証の列車運行があれば、列車未設定形式仕様に、未検証の列車運行を設定し、列車設定済み形式仕様を作成して、形式仕様保持部１０７に登録する。
【００３２】
列車要件生成部１０６は、列車要件種別保持部１０９から列車要件種別を、形式仕様保持部１０７から列車設定済み形式仕様を、変換情報保持部１０４から連動図変換情報を、形式検証結果保持部１１１から形式検証結果をそれぞれ取得する。列車要件種別は、例えば「列車衝突の回避」「列車脱線の回避」「列車デッドロックの回避」など、鉄道保安のための列車の要件種別である。さらに列車要件生成部１０６は、取得した列車設定済み形式仕様に対応する、列車要件種別の示す種別で、未検証の、列車要件を作成する。列車要件種別を、列車設定済み形式仕様に対応する列車要件に具体化する際に、連動図表変換情報を使用する。同様に、未検証の列車要件を選別する際に、取得した形式検証結果を使用する。作成した列車要件は、列車設定済み形式仕様の識別子などと対応付けて、列車要件保持部１０８に登録する。
【００３３】
形式検証部１１０は、形式仕様保持部１０７から列車設定済み形式仕様を、列車要件保持部１０８から列車設定済み形式仕様に対応する列車要件を取得する。そして、列車設定済み形式仕様が、列車要件を満たすかを検証し、その検証結果を形式検証結果保持部１１１に登録する。
【００３４】
列車運行設定部１０５、列車要件生成部１０６、及び形式検証部１１０の詳細な手順は、図１１、図１２、及び図１３を使って後述する。
【００３５】
反例逆変換・表示部１１２は、形式検証結果保持部１１１から形式検証結果を、連動図表保持部１０２から連動図表を、変換情報保持部１０４から連動図表変換情報を取得する。さらに反例逆変換・表示部１１２は、連動図表変換情報に基づいて、形式検証結果に含まれる反例(鉄道保安を否定する具体例)を、連動図表上の動作系列(動作の時系列、又は動作による状態遷移の系列)に変換する。そして、変換によって得た動作系列を、連動図表上で実行し、列車の運行や設備の表示切り替えを、出力部１１３を介して画面に表示する。反例逆変換・表示部１１２の詳細な手順は、図１４を使って後述する。
【００３６】
出力部１１３は、反例逆変換部・表示部からの画面出力情報を取得し、画面表示を行う。
【００３７】
図２は、連動仕様検証装置２０１のハードウェア構成例を示す図である。
【００３８】
連動仕様検証装置２０１は、ＣＰＵ２０２、メモリ２０３、外部記憶装置２０４、表示装置２０５、入力装置２０６、及び外部媒体入出力装置２０７を備える。
【００３９】
ＣＰＵ２０２は、メモリ２０３に記憶されたプログラムを実行することによって、各種処理を実行する。メモリ２０３の一部は、ＣＰＵ２０２のワークエリアとして機能し、プログラム及びプログラムの実行に必要なデータを記憶する。具体的には、連動図表変換部１０３、列車運行設定部１０５、列車要件生成部１０６、形式検証部１１０、及び反例逆変換・表示部１１２を構成するプログラムが記憶されると共に連動図表保持部１０２、変換情報保持部１０４、推論規則保持部１１４、形式仕様保持部１０７、列車要件保持部１０８、及び形式検証結果保持部１１１の保持するデータが記憶される。
【００４０】
外部記憶装置２０４は、各種データを格納する。外部記憶装置２０４は、例えば、ハードディスク装置などである。具体的には、列車要件種別保持部１０９が格納される。
【００４１】
あるいは、連動図表変換部１０３、列車運行設定部１０５、列車要件生成部１０６、形式検証部１１０、及び反例逆変換・表示部１１２を構成するプログラムや、連動図表保持部１０２、変換情報保持部１０４、推論規則保持部１１４、形式仕様保持部１０７、列車要件保持部１０８、及び形式検証結果保持部１１１の保持するデータの少なくとも一部についても、外部記憶装置２０４に格納され、各種処理実行の際にＣＰＵ２０２がメモリ２０３へ読み出してプログラムを実行することとしてもよい。また各プログラムは、あらかじめ、メモリ２０３または外部記憶装置２０４に格納されていても良いし、必要に応じ、利用可能な媒体を介して、他の装置からメモリ２０３または外部記憶装置２０４に導入されてもよい。媒体とは、例えば、外部媒体入出力装置２０７に着脱可能な記憶媒体、または、ネットワークや、ネットワークを伝搬する搬送波やデジタル信号などの通信媒体を指す。
【００４２】
表示装置２０５は、プログラムの処理結果などを表示する。表示装置２０５は、例えば、ディスプレイなどである。入力装置２０６は、処理の実行指示及び処理に必要な情報の入力などを、連動仕様検証装置２０１の利用者から受け付ける。入力装置２０６は、例えば、キーボード及びマウスなどである。
【００４３】
外部媒体入出力装置２０７は、外部媒体と、外部記憶装置２０４に格納されているデータなどの入出力を行う。外部媒体は、外部媒体入出力装置２０７に着脱可能で可搬性のある記憶媒体であり、外部媒体出力装置２０７は、外部媒体に読み書き可能なドライブ装置などである。
【００４４】
図３は、連動仕様検証装置２０１の入力となる連動図表の構成要素である、配線略図の例を示す図である。
【００４５】
配線略図は、信号機と軌道回路、及び転てつ器の配置を示す。信号機３０１、３０２、３０５、３０９、３１３、３１８、３２０、及び３２１は設置された信号機を表す。同様に、軌道回路３０８、３０３、３０４、３０６、３０７、３１０、３１２、３１１、３１７、３１４、３１９、３１５、３１６は、線路上に設置された軌道回路を表す。また、軌道回路３０３、及び３１０は、両軌道回路上に転てつ器が設置されていることを表している。同様に、軌道回路３０６と軌道回路３１１上、軌道回路３１４上、軌道回路３１５上にも転てつ器が設置されている。配線略図の詳細な読み方は、菱沼好章著、「信号保安・鉄道通信入門」、中央書院、昭和63年3月、p.65-66に解説されている。
【００４６】
図４は、連動仕様検証装置２０１の入力となる連動図表の構成要素である、連動表の例を示す図である。
【００４７】
連動表４０１は、設備名称４０２、設備番号４０３、鎖錠４０４、信号制御又はてっ査鎖錠４０５、進路鎖錠４０６、及び接近又は保留鎖錠４０７を含む。
【００４８】
設備名称４０２は、設備の種別とその名称である。設備番号４０３は、設備を一意に識別するための識別番号である。鎖錠４０４は、信号機の開通方向を示しており、具体的には、信号機の示す進路を構成する転てつ器とその向きを示している。信号制御又はてっ査鎖錠４０５は、対象が信号機の場合、記入されている軌道回路上に列車が在線していると、この信号機は停止現示になることを示している。対象が転てつ器の場合、記入されている軌道回路上に列車が在線していると、この転てつ器は転換できないことを示している。進路鎖錠４０６は、記入されている軌道回路に列車が在線中は、その信号機の示す進路を保証し続けることを示す。接近又は保留鎖錠４０７は、信号機に一旦進行現示した後、記入されている軌道回路上に列車が在線している時に停止現示に変更した場合、接近している列車の安全のため、記入されている時分経過するまでは当該信号機の示す進路を保証し続けることを示す。連動表の詳細な読み方は、前述の菱沼好章著「信号保安・鉄道通信入門」で解説されている。
【００４９】
図５は、連動図表変換部１０３が作成する列車未設定形式仕様の、グラフデータの例を示す図である。
【００５０】
列車未設定形式仕様は、グラフデータと、軌道回路や転てつ器などの設備の状態や設定を表す変数データで構成される。
【００５１】
図５に示すグラフデータは、ノード５０１、５０２、５０７、５０９、５１１、５１２、５１６、５１８、５２３、５２６、５４０、５３２、５３４、５３６、及び５３９と、エッジ５０３、５０４、５０５、５０６、５０８、５１０、５１３、５１４、５１５、５１７、５１９、５２０、５２１、５２２、５２４、５２５、５２７、５２８、５２９、５３０、５３１、５３３、５３５、５３７、及び５３８を含む。
【００５２】
各ノードは、列車の在線可能な位置を表しており、例えば、ある列車が現在在線している現在ノードがノード５０２の場合は、その列車が軌道回路３０８上に在線していることを表す。１つのノードが表す在線位置は唯一であるが、複数のノードが同じ在線位置を表す場合はある。例えば、ノード５０１は、ノード５０２と同様に、列車が軌道回路３０８上に在線していることを表すノードである。
【００５３】
各エッジはノードからノードへの遷移を表しており、遷移のための遷移条件や、遷移する際に行う更新処理を付加情報として持つ。この遷移条件や、遷移する際に行う更新処理は、列車未設定形式仕様の構成要素である変数データに対する条件、及び更新処理である。また、これらの条件や更新処理は、連動表４０１から導出される。
【００５４】
例えば、列車が、軌道回路３０８から信号機３０１の内方軌道回路である軌道回路３０３へと進入するためには、連動表４０１の鎖錠４０４より、軌道回路３０３及び軌道回路３１０上の転てつ器が、定位方向でなければならない。よって、軌道回路３０８上の在線を表すノード５０２から、信号機３０１の内方軌道回路３０３上の在線を表すノード５０７への遷移を表すエッジ５０５の遷移条件は、軌道回路３０３及び軌道回路３１０上の転てつ器の方向変数が定位であるか、それらの転てつ器の鎖錠変数が解錠であるという条件になる。
【００５５】
また、連動表４０１の鎖錠４０４は、列車が信号機３０１の内方軌道回路である軌道回路３０３へ進入すると同時に、軌道回路３０３及び軌道回路３１０上の転てつ器を、転換できないように鎖錠することも意味している。よって、軌道回路３０８上の在線を表すノード５０２から、信号機３０１の内方軌道回路３０３上の在線を表すノード５０７への遷移を表すエッジ５０５の更新処理は、軌道回路３０３及び軌道回路３１０上の転てつ器の方向変数を定位に設定し、同転てつ器の鎖錠変数を鎖錠に設定する処理となる。
【００５６】
図６は、形式仕様保持部１０７が保持する列車設定済み形式仕様のグラフデータの例を示す図である。
【００５７】
図６に示す例は、図５の列車未設定形式仕様のグラフデータに対して、列車Ａ、及び列車Ｂの運行を設定した例である。列車Ａは軌道回路３０８から下り方面に運行する列車、列車Ｂは軌道回路３１６から上り方面に運行する列車である。
【００５８】
グラフ６０３、及びグラフ６０４は、図５に示した列車未設定形式仕様のグラフデータの例と一致する。ノード６０１及びノード６０６はグラフの初期ノードを表す。エッジ６０２及びエッジ６０５は、それぞれ初期ノード６０１または初期ノード６０６からの遷移を表す。
【００５９】
グラフ６０３、初期ノード６０１、及びエッジ６０２からなるグラフは、列車Ａの運行を表すグラフである。列車Ａの在線位置を表す現在ノードは、初期ノード６０１から開始し、エッジ６０２によってノード５０２に遷移する。これは、列車Ａがノード５０２に対応する軌道回路３０８上に配置され、運行を開始したことを表している。
【００６０】
同様に、グラフ６０４、初期ノード６０６、及びエッジ６０５からなるグラフは、列車Ｂの運行を表すグラフである。列車Ｂの在線位置を表す現在ノードは、初期ノード６０６から開始し、エッジ６０５によってノード５３９に遷移する。これは、列車Ｂがノード５３９に対応する軌道回路３１６上に配置され、運行を開始したことを表している。
【００６１】
図７は、形式仕様保持部１０７が保持する列車設定済み形式仕様の、変数データの例を示す図である。
【００６２】
列車設定済み形式仕様の変数データは、列車Ａ、列車Ｂにとって共通のデータである大域変数データ７０１と、それぞれ列車Ａ、列車Ｂの局所データである、列車Ａの局所変数データ７０４、列車Ｂの局所変数データ７０５を含む。
【００６３】
大域変数データ７０１は、転てつ器の状態データ７０２と、軌道回路の状態データ７０３を含む。転てつ器の状態データは、その方向と鎖錠に関する状態を持つ構造体である。
【００６４】
列車Ａの局所変数データ７０４は、列車Ａの時間変数７０６と、列車Ａの現在ノード及び前回ノードを表す位置変数７０７を含む。時間変数７０６は、接近又は保留鎖錠４０７に基づく遷移条件に使う変数で、時間変数が一定時間以内であれば遷移可能といった使い方をする。位置変数７０７は、前回ノードを表す前回ノード変数７０８と、現在ノードを表す現在ノード変数７０９を含む。これらの変数は、列車Ａの現在ノードや、前回ノードに関する要件を記述する際に使用する。
【００６５】
同様に、列車Ｂの局所変数データ７０５は、列車Ｂの時間変数７１０と、列車Ａの現在ノード、及び前回ノードを表す位置変数７１１を含む。さらに、位置変数７１１は、前回ノードを表す前回ノード変数７１２と、現在ノードを表す現在ノード変数７１３を含む。
【００６６】
図８は、列車要件保持部１０８が保持する、列車要件のデータの例を示す図である。
【００６７】
列車要件のデータ８０１は、脱線回避の要件８０２、衝突回避の要件８０３、及びデッドロック回避の要件８０４を含む。
【００６８】
脱線回避の要件８０２は、列車Ａ及び列車Ｂが脱線を回避するための要件で、列車Ａ及び列車Ｂが、転てつ器のある軌道回路上に在線しているならば、当該転てつ器は鎖錠中であるという要件を表している。
【００６９】
衝突回避の要件８０３は、列車Ａと列車Ｂの衝突を回避するための要件で、列車Ａと列車Ｂの在線位置が等しくなることはないという要件を表している。
【００７０】
デッドロック回避の要件８０４は、列車Ａ及び列車Ｂがデッドロック状態に陥ることを回避するための要件で、列車Ａ及び列車Ｂの在線位置が固定され、それ以上進めなくなることはないという要件を表している。列車の在線位置が固定される（即ちデッドロックする）とは、列車の在線位置を表すノードからなるグラフにおいて、現在ノードから隣接する他のあらゆるノードに遷移できない状況を意味する。ちなみに、列車Ａはノード５１２が、列車Ｂはノード５４０が終着ノードであるため、それぞれ現在ノードがノード５１２、ノード５４０の場合は、隣接する他のノードに遷移できなくともデッドロックとはみなさない。
【００７１】
図９は、変換情報保持部１０４が保持する、連動図表変換情報のデータの例を示す図である。
【００７２】
連動図表変換情報９０１は、連動図表識別子９０２、設備種別９０３、連動図表上の名称９０４、及び形式仕様上の名称９０５を含む。
【００７３】
連動図表識別子９０２は、連動図表を一意に特定するための識別子である。設備種別９０３は、連動図表に含まれる設備の設備種別を表す。連動図表上の名称９０４は、設備の連動図表における名称を表す。形式仕様上の名称９０５は、設備の形式仕様上の名称を表す。形式仕様上の名称９０５は、ノード名称９０６、及び変数名称９０７を含む。ノード名称９０６は、形式仕様のグラフデータにおいて、設備の設置位置を表すノード名称である。変数名称９０７は、形式仕様の変数データにおいて、設備の状態を表す変数名称である。例えば、軌道回路３０８の場合、連動図表上の名称９０４は下１Ｔであり、ノード名称９０６も下１Ｔである。さらに、軌道回路の状態を表す変数名称９０７は、ＴｒａｃｋＤ１Ｔである。また例えば、起動回路３０３及び軌道回路３１０上の転てつ器の場合、連動図表上の名称９０４は５１である。ノード名称９０６は５１イＴと５１ロＴであり、変数名称９０７は、Ｐｏｉｎｔ５１である。
【００７４】
図１０は、形式検証結果保持部１１１が保持する、形式検証結果のデータの例を示す図である。
【００７５】
形式検証結果１００１は、連動図表識別子１００２、列車設定済み形式仕様識別子１００３、列車要件種別１００４、列車運行設定１００５、検証結果１００６、及び反例１００７を含む。
【００７６】
連動図表識別子１００２は、連動図表及び列車未設定形式仕様を一意に特定するための識別子である。列車設定済み形式仕様識別子１００３は、列車設定済み形式仕様を一意に特定するための識別子である。１つの列車未設定形式仕様から、複数の異なる列車設定済み形式仕様を作成できるため、連動図表識別子１００２とは別に、列車設定済み形式仕様識別子１００３が必要になる。列車要件種別１００４は、列車要件種別保持部１０９が保持する列車要件種別と同様で、例えば、「列車衝突の回避」「列車脱線の回避」「列車デッドロックの回避」など、鉄道保安のための列車の要件種別である。列車運行設定１００５は、列車の運行開始位置や、その位置から運行開始する列車の本数など、列車の運行設定情報である。連動図表識別子１００２の示す列車未設定形式仕様に対して、列車運行設定１００５を設定すると、列車設定済み形式仕様識別子１００３の示す列車設定済み形式仕様が得られる。検証結果１００６は、列車設定済み形式仕様識別子１００３の示す列車設定済み形式仕様を、列車要件種別１００４の示す要件で検証した結果を示す。反例１００７は、検証結果１００６が要件を満たさない場合の反例（要件を満たさない場合のグラフノード遷移系列の例）を示す。
【００７７】
図１１は、列車運行設定部１０５、列車要件生成部１０６、及び形式検証部１１０によって、列車設定済み形式仕様の検証の手順例を示すフローチャートである。以下に示す処理は、連動仕様検証装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００７８】
ＣＰＵ２０２は、列車運行設定部１０５を実行することによって、連動図表変換部１０３から列車未設定形式仕様を取得する（ステップ１１０１）。
【００７９】
列車運行設定部１０５は、取得した列車未設定形式仕様に対する全形式検証結果を、形式検証結果保持部１１１から取得する（ステップ１１０２）。
【００８０】
列車運行設定部１０５は、取得した形式検証結果を参照し、未検証の列車運行設定があるかを確認する。例えば、図１０に示すような列車運行設定の場合は、あらゆる軌道回路を列車運行開始位置に指定し、あらゆる列車本数について検証結果が得られているかを確認する。検証結果が得られていない列車運行設定がある場合は、ステップ１１０４を実行する。全運行設定について検証結果が得られていた場合は、実行を終了する（ステップ１１０３）。
【００８１】
列車運行設定部１０５は、推論規則１１４保持部から検証結果推論のための推論規則を取得し、得られた形式検証結果を使って、未検証の列車運行設定に対する形式検証結果を推論する（ステップ１１０４）。推論規則は様々ある。例えば図１０に示すような列車運行設定であれば、ある列車運行設定においてデッドロックが発生した場合、その運行設定に列車運行開始位置や列車本数を追加した運行設定においても、デッドロックは発生すると推論できる。また、ある列車運行設定において列車が脱線する可能性がないと分かった場合、その運行設定に列車本数を追加した運行設定においても脱線する可能性はないと推論できる。ある列車運行開始位置から、連動図表中に表れる軌道回路の総数と等しい本数の列車を運行させ、デッドロックが生じなかった場合、同じ列車運行開始位置からそれ以上の本数の列車を運行させても、デッドロックは生じないと推論できる。これらの推論は、ステップ１１０２で取得した形式検証結果に基づいて行うため、形式検証結果によっては、未検証の列車運行設定に対する検証結果を推論できない場合がある。
【００８２】
列車運行設定部１０５は、ステップ１１０４において、未検証の列車運行設定に対する形式検証結果を推論できたらステップ１１０６を、推論できなかったらステップ１１０７を実行する（ステップ１１０５）。
【００８３】
列車運行設定部１０５は、ステップ１１０４の推論によって得た形式検証結果を、形式検証結果保持部１１１に登録する。その後、ステップ１１０２に戻って実行する（ステップ１１０６）。
【００８４】
列車運行設定部１０５は、未検証の列車運行設定を、ステップ１１０１で取得した列車未設定形式仕様に対して設定し、列車設定済み形式仕様を作成する。作成した列車設定済み形式仕様は、形式仕様保持部１０７に登録する（ステップ１１０７）。
【００８５】
列車運行設定部１０５によるステップ１１０１〜ステップ１１０７の手順は、図１２を使って詳細に説明する。
【００８６】
ＣＰＵ２０２は、列車要件生成部１０６を実行することによって、ステップ１１０７で作成した列車設定済み形式仕様に対する列車要件で、未検証の列車要件を作成する（ステップ１１０８）。
【００８７】
列車要件生成部１０６によるステップ１１０８の手順は、図１３を使って詳細に説明する。
【００８８】
ＣＰＵ２０２は、形式検証部１１０を実行することによって、ステップ１１０７で作成した列車設定済み形式仕様が、ステップ１１０８で作成した列車要件を満たすかを検証する（ステップ１１０９）。
【００８９】
形式検証部１１０は、ステップ１１０７の検証で得た形式検証結果を、形式検証結果保持部１１１に登録する。その後、ステップ１１０２に戻って実行する（ステップ１１１０）。
【００９０】
図１２は、列車運行設定部１０５によって、列車未設定形式仕様に列車運行情報を設定する手順例を示すフローチャートである。以下に示す処理は、連動仕様検証装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００９１】
ＣＰＵ２０２は、列車運行設定部１０５を実行することによって、連動図表変換部１０３から列車未設定形式仕様を取得する（ステップ１２０１）。
【００９２】
列車運行設定部１０５は、入力部１０１を介して列車運行条件を取得する（ステップ１２０２）。運行条件は、列車運行の条件で、列車運行設定に対する制約を与える。例えば、列車は特定の位置からのみ運行を開始するといった条件や、同位置から運行を開始する列車本数は高々１本であるなどの条件である。
【００９３】
列車運行設定部１０５は、ステップ１２０１で取得した列車未設定形式仕様に列車運行設定を行った列車設定済み形式仕様の全形式検証結果を、形式検証結果保持部１１１から取得する（ステップ１２０３）。
【００９４】
列車運行設定部１０５は、取得した形式検証結果に、脱線回避、あるいは衝突回避の要件がエラーとなる（要件を満たさない）検証結果が含まれるかを確認する。脱線回避、あるいは衝突回避の要件がエラーとなる検証結果が含まれる場合、実行を終了する。含まれない場合は、ステップ１２０５を実行する（ステップ１２０４）。
【００９５】
列車運行設定部１０５は、取得した形式仕様検証結果を参照し、未検証の列車運行設定があるかを確認する。検証結果が得られていない列車運行設定がある場合は、ステップ１２０６を実行する。全運行設定について検証結果が得られていた場合は、実行を終了する（ステップ１２０５）。
【００９６】
列車運行設定部１０５は、推論規則１１４保持部から検証結果推論のための推論規則を取得し、形式検証結果を使って、未検証の列車運行設定に対する形式検証結果を推論する（ステップ１２０６）。この推論は、ステップ１２０３で取得した形式検証結果に基づいて行うため、形式検証結果によっては、未検証の列車運行設定に対する検証結果を推論できない場合がある。
【００９７】
列車運行設定部１０５は、ステップ１２０６において、未検証の列車運行設定に対する形式検証結果を推論できたならステップ１２０８を、推論できなかったならステップ１２０９を実行する（ステップ１２０７）。
【００９８】
列車運行設定部１０５は、ステップ１２０６の推論によって得た形式検証結果を、形式検証結果保持部１１１に登録する。その後、ステップ１２０３に戻って実行する（ステップ１２０８）。
【００９９】
列車運行設定部１０５は、未検証の列車運行を、ステップ１２０１で取得した列車未設定形式仕様に対して設定し、列車設定済み形式仕様を作成する（ステップ１２０９）。
【０１００】
列車運行設定部１０５は、作成した列車設定済み形式仕様を、形式仕様保持部１０７に登録する（ステップ１２１０）。
【０１０１】
図１３は、列車要件生成部１０６によって、列車要件を生成する手順例を示すフローチャートである。以下に示す処理は、連動仕様検証装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１０２】
ＣＰＵ２０２は、列車要件生成部１０６を実行することによって、形式仕様保持部１０７から列車設定済み形式仕様を取得する（ステップ１３０１）。
【０１０３】
列車要件生成部１０６は、連動図表から列車設定済み形式仕様を作成した際の変換情報を、変換情報保持部１０４から取得する（ステップ１３０２）。
【０１０４】
列車要件生成部１０６は、ステップ１３０１で取得した列車設定済み形式仕様の全形式検証結果を、形式検証結果保持部１１１から取得する（ステップ１３０３）。
【０１０５】
列車要件生成部１０６は、列車要件種別保持部１０９から、列車要件種別を取得する（ステップ１３０４）。
【０１０６】
列車要件生成部１０６は、ステップ１３０３で取得した検証結果と、ステップ１３０４で取得した列車要件種別とを比較し、未検証の列車要件種別を抽出する。抽出した未検証の列車要件種別を、ステップ１３０２で取得した変換情報に基づいて、列車設定済み形式仕様に対する列車要件として具体化する（ステップ１３０５）。
【０１０７】
図１４は、反例逆変換・表示部１１２によって、形式検証結果を画面出力する手順例を示すフローチャートである。以下に示す処理は、連動仕様検証装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１０８】
ＣＰＵ２０２は、反例逆変換・表示部１１２によって、形式検証結果保持部１１１から、表示する検証結果を取得する（ステップ１４０１）。
【０１０９】
反例逆変換・表示部１１２は、連動図表保持部１０２から、ステップ１４０１で取得した検証結果の対象仕様である、連動図表を取得する（ステップ１４０２）。
【０１１０】
反例逆変換・表示部１１２は、変換情報保持部１０４から、ステップ１４０２で取得した連動図表の変換情報を取得する（ステップ１４０３）
反例逆変換・表示部１１２は、ステップ１４０３で取得した変換情報に基づき、ステップ１４０１で取得した検証結果に含まれる反例を、ステップ１４０３で取得した連動図表上の動作系列に逆変換する（ステップ１４０４）。
【０１１１】
反例逆変換・表示部１１２は、連動図表の配線略図を、出力部１１３を介して画面に表示する（ステップ１４０５）。
【０１１２】
反例逆変換・表示部１１２は、ステップ１４０５で表示した配線略図上にて、ステップ１４０４で作成した連動図表上の動作系列に基づき、列車の運行表示と配線略図の設備の表示切り替えを行う（ステップ１４０６）。
【０１１３】
以上のようにして、連動図表などで提供される連動仕様が、デッドロック回避を初めとする鉄道保安のための列車の要件を満たすことを、あらゆる列車運行設定について効率的に検証する手段と、逆に、鉄道保安のための列車の要件を満たさないような列車運行設定を効率的に検出する手段と、検出した反例（要件を満たさない場合の動作系列）を、連動図表上に視覚的に表示する手段とを有する動仕様検証装置を提供できる。連動仕様の設計者は、これらの手段を使って連動仕様を検証することで、連動仕様が鉄道保安の要件を満たすことを保証できるようになる、あるいは連動仕様が鉄道保安の要件を満たさないことを漏れなく検出し、その状況を確認できるようになる。そのため、鉄道保安のための列車の要件を満たす連動仕様を容易に作成できるようになる。
【０１１４】
本実施形態によれば、連動仕様が、鉄道保安のための列車の要件を満たすかを直接検証できるため、鉄道保安のための列車の要件から鉄道保安のための設備の要件を作成する必要がなくなる。その結果、誤りや抜け漏れなく鉄道保安の要件を検証できるようになるとともに、鉄道保安のための設備の要件を作成する手間を削減できる。
【０１１５】
また、本実施形態によれば、鉄道保安のための列車の要件の１つである、デッドロック回避を検証できるようになるため、デッドロック回避可能な連動仕様を作成できるようになる。あるいは同様の理由から、対象の連動仕様において、デッドロックが発生する列車運行設定を把握できるようになる。
【０１１６】
また、本実施形態によれば、ある一定数以上の形式検証結果が得られた場合、得られた形式検証結果に基づいて、その他のあらゆる未実施の形式検証の結果を推論できるようになるため、対象の連動仕様が鉄道保安のための要件、特にデッドロック回避を満たすことを、あらゆる列車運行設定について証明できるようになる。あるいは同様の理由から、対象の連動仕様において、鉄道保安の要件を満たさない、特にデッドロック回避を満たさない列車運行設定を、網羅的に把握できるようになる。
【０１１７】
また、本実施形態によれば、実施済みの形式検証結果に基づいて、未実施の検証の中から実施する必要のある検証を選別し、その未実施の形式検証の結果を推論できるようになる。また、設計者から受け付けた列車運行条件に反する列車運行設定は、検証対象から除外することができる。そのため、結果が明らかな検証や、結果が不要な検証など、無駄な検証の実施を回避できる。特に、列車衝突回避や列車脱線回避を満たさない連動仕様に対して、デッドロック回避の検証を行うことを回避できる。
【符号の説明】
【０１１８】
１０１：入力部、１０２：連動図表保持部、１０３：連動図表変換部、１０４：変換情報保持部、１０５：列車運行設定部、１０６：列車要件生成部、１０７：形式仕様保持部、１０８：列車要件保持部、１０９：列車要件種別保持部、１１０：形式検証部、１１１：形式検証結果保持部、１１２：反例逆変換・表示部、１１３：出力部。
【図１】
2011131812.tif 000003
【図２】
2011131812.tif 000004
【図３】
2011131812.tif 000005
【図４】
2011131812.tif 000006
【図５】
2011131812.tif 000007
【図６】
2011131812.tif 000008
【図７】
2011131812.tif 000009
【図８】
2011131812.tif 000010
【図９】
2011131812.tif 000011
【図１０】
2011131812.tif 000012
【図１１】
2011131812.tif 000013
【図１２】
2011131812.tif 000014
【図１３】
2011131812.tif 000015
【図１４】
2011131812.tif 000016