(57)【要約】【課題】プログラムの並行実行に伴う不定性の有無を判定する。【解決手段】並行実行される第１サブプログラム及び第２サブプログラムを含むコンピュータプログラムの検査装置１０は、２つのサブプログラムが並行実行された後の第１プログラム状態と、２つのサブプログラムが順次実行された後の第２プログラム状態とが所定の等価性基準を充足するか否かを判定し、等価性基準の判定結果７０を出力する。【選択図】図１
2018151803.tif 000002
【特許請求の範囲】
【請求項１】
並行実行される第１サブプログラム及び第２サブプログラムを含むコンピュータプログラムの検査装置であって、
前記第１サブプログラム及び前記第２サブプログラムが並行実行された後の第１プログラム状態と、前記第１サブプログラム及び前記第２サブプログラムが順次実行された後の第２プログラム状態とが所定の等価性基準を充足するか否かを判定する判定部と、
前記判定部の判定結果を出力する出力部と、を有する検査装置。
【請求項２】
前記判定部は、前記第１サブプログラム及び前記第２サブプログラムがデータ分離されているときは、前記等価性基準が充足されると判定する、請求項１記載の検査装置。
【請求項３】
前記第１のサブプログラム及び前記第２のサブプログラムが、少なくとも複数の部分シーケンシャルプログラムと一以上の分岐命令とを含む場合は、
前記判定部は、第１サブプログラムの部分シーケンシャルプログラムと、第２サブプログラムの部分シーケンシャルプログラムとの組み合わせごとにデータ分離がされているか否かを判定し、すべての組み合わせでデータ分離されているときに前記等価性基準が充足されると判定する、請求項２記載の検査装置。
【請求項４】
前記判定部は、プログラムセレクタが定める実行開始時及び実行終了時の制約条件に従って前記第１サブプログラム及び前記第２サブプログラムがそれぞれ実行されたときに、前記第１サブプログラム及び前記第２サブプログラムの実行期間が重複する場合の有無を判定し、重複しないときは前記等価性基準が充足されると判定する、請求項１記載の検査装置。
【請求項５】
並行実行される第１サブプログラム及び第２サブプログラムを含む車両制御用コンピュータプログラムの検査を行う車載装置であって、
前記第１サブプログラム及び前記第２サブプログラムが並行実行された後の第１プログラム状態と、前記第１サブプログラム及び前記第２サブプログラムが順次実行された後の第２プログラム状態とが所定の等価性基準を充足するか否かを判定する判定部と、
前記判定部の判定結果を出力する出力部と、を有する車載装置。
【請求項６】
プログラムセレクタをさらに有し、
前記判定部は、前記プログラムセレクタが定める実行開始時及び実行終了時の制約条件に従って前記第１サブプログラム及び前記第２サブプログラムがそれぞれ実行されたときに、前記第１サブプログラム及び前記第２サブプログラムの実行期間が重複するか否かを判定する、請求項５記載の車載装置。
【請求項７】
プログラムセレクタをさらに有し、
前記判定部は、前記プログラムセレクタが定める実行開始時及び実行終了時の制約条件に従って前記第１サブプログラム及び前記第２サブプログラムがそれぞれ実行されたときに、プログラム変数へのリード・ライト履歴に基づいて等価性基準を充足するか否かを判定する、請求項５記載の車載装置。
【請求項８】
前記出力部は、
等価性基準を充足しないプログラム変数へのリード・ライト履歴を出力する、請求項７記載の車載装置
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータプログラムを検査する技術に関する。
【背景技術】
【０００２】
ムーアの法則に従って進展してきた半導体の微細化技術および動作周波数の改善が限界に到達し、シングルコアのＣＰＵでは、自動運転システムに代表される、大量のデータを高速に処理するプログラムを実行する際の計算負荷が過大になってきている。高い処理負荷に対応するために共有メモリ型マルチコアＣＰＵが実用されている。これにより、シーケンシャル実行するプログラムを何らかの手段を用いて分割して、複数のＣＰＵによる複数のシーケンシャル実行を併合した、プログラム並行実行によって性能改善を図ることが期待されている。
【０００３】
しかし、単一ＣＰＵコア上でシーケンシャル実行を前提として設計されてきたソフトウェア資産を、マルチコアＣＰＵ上で並行実行できるように機械的に改変するのは容易ではない。また、アムダールの法則で言及される通り、性能改善効果には原理的な限界がある。
【０００４】
マルチコアＣＰＵを用いて性能改善を図る際にあまり言及されない課題は、デバッグの困難さである。
【０００５】
特許文献１には、プログラムの並行実行の順序を記録し、プログラムの実行順序の履歴をデバッグ作業者に開示することで、このデバッグの困難さに対処することが記載されている。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２０１３−１１８００５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
プログラム状態は、実際にはＤＲＡＭ上のデータ（プログラム変数の値）である。プログラムの実行後のプログラム状態は、データに対する時系列のリード、ライト命令列により決まる。
【０００８】
シーケンシャルに実行されるプログラムは、単一のデータに対する複数回のリード・ライト命令が含まれていても、その順序が明示的に限定されているため、実行後のプログラム状態は一つに定まる。一方、プログラムが並行実行されたときは、リード・ライト命令の実行順序が不定であれば、実行後のプログラム状態は複数あり得る。このプログラム状態の不定性は、デバッグの困難さを招く。なぜならば、プログラムが実行されるごとに異なるプログラム状態が導かれ得るので、プログラムに不具合がある場合でもそれを特定することが難しいからである。
【０００９】
従って、プログラムの実行順序の不定性を排除できていることが保証されない限り、プログラムの並行実行が意図しないプログラム状態を導いた際に、プログラム自体の不具合であるのか、不定性に起因した不具合であるのかの判別が難しい。
【００１０】
そこで、本発明の目的は、プログラムの並行実行に伴う不定性の有無を判定することである。
【課題を解決するための手段】
【００１１】
本発明の一つの実施態様に従うプログラム検査装置は、並行実行される第１サブプログラム及び第２サブプログラムを含むコンピュータプログラムの検査を行う。プログラム検査装置は、第１サブプログラム及び第２サブプログラムが並行実行された後の第１プログラム状態と、第１サブプログラム及び第２サブプログラムが順次実行された後の第２プログラム状態とが所定の等価性基準を充足するか否かを判定する判定部と、判定部の判定結果を出力する出力部と、を有する。
【００１２】
本発明の一つの実施態様に従う車載装置は、並行実行される第１サブプログラム及び第２サブプログラムを含む車両制御用コンピュータプログラムの検査を行う。車載装置は、第１サブプログラム及び第２サブプログラムが並行実行された後の第１プログラム状態と、第１サブプログラム及び第２サブプログラムが順次実行された後の第２プログラム状態とが所定の等価性基準を充足するか否かを判定する判定部と、判定部の判定結果を出力する出力部と、を有する。
【図面の簡単な説明】
【００１３】
【図１】本発明の第１の実施形態に係るプログラム検査装置１０について説明する。
【図２】サブプログラム２０の構造を示す。
【図３】等価性判定テーブル３００の一例を示す。
【図４】プログラム実行順序番号テーブル４００の一例を示す。
【図５】本実施形態に係る車両制御装置１１０の構成図である。
【図６】プログラム実行順序履歴テーブル１２０の一例を示す。
【図７】リード・ライト命令履歴テーブル１３０の一例を示す。
【発明を実施するための形態】
【００１４】
以下、本発明の一実施形態に係るプログラム検査装置について、図面を参照して説明する。
【００１５】
図１は、本発明の第１の実施形態に係るプログラム検査装置１０について説明する。
【００１６】
プログラム検査装置１０は、例えば、中央処理装置（ＣＰＵ）、主記憶装置および補助記憶装置などを有する汎用的なコンピュータシステムにより構成され、以下に説明するプログラム検査装置１０の個々の構成要素または機能は、例えば、コンピュータプログラムを実行することにより実現される。
【００１７】
プログラム検査装置１０が検査対象とするコンピュータプログラム１５は、複数のサブプログラム２０で構成される。プログラム検査装置１０は、並行実行され得る任意の二つのサブプログラム２０の可換等価性を判定する。コンピュータプログラム１５は、例えば、車両制御用コンピュータプログラムでよい。
【００１８】
ここで、２つのサブプログラムが可換等価であるとは、２つのサブプログラムをシーケンシャル（逐次）実行したときと、並行して実行したときで、終了時のプログラム変数の値（プログラム状態）が同一であることを言う。つまり、２つのサブプログラムの並行実行によるプログラム変数へのリード及びライトによるアクセス順序の不定性に関わらず、同一のプログラム状態が導かれるときは、２つのサブプログラムが可換等価である。２つのサブプログラムが可換等価であるための必要十分条件は、２つのサブプログラムを構成するリード命令及びライト命令単位で可換であることである。
【００１９】
任意の２つのサブプログラムが可換等価であるか否かの判断基準である等価性基準４０は、以下の３つの分離原理からなる。
【００２０】
＜第１分離原理：データ分離＞
データ分離とは、２つのサブプログラムのリード・ライト命令がデータ（プログラム変数）の観点から分離されることをいう。共通のプログラム変数に対して、少なくとも一方のサブプログラムがライトを行い、他方のサブプログラムがリードする場合（リード・ライト競合）またはライトする場合（ライト・ライト競合）には、２つのサブプログラムの実行順序に応じて結果が変わり得る。一方で、このようなプログラム変数が存在しなければ、すなわちデータ分離が成立すれば、２つのサブプログラムの実行結果が実行順序に応じて変わることない。従って、データ分離がされている２つのサブプログラムは可換等価である。なお、２つのサブプログラムでリード・リード競合があっても、可換等価性に影響を与えることはないので、これは考慮しない。
【００２１】
＜第２分離原理：時間分離＞
時間分離とは、２つのサブプログラムのリード・ライト命令が実行時間の観点から分離されること、すなわち、実行期間が重複しないことをいう。２つのサブプログラムの実行期間が重複することがなければ、２つのプログラムはシーケンシャルに実行され、実行順序が定まるときは、実行順序に起因する実行結果の不定性の問題は生じない。
【００２２】
＜第３分離原理：制御分離＞
制御分離とは、データ分離が成立しない２つのサブプログラムにおいて、その２つのサブプログラムの開始時点で取りうるプログラム変数の状態であれば、そのリード・ライト命令が競合する箇所へ到達しないようにプログラム実行経路が設計されている場合をいう。
【００２３】
従って、可換等価性の判定は、すなわち、プログラム検査装置１０が等価性基準４０に基づいて、任意の２つのサブプログラム対がいずれかの分離原則を満たすか否かを判定することである。本実施形態では、データ分離及び時間分離について判定する。
【００２４】
第一の分離原則を逸脱する場合を検出する既知の手段として、プログラム実行時に、リード・ライト命令の対象となるデータの履歴を記録しておき、この履歴が有効である実行期間中に、可換でない命令列の有無を監視する方法が知られている。しかし、処理負荷が高いシーケンシャルプログラムは多数の変数にアクセスするため、著しい性能低下を招く上、第二、第三の分離原則を満たさない場合が無いか否かを判断しないため、設計段階での検出漏れを許す。つまり、不具合が実際に起こった時には検出できるが、不具合を起こさないように設計段階で検査する目的に資する方法ではない。そこで、本実施形態では以下に説明する方法で等価性判定を行う。
【００２５】
また、等価性基準を緩和することは、シーケンシャルプログラム実行が導くプログラム状態と同一とみなすプログラム状態の集合を拡張することに相当する。プログラム並行実行を構成するリード、ライト命令の実行順序の不定性を前提とした時、前述のいずれかの分離原則を常に保証できるようにシーケンシャルプログラム対が並行実行されるという保証をできない場合がある。特に、システム外部から予測不可能な時点で発生する割り込みに応答して実行されるシーケンシャルプログラムに含まれるライト命令対象のデータには、通常はそのデータを読み込む別のシーケンシャルプログラムが存在するため、第一、第二の分離原則を損なう。
【００２６】
この場合に可換等価性を代替する等価性の基準は、例えばシステム要件を参照するなどして得られる、ライト命令対象のデータ値が正常であるとする基準を用いて、リード・ライト命令単位では可換等価でなくとも例外とすることである。つまり、可換等価性に違反する当該データが前記正常値基準を満たす場合は、同一のプログラム状態の集合に属するとすればよい。
【００２７】
プログラムセレクタ３０は、システム外部からの入力及び時刻等に基づいて、各サブプログラム２０の実行開始時点及び実行終了時点を決定する。検査対象のプログラム１５が実行されるときは、プログラムセレクタ３０により各サブプログラム２０の実行開始及び終了が制御される。プログラムセレクタ３０は、各サブプログラムの開始決定、終了確認をするイベントハンドラである。
【００２８】
例えば、プログラムセレクタ３０は、各サブプログラム２０の実行開始タイミングを制御する。サブプログラム２０ごとに実行に要する時間は異なる。プログラムセレクタ３０は、各サブプログラム２０の標準的な実行時間の情報を有する。しかし、サブプログラム２０を実行したときのＣＰＵの占有状態やＤＲＡＭへのアクセス競合の発生度合いなどにより、各サブプログラム２０の実行に要する時間は変動し得る。そこで、プログラムセレクタ３０は各サブプログラム２０の最短実行時間及び最長実行時間の情報を有する。
【００２９】
ここで、図２を参照して、サブプログラム２０の構造について説明する。
【００３０】
サブプログラム２０は、少なくとも複数の部分シーケンシャルプログラムと一以上の分岐命令とで構成されていてもよい。部分シーケンシャルプログラムは、サブプログラム２０の中で分岐がない処理区間である。部分シーケンシャルプログラムは、例えば、基本的な処理単位であるデータへのリード命令、ライト命令、演算命令、真偽値評価などで構成されてよい。分岐命令は、ＩＦなどの条件分岐命令である。１以上の分岐命令を有するサブプログラム２０は、複数の部分シーケンシャルプログラムと、部分シーケンシャルプログラムを連結する一以上の分岐命令で表現できる。例えば、図２Ａ、Bに示すように、サブプログラム２０は、分岐命令で取り得る方向を示す有向グラフで部分シーケンシャルプログラムを結合したものと表現することができる。サブプログラム２０は、分岐命令を有しない場合もある。分岐命令を有しない場合、図２Ｃ，Ｄに示すように、一つの部分シーケンシャルプログラムで一つのサブプログラム２０が構成される。
【００３１】
プログラム検査装置１０が行う処理手順について、図１に従って説明する。
【００３２】
ＳＴＥＰ１００１では、プログラム検査装置１０は各サブプログラム２０をリード・ライト命令列に変換する。プログラム検査装置１０は、例えば、この変換をコンパイラ内部で行われているプログラム変数へのラベリング技術を援用して行ってもよい。例えば、プログラム検査装置１０は、サブプログラム２０を構成する個々の部分シーケンシャルプログラムのリード命令及びライト命令、ここでリードまたはライトするプログラム変数を特定する。さらに、プログラム検査装置１０は、サブプログラム２０に含まれる分岐命令において引数となる真偽値の評価に用いるプログラム変数を特定する。プログラム検査装置１０は、サブプログラム２０ごとに特定されたプログラム変数のリストを生成しても良い。
【００３３】
ＳＴＥＰ１００２〜１００４で、プログラム検査装置１０は、第１サブプログラム及び第２サブプログラムが並行実行された後の第１プログラム状態と、第１サブプログラム及び第２サブプログラムが順次実行された後の第２プログラム状態とが所定の等価性基準を充足するか否かを判定する。
【００３４】
ＳＴＥＰ１００２では、プログラム検査装置１０は、等価性基準４０に従って、並行実行されうる任意の２つのサブプログラムの可換等価性を判定する。プログラム検査装置１０は並行実行されうる任意の２つのサブプログラムを選択する。例えば、プログラム検査装置１０は、等価性基準４０のうちデータ分離原則により２つのサブプログラムが可換等価であるか否かを判定してもよい。例えば、プログラム検査装置１０は選択された２つのサブプログラム２０の対（サブプログラム対）について、ＳＴＥＰ１００１で得たリードまたはライトされる対象のプログラム変数リストを参照し、リード・ライト競合またはライト・ライト競合する共通のプログラム変数（命令対象データ）の有無により、可換等価であるか否かを判定する。プログラム検査装置１０は、２つのサブプログラム（第１サブプログラム及び第２サブプログラム）がデータ分離されているときは、等価性基準が充足されると判定してもよい。
【００３５】
図２のサブプログラムＣ及びＤのように、サブプログラム対の両方ともが一つの部分シーケンシャルプログラムだけで構成されている場合、プログラム検査装置１０は部分シーケンシャルプログラム同士（図２の部分シーケンシャルプログラムＣ１とＤ１）がデータ分離されているか否か判定すれば良い。
【００３６】
図２のサブプログラムＡ及びＢのように、サブプログラム対（第１のサブプログラム及び第２のサブプログラム）の少なくともいずれか一方（この場合は両方）が複数の部分シーケンシャルプログラムと一以上の分岐命令とを含む場合の判定方法について説明する。図２に示すサブプログラムＡは部分シーケンシャルプログラムＡ１、Ａ２及びＡ３と、一つの分岐を有する。サブプログラムＢは部分シーケンシャルプログラムＢ１、Ｂ２及びＢ３と、一つの分岐を有する。
【００３７】
分岐を含むサブプログラム対の可換等価性を判定する場合、すべての実行パス同士の組み合わせを考慮する必要がある。サブプログラムＡはＡ１→Ａ２とＡ１→Ａ３の二つの実行パスを有する。サブプログラムＢはＢ１→Ｂ２とＢ１→Ｂ３の二つの実行パスを有する。つまり、２×２＝４通りの実行パスの組み合わせがあり得るので、４通りのすべての組み合わせでデータ分離されていればサブプログラムＡとサブプログラムＢは可換等価である。
【００３８】
本実施形態では、可換等価性判定の計算量削減のために部分シーケンシャルプログラム単位で以下のように等価性判定を行う。すなわち、プログラム検査装置１０は、サブプログラムＡ（第１サブプログラム）の部分シーケンシャルプログラムと、サブプログラムＢ（第２サブプログラム）の部分シーケンシャルプログラムとの組み合わせごとにデータ分離がされているか否かを判定する。上記の例では、以下の９通りの組み合わせについてデータ分離の判定を行い、すべての組み合わせでデータ分離されているときに等価性基準が充足されると判定される。
（１）Ａ１とＢ１
（２）Ａ１とＢ２
（３）Ａ１とＢ３
（４）Ａ２とＢ１
（５）Ａ２とＢ２
（６）Ａ２とＢ３
（７）Ａ３とＢ１
（８）Ａ３とＢ２
（９）Ａ３とＢ３
【００３９】
上記９通りのすべての組み合わせでデータ分離されていれば、サブプログラムＡとサブプログラムＢはデータ分離されている。これにより、計算量の削減を実現できる。
【００４０】
プログラム検査装置１０は、ＳＴＥＰ１００２の判定結果を図３に示す等価性判定テーブルに保存する。
【００４１】
図３は、等価性判定テーブル３００の一例を示す。等価性判定テーブル３００は、同図に示すように、サブプログラムＳＰ［ｉ］とサブプログラムＳＰ［ｊ］との組み合わせが等価であるか非等価であるかを示す情報を有する。
【００４２】
ＳＴＥＰ１００３及びＳＴＥＰ１００４で、プログラム検査装置１０は、プログラムセレクタが定める実行開始時及び実行終了時の制約条件に従ってサブプログラム対（第１サブプログラム及び第２サブプログラム）がそれぞれ実行されたときに、第１サブプログラム及び第２サブプログラムの実行期間が重複する場合の有無を判定する。
【００４３】
例えば、ＳＴＥＰ１００３及びＳＴＥＰ１００４で、プログラム検査装置１０は、各サブプログラム２０の開始時点及び終了時点を順序化して、各サブプログラム２０の開始時点及び終了時点に順序番号として重複のない自然数を付与する。このサブプログラムの開始時点及び終了時点の順序番号は、図４に示すプログラム実行順序番号テーブル４００に格納される。
【００４４】
図４は、プログラム実行順序番号テーブル４００の一例を示す。プログラム実行順序番号テーブル４００は、同図に示すように、サブプログラムＳＰ［ｉ］の開始時点の順序番号Ｘ［ｉ］及び終了時点の順序番号Ｙ［ｉ］を有する。
【００４５】
各サブプログラム２０は、この順序番号に従って実行が開始され、終了する。つまり、この順序番号はサブプログラム２０の実行スケジュールを示す。従って、この順序番号により実行期間が重複する可能性があるサブプログラム対を検出することができるので、任意の２つのサブプログラム２０が時間分離されるか否かの判定が可能である。
【００４６】
ＳＴＥＰ１００３で、プログラム検査装置１０は、サブプログラム間の実行順序に関する制約条件である要件制約式ＳＡ、各サブプログラム２０の開始及び終了時点に関する順序番号制約式ＳＢ及び非等価基準判定制約式ＳＣを生成する。
【００４７】
なお、外部からの入力等、実行時点が予期できない場合には、順列化する時点の最大長に関する制約条件を付与する。この最大長は、反復を含めて実際に並行実行されうるサブプログラムの呼び出し回数に２を掛けた値とすればよい。
【００４８】
要件制約式ＳＡは、プログラムセレクタ３０が指定する、各サブプログラム２０の実行順序とタイミングに関する制約を示す式である。要件制約式ＳＡは、例えば、各サブプログラム２０の呼び出し順序の大小関係で表現される。
【００４９】
ここで、各サブプログラムＳＰ［ｉ］の開始時点をＸ［ｉ］、終了時点をＹ［ｉ］として、プログラム検査装置１０は要件制約式ＳＡを生成する。
【００５０】
プログラムセレクタ３０は、逐次実行タスク及び周期実行タスクを規定してもよい。例えば、サブプログラムＳＰ［０］を呼び出し、続いてサブプログラムＳＰ［１］を呼び出す逐次呼び出しをするようにプログラムセレクタ３０が設計されているとき、要件制約式ＳＡは、
Ｙ［０］＜Ｘ［１］
となる。あるいは、サブプログラムＳＰ［０］を呼び出し、一定の時間間隔ΔｔをおいてサブプログラムＳＰ［１］が呼び出されるとき、要件制約式ＳＡは、
Ｘ［１］−Ｙ［０］≧＝Δｔ
となる。
【００５１】
また、サブプログラムＳＰ［０］が周期実行タスクである場合は、一定周期Ｔ後の別の時点で呼び出される同じ処理ＳＰ［１０］があるとき、要件制約式ＳＡは、
Ｔ−誤差＝＜Ｘ［１０］−Ｘ［０］＜＝Ｔ＋誤差
となる。ここで、同じ処理でも開始時点及び終了時点が異なるので、ＳＰ［０］とＳＰ［１０］と異なる表記をする。
【００５２】
また、プログラム検査装置１０は、各サブプログラムＳＰ［ｉ］の開始時点Ｘ［ｉ］及び終了時点Ｙ［ｉ］を用いて、順序番号の重複がないことを示す順序番号制約式ＳＢを生成する。
【００５３】
例えば、順序番号制約式ＳＢは以下の式１で表される。
【数１】
2018151803.tif 000003
（式１）
【００５４】
順序番号制約式ＳＢは、以下の順序番号に関する拘束条件の論理和が含まれる。
（１）順序番号の重複が無い
（２）サブプログラムＳＰ［ｉ］の実行時間（Ｙ［ｉ］−Ｘ［ｉ］）の下限（最低実行時間ｍｉｎ＿ＥｘｅｃＴｉｍｅ）と上限（最高実行時間ｍａｘ＿ＥｘｅｃＴｉｍｅ）が定められている
（３）サブプログラムＳＰ［ｉ］とサブプログラムＳＰ［ｊ］の開始及び終了は同時ではない
【００５５】
プログラム検査装置１０はさらに、ＳＴＥＰ１００２でデータ分離原則の等価性基準４０を満たさないと判定されたサブプログラムＳＰ［ｉ］とＳＰ［ｊ］の対を特定し、非等価基準判定制約式ＳＣを構築する。非等価基準判定制約式ＳＣは、時間分離の等価性基準判定制約式であり、以下の式２で表される。
【数２】
2018151803.tif 000004
（式２）
【００５６】
非等価基準判定制約式ＳＣは、等価性基準を満たさない二つのサブプログラム対ＳＰ［ｉ］とＳＰ［ｊ］が並行実行されるような、開始時点及び終了時点の制約関係があるという条件を表現する。なお、式２は以下の式３に変換可能である。
【数３】
2018151803.tif 000005
（式３）
【００５７】
ＳＴＥＰ１００４では、プログラム検査装置１０は、ＳＡＴソルバ５０を用いて要件制約式ＳＡの充足解の有無と、ＳＡ＆＆ＳＢ＆＆ＳＢの充足解の有無を判定する。充足解があるときは、プログラム検査装置１０はＳＡＴソルバ５０から順序番号の具体的な割当値を取得する。
【００５８】
ＳＡＴソルバ５０は、所与の制約条件式を満たす自然数値の割当値があれば、具体的な割当値を列挙する機能を有するものを用いてもよい。実行順序に関する制約条件式は自然数に対する線形制約のみであるため、ＳＡＴソルバ５０に代えてＳＭＴソルバを用いてよい。市販の整数計画法ソルバは、制約条件式の論理積のみ受け付けるものが多い。しかし、サブプログラム実行順序が、何らかのガード条件により制御される場合には、制約条件式は、複数の制約条件式の論理和を含むものになる。この場合、例えば補助変数を援用した式４に示す公式を用いて、論理和を含む式を制約条件式の論理積の形式に変換してもよい。
【数４】
2018151803.tif 000006
（式４）
【００５９】
なお、論理和と論理積とを組み合わせた制約式を解く汎用のＳＡＴソルバ５０の出力値はビット値列であり、市販の整数計画法ソルバの場合も補助変数を含む自然数列を出力する。そこで、プログラム検査装置１０は、ＳＡＴソルバ５０の出力値のビット列から実行順序番号｛Ｘ［ｉ］，Ｙ［ｉ］｝を取り出すデコード処理を行っても良い。デコードにより取得した実行順序番号｛Ｘ［ｉ］，Ｙ［ｉ］｝はプログラム実行順序番号テーブル４００に保存される。
【００６０】
なお、実行可能な形でプログラムセレクタ３０が設計されている場合には、要件制約式ＳＡの充足解が存在する。充足解が存在しない場合は、そのプログラム１５を実行できないので、プログラム検査装置１０の検査対象にならない。
【００６１】
ＳＴＥＰ１００５では、プログラム検査装置１０は、ＳＴＥＰ１００４で生成されたプログラム実行順序番号テーブル４００を参照し、サブプログラム対ごとに制約式ＳＡ＆＆ＳＢ＆＆ＳＣの充足解の有無を確認する。
【００６２】
制約式ＳＡ＆＆ＳＢ＆＆ＳＣの充足解がない場合は（ＳＴＥＰ１００５：Ｎｏ）、そのサブプログラム対については、時間分離ができない実行順序は存在しないことを意味する。つまり、そのサブプログラム対は時間分離されるので可換等価である。この場合にはＳＴＥＰ１００６に進み、プログラム検査装置１０は、ＳＴＥＰ１００４で得た要件制約式ＳＡの充足解を参照し、その中からサブプログラム対のそれぞれの開始時点Ｘ［ｉ］の順序番号を取得する。ＳＴＥＰ１００７で、プログラム検査装置１０は、その順序番号に従い、等価性基準の判定結果７０としてサブプログラム対を直列化した合成シーケンシャルプログラムを出力してもよい。
【００６３】
他方、制約式ＳＡ＆＆ＳＢ＆＆ＳＣの充足解がある場合は（ＳＴＥＰ１００５：Ｙｅｓ）、そのサブプログラム対については、時間分離ができない実行順序が存在することを意味する。つまり、そのサブプログラム対は時間分離できない場合があり、可換等価ではない。この場合にはＳＴＥＰ１００８に進み、プログラム検査装置１０は、制約式ＳＡ＆＆ＳＢ＆＆ＳＣの充足解を参照し、制約式ＳＣの構成要素である制約式Ｅ［ｉ，ｊ］を満たしていないサブプログラム対であるサブプログラムＳＰ［ｉ］，ＳＰ［ｊ］を特定する。制約式Ｅ［ｉ，ｊ］を満たしていないサブプログラムＳＰ［ｉ］，ＳＰ［ｊ］は、すなわち、サブプログラムＳＰ［ｉ］の実行期間とＳＰ［ｊ］の実行期間の一部が重複する。プログラム検査装置１０は、そのようなサブプログラムＳＰ［ｉ］、ＳＰ［ｊ］の開始時点に対応する順序番号を取得する。ＳＴＥＰ１００９では、プログラム検査装置１０は、等価性基準を充足しない合成シーケンシャルプログラムとして、サブプログラムＳＰ［ｉ］→ＳＰ［ｊ］の順で直列化した合成シーケンシャルプログラム０と、ＳＰ［ｊ］→ＳＰ［ｉ］の順で直列化した合成シーケンシャルプログラム１を生成してもよい。
【００６４】
ＳＴＥＰ１０１０では、プログラム検査装置１０は、等価性基準を充足するか否かの判定結果を出力する。例えば、プログラム検査装置１０は、ＳＴＥＰ１００７及びＳＴＥＰ１００９で生成された合成シーケンシャルプログラム６０及び等価性の判定結果７０を出力する。
【００６５】
これにより、検査対象プログラム１５に含まれるサブプログラム２０のうち並行実行され得るサブプログラム対の可換等価性を判定することができる。
【００６６】
本発明の第２の実施形態に係る車両制御装置１１０について説明する。本実施形態では、第１の実施形態と同じ機能または構成については同一の符号を付して説明を省略する場合がある。本実施形態の車両制御装置１１０では、例えば、第１の実施形態で説明したプログラム検査装置１０で検査済みのコンピュータプログラム１５が実行される。車両制御装置１１０は、例えば、データ分離がされていないサブプログラム対が、時間分離されて実行されているか否かを監視する。
【００６７】
図５は、本実施形態に係る車両制御装置１１０の構成図である。車両制御装置１１０は、プロセッサ８０及びメモリ９０を有する。メモリ９０には、複数のサブプログラム２０を含むコンピュータプログラム１５、プログラムセレクタ３０、プログラム変数１００、プログラム実行順序履歴テーブル１２０及びリード・ライト命令履歴テーブル１３０が記憶されている。プロセッサ８０がサブプログラム２０単位に読み込んでコンピュータプログラム１５を実行する。ここでは、コンピュータプログラム１５は車両制御に関するコンピュータプログラムである。
【００６８】
プロセッサ８０は、プログラムセレクタ３０により制御されるプログラム実行順序番号に従ってサブプログラム２０を実行して車両を制御する。プロセッサ８０は、サブプログラム２０を実行すると同時にサブプログラム２０の実行開始及び終了を監視し、所定の２つのサブプログラム２０の実行期間の重複の有無を判定してもよい。本実施形態では、２つのサブプログラム２０の実行期間の重複の有無を、以下に説明する二通りの判定方法のいずれかで行ってもよい。
【００６９】
図６にプログラム実行順序履歴テーブル１２０の一例を示す。プログラム実行順序履歴テーブル１２０は、連番１２１と、サブプログラム番号１２２と、イベント１２３とをデータ項目として有する。
【００７０】
プログラム実行順序履歴テーブル１２０には、所定のサブプログラム２０の実行開始時及び終了時が順序化して記録される。例えば、プロセッサ８０が所定のサブプログラム２０の実行を開始した時点及び終了した時点で、プログラム実行順序履歴テーブル１２０に、連番１２１に対してサブプログラム番号１２２及び開始または終了を示すイベント１２３が記録されるようにしてもよい。
【００７１】
プロセッサ８０は、プログラム実行順序履歴テーブル１２０を参照して等価性判定を行っても良い。例えば、第１の実施形態のプログラム検査装置１０でデータ分離がされていないことが確認されているサブプログラム対について、プログラム実行順序履歴テーブル１２０にそれらの開始及び終了の履歴が記録されるようにしてもよい。これにより、プロセッサ８０は、その２つのサブプログラムの実行期間が部分的であっても重複している場合を検出できる。実行期間が重複する場合は等価性基準４０の時間分離がされていないということであり等価性基準を満たさない。その場合、プロセッサ８０は、この２つのサブプログラム番号を特定し、このサブプログラム対は等価性基準４０を満たさないとする等価性基準判定結果７０を出力してもよい。
【００７２】
プロセッサ８０は、プログラムセレクタ３０が定める実行開始時及び実行終了時の制約条件に従ってサブプログラム対（第１サブプログラム及び第２サブプログラム）がそれぞれ実行されたときに、プログラム変数１００へのリード・ライト履歴に基づいて等価性基準を充足するか否かを判定してもよい。
【００７３】
図７は、リード・ライト命令履歴テーブル１３０の一例を示す。リード・ライト命令履歴テーブル１３０は、プログラム変数番号１３１と、リード命令を出したサブプログラム番号１３２と、ライト命令を出したサブプログラム番号１３３とをデータ項目として有する。
【００７４】
プロセッサ８０は、リード命令またはライト命令の実行を検出すると、リード・ライト命令履歴テーブル１３０の対応する領域にそのサブプログラム番号を履歴として追加する。リード・ライト命令履歴テーブル１３０では、サブプログラムの実行期間中のみその履歴が保持される。サブプログラム２０の実行が終了すると、プロセッサ８０は対応する履歴をリード・ライト命令履歴テーブル１３０から削除する。
【００７５】
リード・ライト命令履歴テーブル１３０を用いる場合もプログラム実行順序履歴テーブル１２０を用いる場合と同様に、第１の実施形態のプログラム検査装置１０でデータ分離がされていないことが確認されているサブプログラム対について、そのリード・ライト命令履歴を記録するようにしてもよい。これにより、その２つのサブプログラムの実行期間が部分的にでも重複しているか否かを判定することができる。
【００７６】
プロセッサ８０は、リード・ライト命令履歴テーブル１３０に履歴を書き込む際に等価性判定を行っても良い。例えば、ライト命令が実行されるとき、プロセッサ８０がそのライト命令を出したサブプログラム番号をテーブルに書き込む際、既に同じプログラム変数番号１３１に対するリード命令またはライト命令のサブプログラム番号が履歴として記録されていれば、データ競合が生じている。従って、このような場合にはプロセッサ８０は、この２つのサブプログラム番号を特定して、このサブプログラム対は等価性基準４０を満たさないとする等価性基準判定結果７０を出力してもよい。
【００７７】
これにより、車両制御用コンピュータプログラムを実行中に、そのサブプログラム２０が等価性基準を満たすか否かを判定することができる。
【００７８】
上述した本発明の実施形態は、本発明の説明のための例示であり、本発明の範囲をそれらの実施形態にのみ限定する趣旨ではない。当業者は、本発明の要旨を逸脱することなしに、他の様々な態様で本発明を実施することができる。
【符号の説明】
【００７９】
１０     プログラム検査装置
２０     サブプログラム
３０     プログラムセレクタ
４０   等価性基準
５０     ＳＡＴソルバ
６０     合成シーケンシャルプログラム
７０     等価性基準判定結果
８０     プロセッサ
９０     メモリ
１１０  車両制御装置
【図１】
2018151803.tif 000007
【図２】
2018151803.tif 000008
【図３】
2018151803.tif 000009
【図４】
2018151803.tif 000010
【図５】
2018151803.tif 000011
【図６】
2018151803.tif 000012
【図７】
2018151803.tif 000013