(57)【要約】【課題】並列実行される複数の実行パスの整合性評価に関する定量情報を出力する検証装置等を提供する。【解決手段】車両動作データ記憶手段２１は、車両３の動作データを記憶する。制御プログラムデータ記憶手段２２は、車載電子制御システム４の制御プログラムデータを記憶する。実動作時パターン抽出手段２３は、車両３の動作データを入力し、制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する。評価可能パターン抽出手段２４は、制御プログラムデータを入力し、モデル検査のツールを用いて制御プログラムデータに埋め込まれているアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、評価可能パターンを抽出する。評価網羅率算出手段２５は、評価可能パターンの総数及び実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する。【選択図】図３
2014016752.tif 000002
【特許請求の範囲】
【請求項１】
複数の実行パスが並行して動作する制御システムの制御プログラムを検証する検証装置であって、
前記制御システムによる制御対象の動作データを記憶する動作データ記憶手段と、
前記制御プログラム及び／又は前記制御プログラムに対応する制御モデルを含む制御プログラムデータを記憶する制御プログラムデータ記憶手段と、
前記動作データを入力し、前記制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する実動作時パターン抽出手段と、
前記制御プログラムデータを入力し、モデル検査のツールを用いて前記制御プログラムデータに埋め込まれている第１のアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する評価可能パターン抽出手段と、
前記評価可能パターンの総数及び前記実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する評価網羅率算出手段と、
を具備することを特徴とする検証装置。
【請求項２】
前記評価可能パターンの中で前記実動作時パターンではないものを評価漏れパターンとし、２以上の前記評価漏れパターンに共通して含まれる評価漏れコアパターンを抽出する評価漏れコアパターン抽出手段、
を更に具備することを特徴とする請求項１に記載の検証装置。
【請求項３】
前記評価漏れパターンに対して、前記モデル検査のツールを用いて前記第１のアサーションとは異なる第２のアサーションの反例を抽出し、前記評価漏れパターンの入力データを生成する評価漏れパターン入力データ生成手段、
を更に具備することを特徴とする請求項２に記載の検証装置。
【請求項４】
前記評価漏れコアパターン抽出手段は、前記評価漏れコアパターンの順位付けを行い、順位付け結果を出力する
ことを特徴とする請求項２又は請求項３に記載の検証装置。
【請求項５】
前記実動作時パターン抽出手段は、前記制御システムによる制御対象の動作環境を組合せパターンに含めて前記実動作時パターンを抽出し、
前記評価可能パターン抽出手段は、前記制御システムによる制御対象の動作環境を組合せパターンに含めて前記評価可能パターンを抽出する
ことを特徴とする請求項１乃至請求項４のいずれかに記載の検証装置。
【請求項６】
複数の実行パスが並行して動作する制御システムの制御プログラムを検証する検証方法であって、
前記制御システムによる制御対象の動作データと、前記制御プログラム及び／又は前記制御プログラムに対応する制御モデルを含む制御プログラムデータとを記憶するコンピュータが、
前記動作データを入力し、前記制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する実動作時パターン抽出ステップと、
前記制御プログラムデータを入力し、モデル検査のツールを用いて前記制御プログラムデータに埋め込まれている第１のアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する実行パス評価可能パターン抽出ステップと、
前記評価可能パターンの総数及び前記実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する評価網羅率算出ステップと、
を実行することを特徴とする検証方法。
【請求項７】
コンピュータを、複数の実行パスが並行して動作する制御システムの制御プログラムを検証する検証装置として機能させるための検証プログラムであって、
前記制御システムによる制御対象の動作データを記憶する動作データ記憶手段と、
前記制御プログラム及び／又は前記制御プログラムに対応する制御モデルを含む制御プログラムデータを記憶する制御プログラムデータ記憶手段と、
前記動作データを入力し、前記制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する実動作時パターン抽出手段と、
前記制御プログラムデータを入力し、モデル検査のツールを用いて前記制御プログラムデータに埋め込まれている第１のアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する評価可能パターン抽出手段と、
前記評価可能パターンの総数及び前記実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する評価網羅率算出手段と、
を具備する検証装置として機能させるための検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、制御システムの制御プログラムを検証する検証装置等に関するものである。
【背景技術】
【０００２】
近年、車載電子制御システムは、予防安全や快適性向上の高機能化が進んでいる。従って、各機能を実現する制御プログラムの信頼性を確認するために多大な時間を要するようになっている。制御システムの制御プログラムの信頼性を確認する手段としては、テストのカバレージ測定がある（特許文献１、２参照）。
【０００３】
特許文献１では、テスト対象の制御プログラムに含まれる実行パス中の関数について、入力値の範囲を特定し、入力範囲を所定の方法で分割した空間を用いてカバレージ（＝テストケースの網羅状況）を測定するカバレージ測定装置が開示されている。特許文献１のカバレージ測定装置によれば、実行パス中の関数の入出力に関して信頼性のあるカバレージ測定ができる。
【０００４】
特許文献２では、テスト対象の制御プログラムの実行パスからＦＳＭ（Finite
State Machine：制御モードとその遷移を表すモデル）を抽出し、テスト実行時のログ情報をもとに、ＦＳＭに基づいてカバレージを測定するカバレージ測定装置が開示されている。特許文献２のカバレージ測定装置は、テスト実施者の注目する変数（出力情報）に関連する実行パスのみを抽出したり、所定の機能に関するＦＳＭのみを抽出したりする「テスト対象絞込み制御部」を有する。テスト対象絞込み制御部によれば、不要なテストが行われていないことによるカバレージ測定の低値化を回避できる。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００９−３０１１２９号公報
【特許文献２】特開２００９−１８１５４９号公報
【非特許文献】
【０００６】
【非特許文献１】藤倉  俊幸著、「組み込みソフトへの数理的アプローチ」、CQ出版社、発行年：２０１２年４月１５日初版発行
【発明の概要】
【発明が解決しようとする課題】
【０００７】
しかしながら、特許文献１のカバレージ測定装置は、実行パス中の関数の入出力に着目したカバレージ評価を行っている。従って、複数の実行パスが並行して動作するシステムに特許文献１のカバレージ測定装置を適用した場合、カバレージ評価が１００％であっても、システム全体としての評価に重要な、実行パス間の組合せが全く網羅されていない事態が起こり得る。その結果、機能間の不整合要因を見逃してしまう可能性がある。
【０００８】
また、特許文献２のカバレージ測定装置は、注目変数ごとに実行パス、ＦＳＭを抽出するため、複数の注目変数に関する実行パスの組合せについては、カバレージ評価から除かれている。従って、複数の実行パスが並行して動作するシステムに特許文献２のカバレージ測定装置を適用した場合、カバレージ評価が１００％であっても、システム全体としての評価に重要な、実行パス間の組合せが全く網羅されていない事態が起こり得る。
【０００９】
尚、「複数の実行パスが並行して動作するシステム」とは、車載電子制御システムであれば、複数のＥＣＵ（Electronic Control Unit）が並行動作している場合や、単一のＥＣＵが複数の変数の値を同時に出力する場合などである。また、「複数の実行パスが並行して動作するシステム」には、自動車の制御システムに限らず、航空機、ロボット、人工衛星などの制御システムも含まれる。
【００１０】
本発明は、前述した問題点に鑑みてなされたものであり、その目的とすることは、並列実行される複数の実行パスの整合性評価に関する定量情報を出力する検証装置等を提供することである。
【課題を解決するための手段】
【００１１】
前述した目的を達成するための第１の発明は、複数の実行パスが並行して動作する制御システムの制御プログラムを検証する検証装置であって、前記制御システムによる制御対象の動作データを記憶する動作データ記憶手段と、前記制御プログラム及び／又は前記制御プログラムに対応する制御モデルを含む制御プログラムデータを記憶する制御プログラムデータ記憶手段と、前記動作データを入力し、前記制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する実動作時パターン抽出手段と、前記制御プログラムデータを入力し、モデル検査のツールを用いて前記制御プログラムデータに埋め込まれている第１のアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する評価可能パターン抽出手段と、前記評価可能パターンの総数及び前記実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する評価網羅率算出手段と、を具備することを特徴とする検証装置である。第１の発明によって、並列実行される複数の実行パスの整合性評価に関する定量情報として、２以上の注目変数の整合性評価に関する評価網羅率を出力することができる。
【００１２】
第１の発明は、前記評価可能パターンの中で前記実動作時パターンではないものを評価漏れパターンとし、２以上の前記評価漏れパターンに共通して含まれる評価漏れコアパターンを抽出する評価漏れコアパターン抽出手段、を更に具備しても良い。これによって、評価漏れコアパターンを把握できるので、制御プログラムの検証を効率的に行うことができる。
【００１３】
また、第１の発明は、前記評価漏れパターンに対して、前記モデル検査のツールを用いて前記第１のアサーションとは異なる第２のアサーションの反例を抽出し、前記評価漏れパターンの入力データを生成する評価漏れパターン入力データ生成手段、を更に具備しても良い。これによって、評価漏れパターンの評価に必要な入力データが自動的に生成されるので、制御プログラムの検証を効率的に行うことができる。
【００１４】
また、第１の発明における前記評価漏れコアパターン抽出手段は、前記評価漏れコアパターンの順位付けを行い、順位付け結果を出力しても良い。これによって、評価漏れコアパターンの順位付けを把握することができる。従って、評価漏れ度合いが大きいパターンを容易に確認することができるので、制御プログラムの検証を効率的に行うことができる。
【００１５】
また、第１の発明における前記実動作時パターン抽出手段は、前記制御システムによる制御対象の動作環境を組合せパターンに含めて前記実動作時パターンを抽出し、前記評価可能パターン抽出手段は、前記制御システムによる制御対象の動作環境を組合せパターンに含めて前記評価可能パターンを抽出するようにしても良い。これによって、異なる複数の動作環境における評価網羅率を算出し、把握することができるので、制御プログラムの信頼性を向上することができる。
【００１６】
第２の発明は、複数の実行パスが並行して動作する制御システムの制御プログラムを検証する検証方法であって、前記制御システムによる制御対象の動作データと、前記制御プログラム及び／又は前記制御プログラムに対応する制御モデルを含む制御プログラムデータとを記憶するコンピュータが、前記動作データを入力し、前記制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する実動作時パターン抽出ステップと、前記制御プログラムデータを入力し、モデル検査のツールを用いて前記制御プログラムデータに埋め込まれている第１のアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する実行パス評価可能パターン抽出ステップと、前記評価可能パターンの総数及び前記実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する評価網羅率算出ステップと、を実行することを特徴とする検証方法である。第２の発明によって、並列実行される複数の実行パスの整合性評価に関する定量情報として、２以上の注目変数の整合性評価に関する評価網羅率を出力することができる。
【００１７】
第３の発明は、コンピュータを、複数の実行パスが並行して動作する制御システムの制御プログラムを検証する検証装置として機能させるための検証プログラムであって、前記制御システムによる制御対象の動作データを記憶する動作データ記憶手段と、前記制御プログラム及び／又は前記制御プログラムに対応する制御モデルを含む制御プログラムデータを記憶する制御プログラムデータ記憶手段と、前記動作データを入力し、前記制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する実動作時パターン抽出手段と、前記制御プログラムデータを入力し、モデル検査のツールを用いて前記制御プログラムデータに埋め込まれている第１のアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する評価可能パターン抽出手段と、前記評価可能パターンの総数及び前記実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する評価網羅率算出手段と、を具備する検証装置として機能させるための検証プログラムである。第３の発明の検証プログラムを汎用のコンピュータにインストールすることによって、第１の発明の検証装置を得ることができ、更に、第２の発明の検証方法を実行することができる。
【発明の効果】
【００１８】
本発明により、並列実行される複数の実行パスの整合性評価に関する定量情報を出力する検証装置等を提供することができる。
【図面の簡単な説明】
【００１９】
【図１】検証システムの概要を示す図
【図２】検証装置のハードウエア構成図
【図３】検証装置の機能構成図
【図４】並列実行される複数の実行パスの一例を示す図
【図５】評価可能パターン抽出処理のためのコード追加の一例を示す図
【図６】注目変数と実行パスの対応関係を示す図
【図７】評価可能パターンの一例を示す図
【図８】評価済パターンの一例を示す図
【図９】３つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図（１）
【図１０】３つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図（２）
【図１１】３つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図（３）
【図１２】２つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図（１）
【図１３】２つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図（２）
【図１４】入力データ生成処理のためのコード追加の一例を示す図
【図１５】動作環境を含む評価可能パターン抽出処理のためのコード追加の一例を示す図
【図１６】検証装置による検証処理の流れを示すフローチャート
【発明を実施するための形態】
【００２０】
以下図面に基づいて、本発明の実施形態を詳細に説明する。
図１は、検証システムの概要を示す図である。図１に示すように、検証システム１は、検証装置２と車両３とから構成される。車両３には、検証対象となる車載電子制御システム４が搭載される。車載電子制御システム４には、データロガー装置５が設けられる。
【００２１】
車載電子制御システム４は、複数の実行パスが並行して動作する制御システムである。車載電子制御システム４では、複数のＥＣＵが並行動作したり、単一のＥＣＵが複数の変数の値を同時に出力したりする。
【００２２】
データロガー装置５は、車両３の動作データ（走行データ）を記録する。データロガー装置５は、無線又は有線の通信手段によって、車両３の動作データを検証装置２に送信する。
【００２３】
検証装置２は、データロガー装置５から送信される車両３の動作データに基づいて、車載電子制御システム４の制御プログラムを検証する。特に、検証装置２は、並列実行される複数の実行パスの整合性評価に関する定量情報を出力する。
【００２４】
尚、図１では、単一の車両３のみを図示したが、検証システム１には、複数の車両３を含めても良い。例えば、検証装置２は、同一の制御プログラムに従う車載電子制御システム４を同一の検証対象とし、複数のデータロガー装置５から複数の車両３の動作データを受信しても良い。
【００２５】
図２は、検証装置のハードウエア構成図である。尚、図２のハードウエア構成は一例であり、用途、目的に応じて様々な構成を採ることが可能である。
【００２６】
図２に示すように、検証装置２は、制御部１１、記憶部１２、メディア入出力部１３、通信制御部１４、入力部１５、表示部１６、周辺機器Ｉ／Ｆ部１７等が、バス１８を介して接続される。
【００２７】
制御部１１は、ＣＰＵ（Central Processing Unit）、ＲＯＭ（Read Only Memory）、ＲＡＭ（Random Access Memory）等によって構成される。
【００２８】
ＣＰＵは、記憶部１２、ＲＯＭ、記録媒体等に格納されるプログラムをＲＡＭ上のワークメモリ領域に呼び出して実行し、バス１８を介して接続された各装置を駆動制御し、検証装置２が行う後述する処理を実現する。ＲＯＭは、不揮発性メモリであり、コンピュータのブートプログラムやＢＩＯＳ等のプログラム、データ等を恒久的に保持している。ＲＡＭは、揮発性メモリであり、記憶部１２、ＲＯＭ、記録媒体等からロードしたプログラム、データ等を一時的に保持するとともに、制御部１１が各種処理を行う為に使用するワークエリアを備える。
【００２９】
記憶部１２は、ＨＤＤ（Hard Disk Drive）等であり、制御部１１が実行するプログラム、プログラム実行に必要なデータ、ＯＳ（Operating System）等が格納される。プログラムに関しては、ＯＳに相当する制御プログラムや、後述する処理をコンピュータに実行させるためのアプリケーションプログラムが格納されている。これらの各プログラムコードは、制御部１１により必要に応じて読み出されてＲＡＭに移され、ＣＰＵに読み出されて各種の手段として実行される。
【００３０】
メディア入出力部１３（ドライブ装置）は、データの入出力を行い、例えば、ＣＤドライブ（−ＲＯＭ、−Ｒ、−ＲＷ等）、ＤＶＤドライブ（−ＲＯＭ、−Ｒ、−ＲＷ等）等のメディア入出力装置を有する。通信制御部１４は、通信制御装置、通信ポート等を有し、コンピュータとネットワーク間の通信を媒介する通信インタフェースであり、ネットワークを介して、他のコンピュータ間との通信制御を行う。ネットワークは、有線、無線を問わない。
【００３１】
入力部１５は、データの入力を行い、例えば、キーボード、マウス等のポインティングデバイス、テンキー等の入力装置を有する。入力部１５を介して、コンピュータに対して、操作指示、動作指示、データ入力等を行うことができる。表示部１６は、液晶パネル等のディスプレイ装置、ディスプレイ装置と連携してコンピュータのビデオ機能を実現するための論理回路等（ビデオアダプタ等）を有する。尚、入力部１５及び表示部１６は、タッチパネルディスプレイのように、一体となっていても良い。
【００３２】
周辺機器Ｉ／Ｆ（Interface）部１７は、コンピュータに周辺機器を接続させるためのポートであり、周辺機器Ｉ／Ｆ部１７を介してコンピュータは周辺機器とのデータの送受信を行う。周辺機器Ｉ／Ｆ部１７は、ＵＳＢ（Universal Serial Bus）やＩＥＥＥ１３９４やＲＳ−２３２Ｃ等によって構成されており、通常複数の周辺機器Ｉ／Ｆを有する。周辺機器との接続形態は有線、無線を問わない。バス１８は、各装置間の制御信号、データ信号等の授受を媒介する経路である。
【００３３】
図３は、検証装置の機能構成図である。検証装置２の記憶部１２には、図３に示す各種の手段を実現するためのプログラムがインストールされている。検証装置２の制御部１１は、これらのプログラムを読み出して実行することによって、各種の手段として機能する。以下では、便宜上、各種の手段を文章の主語として記載する場合があるが、実際には、制御部１１が動作の主体である。
【００３４】
図３に示すように、検証装置２は、車両動作データ記憶手段２１、制御プログラムデータ記憶手段２２、実動作時パターン抽出手段２３、評価可能パターン抽出手段２４、評価網羅率算出手段２５、評価漏れコアパターン抽出手段２６、評価漏れパターン入力データ生成手段２７等の機能を備える。
【００３５】
車両動作データ記憶手段２１は、データロガー装置５から送信される車両３の動作データを記憶部１２に記憶する。車両３の動作データは、例えば、車両３に搭載されるセンサが取得するセンシングデータ、車両３に搭載されるアクチュエータへの指令値や制御モード等に関わる情報である。例えば、オートクルーズ機能の制御モードに関わる情報は、加速モードや減速モード等のモード種別等である。
【００３６】
制御プログラムデータ記憶手段２２は、車載電子制御システム４の制御プログラム及び／又は制御プログラムに対応する制御モデルを含む制御プログラムデータを記憶する。
【００３７】
制御プログラムは、例えば、車載電子制御システム４の制御ロジックが高級言語によって記述されたソースコードである。高級言語とは、人間にとって分かり易い言語を意味し、例えば、Ｃ言語である。
【００３８】
制御モデルは、車載電子制御システム４の制御プログラムと完全に対応するものである。制御モデルは、例えば、車載電子制御システム４の制御ロジックを示すブロック線図モデルや車載電子制御システム４の状態遷移を示す状態遷チャート等である。ブロック線図モデルや状態遷移チャート等を作成するためのソフトウエアの一例としては、ＭＡＴＬＡＢ（MathWorks社）環境によって提供されるSimulinkがある。Simulinkでは、Simulink上で作成したブロック線図モデルから、Ｃ言語のソースコードを自動生成することが可能である。
【００３９】
以下、制御プログラムデータは、制御プログラムと制御モデルを総称する用語として用いる。後述する各種の手段は、処理対象として、制御プログラムを用いても良いし、制御モデルを用いても良い。
【００４０】
実動作時パターン抽出手段２３は、車両３の動作データを入力し、制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する。
【００４１】
注目変数における「変数」とは、車両３に搭載されるアクチュエータへの指令値や制御モード等を格納するプログラム内部の変数又はプログラム内部の変数に対応する制御モデル上の変数を意味する。本発明の特徴の一つは、２以上の注目変数に関する実行パスの整合性評価を行うことである。
【００４２】
「実行パス」とは、車両３の機能が、外部からデータを入力し、外部にデータを出力するまでの一連の制御フローを意味する。機能は、１又は複数のＥＣＵによって実現されるものであっても良いし、単一のＥＣＵに含まれる１又は複数の関数によって実現されるものであっても良い。つまり、本発明は、機能の粒度に関わらず、適用可能である。
【００４３】
図４は、並列実行される複数の実行パスの一例を示す図である。図４における「Ｓ１」〜「Ｓ１０」は、車載電子制御システム４の制御命令を模式的に示したものである。また、図４における太線の矢印は、注目変数に関する実行パスを示したものである。これらは、他の図面においても同様である。
【００４４】
図４に示す例では、注目変数が、変数Ａと変数Ｂの２つである。実行パスＡ１は、変数Ａに関する実行パスの一つである。同様に、実行パスＡ２も、変数Ａに関する実行パスの一つである。例えば、変数Ａの取り得る値が「ａ１」と「ａ２」とする。実行パスＡ１は、一連の制御フローの終了時点において、変数Ａが「ａ１」の値を取る実行パスである。また、実行パスＡ２は、一連の制御フローの終了時点において、変数Ａが「ａ２」の値を取る実行パスである。実行パスＢ１及び実行パスＢ２も同様である。
【００４５】
実動作時パターン抽出手段２３は、車両３の動作データに基づいて、制御設計者の注目変数に関する実車評価時の実行パスの組合せパターンを抽出する。以下、実車評価時の実行パスの組合せパターンのことを「実動作時パターン」と略称する。図４に示す例であれば、実動作時パターンの一例は、「Ａ１、Ｂ１」等である。実動作時パターンが「Ａ１、Ｂ１」ということは、車両３が、ある時点において、実行パスＡ１と実行パスＢ１の両方を実行した状態になったことを意味する。ここで、実行順は特に区別しない。つまり、実行パスＡ１が先に実行された場合も、実行パスＢ１が先に実行された場合も、同様に扱えば良い。
【００４６】
例えば、車載電子制御システム４の制御プログラム中に、実行パスを区別できるようなフラグ変数を埋め込んでおき、車両動作データ記憶手段２１が、フラグ変数の情報も記憶する。実動作時パターン抽出手段２３は、車両動作データ記憶手段２１によって記憶されるフラグ変数の情報から、実動作時パターンを抽出する。
【００４７】
また、例えば、車載電子制御システム４の制御プログラム中に陽にフラグ変数を埋め込むことに代えて、実動作時パターン抽出手段２３は、車両動作データ記憶手段２１によって記憶される他のデータ（＝センシングデータや、注目変数及び注目変数と異なる変数の値等）から実行パスを推定し、実動作時パターンを抽出しても良い。
【００４８】
実動作時パターン抽出手段２３によって抽出される実動作時パターンは、実車評価において評価済の実行パスの組合せパターンである。そして、ある実動作時パターンが成立したときに車両３に問題が発生していないと評価されたならば、その実動作時パターンでは車両３が安全であることが確認されたと言える。
【００４９】
図３の説明に戻る。評価可能パターン抽出手段２４は、制御プログラムデータを入力し、モデル検査のツールを用いて制御プログラムデータに埋め込まれているアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能な組合せパターン（以下、「評価可能パターン」と略称する。）を抽出する。
【００５０】
モデル検査とは、形式システムをアルゴリズム的に検証する手法である。モデル検査は、設計から抽出されたモデルが形式仕様を満足するかどうか検証する。モデル検査のツールの一例としては、ＣＢＭＣ（Bounded Model Checking for ANSI-C）等がある。ＣＭＢＣでは、プログラムをフラットな構造に展開して変数間の関係を漸化式にし、最終的には論理式にしてプログラムの検証を行う。
【００５１】
図５は、評価可能パターン抽出処理のためのコード追加の一例を示す図である。図５を参照しながら、モデル検査のツールを用いた評価可能パターン抽出処理を説明する。
【００５２】
図５では、図４に示す例に対して、評価可能パターン抽出処理のためのコードが追加されている。図５に示すように、追加コードは、（１）開始の直後に追加された「flag1=0」と「flag2=0」、（２）Ｓ７の制御命令の直前に追加された「flag1=1」、（３）Ｓ１０の制御命令の直前に追加された「flag2=1」、（４）終了の直前に追加された「assert(!(flag1==1 && flag2==1))、の４箇所である。ここで、「assert」は、アサーションと呼ばれるプログラミング言語の構文の一種であり、プログラムの前提条件を示すために使われる。アサーションは、プログラムのその箇所で必ず真であるべき式を記述する。
【００５３】
図５のようにコードを追加しておくことによって、モデル検査のツールを用いれば、「どんな入力パターンでもflag1とflag2の両方が１になることはない」というアサーションが真であるか否かを網羅的に検証することができる（非特許文献１のpp111-119参照）。例えば、検証結果が真であれば、どんな入力パターンに対しても実行パスの組合せパターンが「Ａ２、Ｂ２」になることはなく、「Ａ２、Ｂ２」が評価不能パターンであることが分かる。そして、評価可能パターン抽出手段２４は、評価不能パターンを除く実行パスの組合せパターンを、評価可能パターンとして抽出する。
【００５４】
図３の説明に戻る。評価網羅率算出手段２５は、評価可能パターンの総数及び実動作時パターンの総数に基づいて、２以上の注目変数の整合性評価に関する評価網羅率を算出する。ここで、実動作時パターンは、必ず評価可能パターンである。
【００５５】
以下、図６〜図１３を参照しながら、評価網羅率算出手段２５の詳細を説明する。図６〜図１３は、同一の制御プログラム及び同一の注目変数に対する例となっている。
【００５６】
図６は、注目変数と実行パスの対応関係を示す図である。図６に示すように、注目変数は、Ａ〜Ｄの４つである。例えば、注目変数Ａは、実行パスが「Ａ１」、「Ａ２」、「Ａ３」の３つである。
【００５７】
図７は、評価可能パターンの一例を示す図である。図７は、図６に示す注目変数と実行パスの対応関係を有する制御プログラムに対して、評価可能パターン抽出手段２４が評価可能パターンを抽出した結果を示している。例えば、Ｎｏが「１」の評価可能パターンは、「Ａ１、Ｂ１、Ｃ１、Ｄ１」である。
【００５８】
図８は、評価済パターンの一例を示す図である。図８は、図６に示す注目変数と実行パスの対応関係を有する制御プログラムに対して、実動作時パターン抽出手段２３が実動作時パターンを抽出した結果を示している。例えば、Ｎｏが「１」の評価可能パターン「Ａ１、Ｂ１、Ｃ１、Ｄ１」は、「○：評価済」であり、実動作時パターンに含まれていることを示している。
【００５９】
評価網羅率算出手段２５は、図７及び図８の結果に基づき、評価可能パターンの総数を分母とし、実動作時パターンの総数を分子とする、４つの注目変数（＝Ａ〜Ｄ）の整合性評価に関する評価網羅率を算出する。図７に示すように、評価可能パターンの総数は「２５」である。また、図８に示すように、実動作時パターンの総数は「１６」である。従って、評価網羅率算出手段２５は、４つの注目変数（＝Ａ〜Ｄ）の整合性評価に関する評価網羅率を、「１６／２５×１００＝６４％」と算出する。
【００６０】
図７及び図８に示す例では、評価網羅率算出手段２５は、４つの実行パスの組合せによる評価可能パターン及び評価済パターンに基づいて、４つの注目変数（＝Ａ〜Ｄ）の整合性評価に関する評価網羅率を算出している。つまり、評価網羅率算出手段２５は、注目変数と同じ数の実行パスの組合せから評価網羅率を算出している。以下では、評価網羅率算出手段２５が、注目変数よりも少ない数の実行パスの組合せから評価網羅率を算出する場合を説明する。
【００６１】
図９〜図１１は、３つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図である。図６に示す注目変数と実行パスの対応関係から、３つの実行パスの組合せパターンを列挙すると、図９〜図１１に示すように、総数が「８１」となる。この中で、評価可能パターン抽出手段２４によって評価可能パターンが抽出された結果が、列３１である。また、実動作時パターン抽出手段２３によって実動作時パターンが抽出された結果が、列３２である。
【００６２】
図９〜図１１に示すように、評価可能パターンの総数は「５８」である。また、図９〜図１１に示すように、実動作時パターンの総数は「４８」である。従って、評価網羅率算出手段２５は、４つの注目変数（＝Ａ〜Ｄ）の整合性評価に関する評価網羅率を、「４８／５８×１００≒８３％」と算出する。
【００６３】
図１２、図１３は、２つの実行パスの組合せによる評価可能パターン及び評価済パターンを示す図である。図６に示す注目変数と実行パスの対応関係から、２つの実行パスの組合せパターンを列挙すると、図１２、図１３に示すように、総数が「４５」となる。この中で、評価可能パターン抽出手段２４によって評価可能パターンが抽出された結果が、列３１である。また、実動作時パターン抽出手段２３によって実動作時パターンが抽出された結果が、列３２である。
【００６４】
図１２、図１３に示すように、評価可能パターンの総数は「４２」である。また、図１２、図１３に示すように、実動作時パターンの総数は「４１」である。従って、評価網羅率算出手段２５は、４つの注目変数（＝Ａ〜Ｄ）の整合性評価に関する評価網羅率を、「４１／４２×１００≒９８％」と算出する。
【００６５】
例えば、２変数の組合せの観点で評価網羅率が１００％で、３変数の組合せの観点で評価網羅率が９０％以上であれば、市場に出てから問題が起こることがないと分かっている機能については、２変数の組合せの観点と３変数の組合せの観点で評価網羅率を算出することに意義がある。
【００６６】
図３の説明に戻る。評価漏れコアパターン抽出手段２６は、評価可能パターンの中で実動作時パターンではないものを評価漏れパターンとし、２以上の評価漏れパターンに共通して含まれる評価漏れコアパターンを抽出する。
【００６７】
例えば、図８に示す例であれば、「×：未評価」となっている評価可能パターンが、評価漏れパターンである。図８に示す例では、評価漏れパターンの総数は、「９」である。
【００６８】
図８に示す例では、「Ａ１、Ｂ２」を含む評価漏れパターンは、Ｎｏが「５」、「８」の２つ存在する。また、「Ａ３、Ｂ１」を含む評価漏れパターンは、Ｎｏが「１８」、「２２」、「２４」の３つ存在する。このように、複数の評価漏れパターンに共通して存在する組合せパターンを、「評価漏れコアパターン」と称する。
【００６９】
例えば、評価漏れコアパターンを優先して実車評価を行うことによって、一度に複数の評価可能パターンが「○：評価済」となる可能性が高い。また、例えば、実車に問題が発生しているが原因が不明なときに、評価漏れコアパターンの実車評価を行うことによって、原因究明につながる可能性もある。このように、評価漏れコアパターンを把握することによって、制御プログラムの検証を効率的に行うことができる。
【００７０】
また、評価漏れコアパターン抽出手段２６は、評価漏れコアパターンの順位付けを行い、順位付け結果を出力しても良い。順位付けの判定基準は、例えば、評価漏れパターンの数とする。例えば、２つの評価漏れパターンに共通して存在する「Ａ１、Ｂ２」よりも、３つの評価漏れパターンに共通して存在する「Ａ３、Ｂ１」の方が、上位になるようにする。評価漏れコアパターンの順位付けを把握することによって、評価漏れ度合いが大きいパターンを容易に確認することができる。ひいては、制御プログラムの検証を効率的に行うことができる。
【００７１】
評価漏れパターン入力データ生成手段２７は、評価漏れパターンに対して、モデル検査のツールを用いてアサーションの反例を抽出し、評価漏れパターンの入力データを生成する。
【００７２】
モデル検査のツールでは、アサーションに対して、（１）「アサーションを満たすことを証明する」、又は（２）「アサーションの反例を１つ挙げる」のいずれかの結果を出力する。評価可能パターン抽出手段２４では、（１）「アサーションを満たすことを証明する」の結果を利用する。一方、評価漏れパターン入力データ生成手段２７では、（２）「アサーションの反例を１つ挙げる」の結果を利用する。
【００７３】
図１４は、入力データ生成処理のためのコード追加の一例を示す図である。図１４を参照しながら、図４の例において、実行パスの組合せパターン「Ａ１、Ｂ２」を実現する入力データを生成する処理を説明する。
【００７４】
図１４に示すように、追加コードは、（１）開始の直後に追加された「flag1=0」と「flag2=0」、（２）Ｓ７の制御命令の直前に追加された「flag1=1」、（３）Ｓ１０の制御命令の直前に追加された「flag2=1」、（４）終了の直前に追加された「assert(!(flag1==0
&& flag2==1))、の４箇所である。
【００７５】
図１４のようにコードを追加し、モデル検査のツールを用いることによって、「どんな入力パターンでもflag1=0かつflag2=1になることはない」というアサーションに対する反例として、評価漏れパターン「Ａ１、Ｂ２」を実現する入力データを生成することができる（非特許文献１のpp111-119参照）。
【００７６】
このように、評価漏れパターン入力データ生成手段２７によって、評価漏れパターンの評価に必要な入力データが自動的に生成される。自動的に生成される入力データは、評価網羅率の向上に的を得たものであるため、制御プログラムの検証を効率的に行うことができる。
【００７７】
＜変形例＞
次に、変形例を説明する。変形例では、データロガー装置５は、車両３の動作データに加えて、車両３の動作環境（走行環境）も記憶し、車両３の動作データと動作環境を対応付けて、検証装置２に送信する。動作環境の例としては、車両３の外気温、道路の勾配、路面状況（滑り易さ）、カーブ走行の曲率等が挙げられるが、特に限定されるものではない。
【００７８】
そして、実動作時パターン抽出手段２３は、動作環境を組合せパターンに含めて実動作時パターンを抽出する。また、評価可能パターン抽出手段２４は、動作環境を組合せパターンに含めて評価可能パターンを抽出する。「動作環境を組合せパターンに含める」とは、注目変数として、動作環境を示す変数も含めることを意味する。
【００７９】
評価可能パターン抽出手段２４は、制御プログラムデータと走行環境モデルから、取り得る「実行パス、走行環境」の組合せパターンを推定する。以下では、図１５を参照しながら、動作環境を含む評価可能パターン抽出処理を説明する。
【００８０】
図１５は、動作環境を含む評価可能パターン抽出処理のためのコード追加の一例を示す図である。例えば、走行環境に関する変数として「道路の勾配」を採用し、「下り坂」と「水平又は上り坂」を区別して評価することを考える。この場合、図１５に示すように、勾配を表すセンサ値に基づいて、「下り坂ならば、実行パスＺ１」、「水平又は上り坂ならば、実行パスＺ２」を取るような簡易プログラムを作成し、制御プログラムと同様に扱うことによって、動作環境を組合せパターンに含めて評価可能パターンを抽出することができる。
【００８１】
変形例では、異なる複数の動作環境における評価網羅率を算出し、把握することができるので、制御プログラムの信頼性を向上することができる。
【００８２】
図１６は、検証装置による検証処理の流れを示すフローチャートである。図１６のフローチャートは、検証装置２としてのコンピュータが、車載電子制御システム４による制御対象の動作データ及び制御プログラムデータを記憶部１２に記憶していることが前提である。
【００８３】
図１６に示すように、検証装置２の制御部１１は、記憶部１２に記憶されている動作データを入力し、記憶部１２に記憶されている制御プログラムデータを参照して、２以上の注目変数に関する実行パスの実動作時パターンを抽出する（Ｓ１０１）。
【００８４】
次に、検証装置２の制御部１１は、記憶部１２に記憶されている制御プログラムデータを入力し、モデル検査のツールを用いて、記憶部１２に記憶されている制御プログラムデータに埋め込まれているアサーションを満たすことを検証することによって実行パスの評価不能パターンを除外し、実行パスの評価可能パターンを抽出する（Ｓ１０２）。Ｓ１０１とＳ１０２は、どちらを先に実行しても良い。
【００８５】
次に、検証装置２の制御部１１は、評価可能パターンの総数を分母とし、実動作時パターンの総数を分子とする、２以上の注目変数の整合性評価に関する評価網羅率を算出し、出力する（Ｓ１０３）。Ｓ１０３において算出される評価網羅率は、並列実行される複数の実行パスの整合性評価に関する定量情報である。
【００８６】
次に、検証装置２の制御部１１は、評価可能パターンの中で実動作時パターンではないものを評価漏れパターンとし、２以上の評価漏れパターンに共通して含まれる評価漏れコアパターンを抽出し、出力する（Ｓ１０４）。評価漏れコアパターンを把握することによって、制御プログラムの検証を効率的に行うことができる。
【００８７】
次に、検証装置２の制御部１１は、評価漏れパターンに対して、モデル検査のツールを用いてアサーションの反例を抽出し、評価漏れパターンの入力データを生成し、出力する（Ｓ１０５）。Ｓ１０４とＳ１０５は、どちらを先に実行しても良い。評価漏れパターンの入力データに基づいて新たな実車評価を行うことによって、制御プログラムの検証を効率的に行うことができる。
【００８８】
以上、本発明の実施の形態によれば、並列実行される複数の実行パスの整合性評価に関する定量情報として、２以上の注目変数の整合性評価に関する評価網羅率を出力することができる。
【００８９】
尚、前述の説明では、車両３の実車評価の場面に適用するものとして説明したが、車両３の結合テストや統合テストの場面等、車両３の開発フェーズの上流のテストに適用することができる。
【００９０】
また、前述の説明では、検証対象として車載電子制御システム４に適用するものとして説明したが、航空機、ロボット、人工衛星などの制御システムに適用することができる。また、本発明の適用範囲は、これらの制御システムに限定されるものではなく、「複数の実行パスが並行して動作するシステム」であれば、どのような制御システムであっても良い。
【００９１】
以上、添付図面を参照しながら、本発明に係る検証装置等の好適な実施形態について説明したが、本発明はかかる例に限定されない。当業者であれば、本願で開示した技術的思想の範疇内において、各種の変更例又は修正例に想到し得ることは明らかであり、それらについても当然に本発明の技術的範囲に属するものと了解される。
【符号の説明】
【００９２】
１………検証システム
２………検証装置
３………車両
４………車載電子制御システム
５………データロガー装置
２１………車両動作データ記憶手段
２２………制御プログラムデータ記憶手段
２３………実動作時パターン抽出手段
２４………評価可能パターン抽出手段
２５………評価網羅率算出手段
２６………評価漏れコアパターン抽出手段
２７………評価漏れパターン入力データ生成手段
【図１】
2014016752.tif 000003
【図２】
2014016752.tif 000004
【図３】
2014016752.tif 000005
【図４】
2014016752.tif 000006
【図５】
2014016752.tif 000007
【図６】
2014016752.tif 000008
【図７】
2014016752.tif 000009
【図８】
2014016752.tif 000010
【図９】
2014016752.tif 000011
【図１０】
2014016752.tif 000012
【図１１】
2014016752.tif 000013
【図１２】
2014016752.tif 000014
【図１３】
2014016752.tif 000015
【図１４】
2014016752.tif 000016
【図１５】
2014016752.tif 000017
【図１６】
2014016752.tif 000018