(57)【要約】      （修正有）【課題】２つの状態遷移構造の状態の同時成立性を好適に解析する状態遷移解析システムを提供する。【解決手段】状態遷移解析システムは、第１状態遷移構造で着目する第１状態Ｓ１と第２状態遷移構造で着目する第２状態Ｓ２を選択し、Ｓ１に入場する遷移条件である第１入場条件及びＳ２に入場する遷移条件である第２入場条件を特定し、第１入場条件と第２入場条件に共通する因子を抽出するＳ１０１。Ｓ１０２〜Ｓ１０４での判定結果に基づいて、第１入場条件と第２入場条件の同時成立性を判定するＳ１０５。Ｓ１から退場する第１退場条件及びＳ２から退場する第２退場条件を特定し、第１退場条件と第２退場条件に共通する因子を抽出するＳ１０６。Ｓ１０７〜Ｓ１０９での判定結果に基づいて、第１退場条件と第２退場条件との同時成立性を判定するＳ１１０。入場条件及び退場条件の同時成立性の判定結果に基づいて、Ｓ１とＳ２との同時成立性を判定するＳ１１１。【選択図】図６
2019185481.tif 000002
【特許請求の範囲】
【請求項１】
第１システムの複数の状態および遷移条件が定められた第１状態遷移構造を表す第１情報と、第２システムの複数の状態および遷移条件が定められた第２状態遷移構造を表す第２情報とを記憶する記憶部と、
前記記憶部が記憶する前記第１情報および前記第２情報を参照して、前記第１状態遷移構造における第１状態への遷移条件である第１入場条件と、前記第２状態遷移構造における第２状態への遷移条件である第２入場条件とに共通する因子を抽出し、抽出結果と前記第１入場条件および前記第２入場条件の論理的解析とに基づいて、前記第１入場条件および前記第２入場条件の同時成立性を判定する入場判定部と、
前記記憶部が記憶する前記第１情報および前記第２情報を参照して、前記第１状態遷移構造における前記第１状態からの遷移条件である第１退場条件と、前記第２状態遷移構造における前記第２状態からの遷移条件である第２退場条件とに共通する因子を抽出し、抽出結果と前記第１退場条件および前記第２退場条件の論理的解析とに基づいて、前記第１退場条件および前記第２退場条件の同時成立性を判定する退場判定部と、
前記入場判定部および前記退場判定部の判定結果に基づいて、前記第１状態が継続する期間および前記第２状態が継続する期間が重複するか否かを、各前記期間の始期どうし、および、終期どうしの、少なくとも一方が一致する場合と、いずれも一致しない場合とのいずれにおいても判定する同時成立判定部とを備える、状態遷移解析システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、２つの状態遷移構造における各状態の同時成立性を解析する状態遷移解析システムに関する。
【背景技術】
【０００２】
車両等には複数のシステムが搭載されている。各システムの振る舞いは、それぞれ、複数の状態と、状態間の遷移条件とを含む状態遷移構造によって表現できる。特許文献１は、車両のシートに、「乗員無し」、「チャイルドシート固定」、「大人着座」の状態が定義され、これらの状態間の遷移条件が、シートに設けられた荷重検出部が検出する荷重およびその継続時間によって定められることを開示している。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２０１７−１３７７７号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
車両においては、多くの制御システムが搭載されており、それぞれが車両制御のための各種機能を分担して実行する。各制御システムは、ユーザーの車両操作によって定まるアクセルペダル開度、ブレーキペダル踏力、操舵角、各種指示の有無等の制御量や、車両が備える各種センサが検出する前後左右方向の加速度、車速、ロール／ヨー、ＧＰＳ座標等の状態量のうち、それぞれの分担に応じて必要なものを受け取り、これらに基づいて、加減速等の機能や加速度等の制御量、ユーザーへの表示内容等を決定する。
【０００５】
車両制御の堅牢性のためには、例えば複数の協調動作を確実に行い、かつ、背反動作を確実に回避することが好ましい。そのためには、集中的な状態遷移制御によって車両制御を行うことが考えられる。しかし、上述のように、制御システムごとに機能が設計され、それぞれの制御システムが固有の状態遷移構造に従って動作しているので、このような集中的な状態遷移制御を設計する手法は現実的でない。現状では、制御システム間の着目する状態どうしの同時成立性を解析することにより、車両制御の堅牢性の検証を行っている。しかしながら、制御システムの数が多く、また、それぞれの状態遷移構造が複雑であるため、もれなく検証を行う工数は大きい。
【０００６】
並行処理システムの解析に用いられる手法としてＣＳＰ（Communication Sequential Processes）が知られており、例えば、複数のロボットの協調動作をＣＳＰにより論理的に記述し、協調動作を網羅的に分析して、設計段階で並行プロセスの不具合を発見することが試みられている（URL：http://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15H02687）。上述の検証のためＣＳＰを採用することも考えられる。しかし、ＣＳＰでは、２つの制御システムの状態遷移構造をまとめて扱うことができるのは、同一の遷移条件が成立することによって同一タイミングで状態遷移する場合のみである。すなわち、ＣＳＰでは、着目する状態どうしの同時成立性を解析するにあたって、状態遷移のタイミングが異なる場合について解析することが困難であり、上述のような車両制御の堅牢性をもれなく検証するには限界があった。
【０００７】
本発明は、上記課題を鑑みてなされたものであり、２つの状態遷移構造における各状態の同時成立性を好適に解析可能な状態遷移解析システムを提供することを目的とする。
【課題を解決するための手段】
【０００８】
上記課題を解決するために、本発明の一局面は、第１システムの複数の状態および遷移条件が定められた第１状態遷移構造を表す第１情報と、第２システムの複数の状態および遷移条件が定められた第２状態遷移構造を表す第２情報とを記憶する記憶部と、記憶部が記憶する第１情報および第２情報を参照して、第１状態遷移構造における第１状態への遷移条件である第１入場条件と、第２状態遷移構造における第２状態への遷移条件である第２入場条件とに共通する因子を抽出し、抽出結果と第１入場条件および第２入場条件の論理的解析とに基づいて、第１入場条件および第２入場条件の同時成立性を判定する入場判定部と、記憶部が記憶する第１情報および第２情報を参照して、第１状態遷移構造における第１状態からの遷移条件である第１退場条件と、第２状態遷移構造における第２状態からの遷移条件である第２退場条件とに共通する因子を抽出し、抽出結果と第１退場条件および第２退場条件の論理的解析とに基づいて、第１退場条件および第２退場条件の同時成立性を判定する退場判定部と、入場判定部および退場判定部の判定結果に基づいて、第１状態が継続する期間および第２状態が継続する期間が重複するか否かを、各期間の始期どうし、および、終期どうしの、少なくとも一方が一致する場合と、いずれも一致しない場合とのいずれにおいても判定する同時成立判定部とを備える、状態遷移解析システムである。
【０００９】
これにより、第１状態および第２状態の入場条件どうしの解析と、退場条件どうしの解析を論理的に行い、第１状態と第２状態との同時成立性を遷移タイミングが異なっていても判定することができる。
【発明の効果】
【００１０】
以上のように、本発明によれば、第１状態および第２状態の入場条件どうしの解析と、退場条件どうしの解析を、共通因子の抽出および論理的解析を行い、第１状態と第２状態との同時成立性を、遷移タイミングが同じである場合と異なっている場合の両方において、好適に判定することができる状態遷移解析システムを提供することができる。
【図面の簡単な説明】
【００１１】
【図１】本発明の一実施形態に係る状態遷移解析システムの機能ブロック図
【図２】本発明の一実施形態に係る第１状態遷移構造の例を示す図
【図３】本発明の一実施形態に係る第１情報の例を示す図
【図４】本発明の一実施形態に係る第２状態遷移構造の例を示す図
【図５】本発明の一実施形態に係る第２情報の例を示す図
【図６】本発明の一実施形態に係る状態遷移解析処理のフローチャート
【図７】本発明の一実施形態に係る状態遷移解析処理の判定テーブルの例を示す図
【図８】本発明の一実施形態に係る同時成立性のタイプの例を示す図
【図９】本発明の一実施形態に係る同時成立性のタイプの例を示す図
【図１０】本発明の一実施形態に係る同時成立性のタイプの例を示す図
【図１１】本発明の一実施形態に係る同時成立性のタイプの例を示す図
【図１２】本発明の一実施形態に係る同時成立性のタイプの例を示す図
【図１３】本発明の一実施形態に係る同時成立性の一覧の例を示す図
【図１４】本発明の適用例に係る走行支援システムの状態遷移構造を表す情報の例を示す図
【図１５】本発明の適用例に係るブレーキ制御システムの状態遷移構造を表す情報の例を示す図
【発明を実施するための形態】
【００１２】
（概要）
本発明に係る状態遷移解析システムにおいては、第１状態遷移構造において第１状態に遷移する第１入場条件と第２状態遷移構造において第２状態に遷移する第２入場条件について、共通因子を抽出して、共通因子がある場合は第１入場条件および第２入場条件の論理的な解析を行う。また、第１状態遷移構造において第１状態から遷移する第１退場条件と第２状態遷移構造において第２状態から遷移する第２退場条件について、共通因子を抽出して、共通因子がある場合は第１退場条件および第２退場条件の論理的な解析を行う。これらの解析結果を用いることにより、第１状態と第２状態との同時成立性を、入場タイミングや退場タイミングが同じ場合と異なる場合との両方において判定する。
【００１３】
（実施形態）
以下、本発明の実施形態について、図面を参照しながら詳細に説明する。
【００１４】
＜構成＞
図１に、本実施形態に係る状態遷移解析システムの機能ブロック図を示す。状態遷移解析システム１０は、記憶部１１、入場判定部１２、退場判定部１３、同時成立判定部１４を含む。
【００１５】
記憶部１１は、第１システムの状態遷移構造である第１状態遷移構造を表す第１情報、第２システムの状態遷移構造である第２状態遷移構造を表す第２情報を記憶する。第１システム、第２システムは例えば車両に搭載される制御装置である。
【００１６】
図２に第１状態遷移構造の例を示し、図３に第１情報を表すテーブルの例を示す。図２、図３に示す例では、第１状態遷移構造において以下の状態遷移が行われることを表している。
初期状態Ｄｅｆ１において遷移条件１−１が成立すると状態Ａ１に遷移する。
状態Ａ１において遷移条件１−２が成立すると状態Ｂ１に遷移する。
状態Ｂ１において遷移条件１−３が成立すると状態Ａ１に遷移する。
状態Ｂ１において遷移条件１−４が成立すると状態Ｃ１に遷移する。
状態Ｃ１において遷移条件１−５が成立すると状態Ａ１に遷移する。
ここで、遷移条件１−１〜１−５のそれぞれは、具体的には第１制御システムが受け取る制御量や状態量に含まれる因子である因子Ｉｎ１、Ｉｎ２、Ｉｎ３の一部または全部を含む論理式で表現される。
【００１７】
図４に第２状態遷移構造の例を示し、図５に第２情報を表すテーブルの例を示す。図４、図５に示す例では、第２状態遷移構造において以下の状態遷移が行われることを表している。
初期状態Ｄｅｆ２において遷移条件２−１が成立すると状態Ｃ２に遷移する。
状態Ｃ２において遷移条件２−２が成立すると状態Ｂ２に遷移する。
状態Ｂ２において遷移条件２−３が成立すると状態Ａ２に遷移する。
状態Ａ２において遷移条件２−４が成立すると状態Ｂ２に遷移する。
状態Ａ２において遷移条件２−５が成立すると状態Ｃ２に遷移する。
ここで、遷移条件２−１〜２−５のそれぞれは、具体的には第２制御システムが受け取る制御量や状態量に含まれる因子である因子Ｉｎ３、Ｉｎ４、Ｉｎ５の一部または全部を含む論理式で表現される。
【００１８】
入場判定部１２は、第１情報を参照して、第１状態遷移構造における着目する第１状態Ｓ１（Ｄｅｆ１、Ａ１、Ｂ１、Ｃ１のいずれか）が、他の状態から遷移する（入場する）場合の遷移条件である第１入場条件を特定する、また、入場判定部１２は、第２情報を参照して、第２状態遷移構造における着目する第２状態Ｓ２（Ｄｅｆ２、Ａ２、Ｂ２、Ｃ２のいずれか）が、他の状態から遷移する（入場する）場合の遷移条件である第２入場条件を特定する。入場判定部１２は、第１入場条件および第２入場条件の同時成立性を判定する。
【００１９】
退場判定部１３は、第１情報を参照して、第１状態Ｓ１が、他の状態へ遷移する（退場する）場合の遷移条件である第１退場条件を特定する、また、退場判定部１３は、第２情報を参照して、第２状態Ｓ２が、他の状態へ遷移する（退場する）場合の遷移条件である第２退場条件を特定する。退場判定部１３は、第１退場条件および第２退場条件の同時成立性を判定する。
【００２０】
同時成立判定部１４は、入場判定部１２および退場判定部１３の判定結果に基づいて、第１状態Ｓ１および第２状態Ｓ２の同時成立性を判定する。
【００２１】
＜処理＞
以下に、本実施形態に係る状態遷移解析処理の例を説明する。図６は、本処理を示すフローチャートである。
【００２２】
（ステップＳ１０１）：入場判定部１２は、記憶部１１が記憶している第１情報を参照して、第１状態遷移構造における着目する第１状態Ｓ１としてＤｅｆ１、Ａ１、Ｂ１、Ｃ１のいずれかを選択する。ここでは例としてＳ１＝Ｂ１とする。また、入場判定部１２は、記憶部１１が記憶している第２情報を参照して、第２状態遷移構造における着目する第２状態Ｓ２としてＤｅｆ２、Ａ２、Ｂ２、Ｃ２のいずれかを選択する。ここでは例としてＳ２＝Ａ２とする。つぎに入場判定部１２は第１状態Ｓ１に入場する遷移条件である第１入場条件を特定する。この例では、第１入場条件は、状態Ａ１から状態Ｂ１に遷移する条件である遷移条件１−２である。また、入場判定部１２は第２状態Ｓ２に入場する遷移条件である第２入場条件を特定する。この例では、第２入場条件は、状態Ｂ２から状態Ａ２に遷移する条件である遷移条件２−３である。
【００２３】
入場判定部１２は、第１入場条件と第２入場条件とに共通する因子を抽出する。例では、遷移条件１−２と遷移条件２−３との共通因子として因子Ｉｎ３を抽出する。
【００２４】
（ステップＳ１０２）：入場判定部１２は、共通因子が抽出されたか否かを判定する。共通因子がなく抽出されなかった場合、ステップＳ１０５に進み、例のように共通因子があり抽出された場合、ステップＳ１０３に進む。
【００２５】
（ステップＳ１０３）：入場判定部１２は、第１入場条件と第２入場条件とが、論理的に同値であるか否かを判定する。例では、論理式「（遷移条件１−２）≡（遷移条件２−３）＝真」が成立するか否かを判定する。遷移条件が同値である場合、ステップＳ１０５に進み、遷移条件が同値でない場合、ステップＳ１０４に進む。
【００２６】
（ステップＳ１０４）：入場判定部１２は、第１入場条件と第２入場条件とが、論理的に同時に成立することがありうるか否かを判定する。例では、論理式「（遷移条件１−２）かつ（遷移条件２−３）＝真」が成立する場合があるか否かを、例えばＳＭＴ（Satisfiability Modulo Theories）解析等の手法により判定する。判定結果によらず次のステップＳ１０５に進む。
【００２７】
（ステップＳ１０５）：入場判定部１２は、ステップＳ１０２〜Ｓ１０４での判定結果に基づいて、第１入場条件と第２入場条件との同時成立性を以下のように判定する。
ステップＳ１０２で共通因子がないと判定した場合、論理的には解析不可であると判定する。
ステップＳ１０３で遷移条件が同値であると判定した場合、「完全一致」と判定する。
ステップＳ１０４で遷移条件が同時に成立する場合があると判定した場合、「部分一致」と判定する。
ステップＳ１０４で遷移条件が同時に成立する場合がないと判定した場合、「不一致」と判定する。
【００２８】
（ステップＳ１０６）：退場判定部１３は第１状態Ｓ１から退場する遷移条件である第１退場条件を特定する。この例では、第１退場条件は、状態Ｂ１から状態Ａ１に遷移する条件である遷移条件１−３、および、状態Ｂ１から状態Ｃ１に遷移する条件である遷移条件１−４である。また、退場判定部１３は第２状態Ｓ２から退場する遷移条件である第２退場条件を特定する。この例では、第２退場条件は、状態Ａ２から状態Ｂ２に遷移する条件である遷移条件２−４、および、状態Ａ２から状態Ｃ２に遷移する条件である遷移条件２−５である。
【００２９】
退場判定部１３は、第１退場条件と第２退場条件とに共通する因子を抽出する。例では、遷移条件１−３、１−４と遷移条件２−４、２−５との共通因子として因子Ｉｎ３を抽出する。
【００３０】
（ステップＳ１０７）：退場判定部１３は、共通因子が抽出されたか否かを判定する。共通因子がなく抽出されなかった場合、ステップＳ１１０に進み、例のように共通因子があり抽出された場合、ステップＳ１０８に進む。
【００３１】
（ステップＳ１０８）：退場判定部１３は、第１退場条件と第２退場条件とが、論理的に同値であるか否かを判定する。例では、論理式「〔（遷移条件１−３）または（遷移条件１−４）〕≡〔（遷移条件２−４）または（遷移条件２−５）〕＝真」が成立するか否かを判定する。遷移条件が同値である場合、ステップＳ１１０に進み、遷移条件が同値でない場合、ステップＳ１０９に進む。
【００３２】
（ステップＳ１０９）：退場判定部１３は、第１退場条件と第２退場条件とが、論理的に同時に成立することがありうるか否かを判定する。例では、論理式「〔（遷移条件１−３）または（遷移条件１−４）〕かつ〔（遷移条件２−４）または（遷移条件２−５）〕＝真」が成立する場合があるか否かを、例えばＳＭＴ（Satisfiability Modulo Theories）解析等の手法により判定する。判定結果によらず次のステップＳ１１０に進む。
【００３３】
（ステップＳ１１０）：退場判定部１３は、ステップＳ１０７〜Ｓ１０９での判定結果に基づいて、第１退場条件と第２退場条件との同時成立性を以下のように判定する。
ステップＳ１０７で共通因子がないと判定した場合、論理的には解析不可であると判定する。
ステップＳ１０８で遷移条件が同値であると判定した場合、「完全一致」と判定する。
ステップＳ１０９で遷移条件が同時に成立する場合があると判定した場合、「部分一致」と判定する。
ステップＳ１０９で遷移条件が同時に成立する場合がないと判定した場合、「不一致」と判定する。
【００３４】
（ステップＳ１１１）：同時成立判定部１４は、ステップＳ１０５の入場判定部１２の判定結果とステップＳ１１０の退場判定部１３の判定結果とに基づいて、第１状態Ｓ１と第２状態Ｓ２との同時成立性を判定する。図７に判定に用いるテーブルの一例を示す。同時成立判定部１４は図７に示すようなテーブルを参照して、同時成立性のタイプを判定する。
【００３５】
タイプごとの同時成立性について、第１状態Ｓ１の継続期間と第２状態Ｓ２の継続期間との関係を示す図８〜図１２を参照して説明する。
タイプ１の場合、図８に示すように、第１状態Ｓ１と第２状態Ｓ２とが同時に成立し、各継続期間の入場タイミング（始期）および退場タイミング（終期）が、ともに一致する（表現：Ｓ１≡Ｓ２）。
タイプ２の場合、図９に示すように、第１状態Ｓ１と第２状態Ｓ２とが同時に成立し、各継続期間の始期が一致する（表現：Ｓ１⊃Ｓ２）。
タイプ３の場合、図１０に示すように、第１状態Ｓ１と第２状態Ｓ２とが同時に成立し、各継続期間の終期が一致する（表現：Ｓ１⊂Ｓ２）。
タイプ４の場合、図１１に示すように、第１状態Ｓ１と第２状態Ｓ２とが同時に成立し、各継続期間の始期および終期のいずれも一致するとは限らないが、各継続期間は重複する（表現：Ｓ１∋Ｓ２）。
タイプ５の場合、図１２に示すように、第１状態Ｓ１と第２状態Ｓ２とが同時に成立しないため、各継続期間は重複しない（表現：Ｓ１！Ｓ２）。
タイプ６の場合、第１状態Ｓ１と第２状態Ｓ２とが同時に成立するか否か、論理的には解析不可である（表現：×）。この場合は、実際に同時に成立するか否か、シミュレーションを行って解析を行う。
【００３６】
以上によって、第１状態Ｓ１と第２状態Ｓ２との同時成立性を解析することができる。なお、第１状態Ｓ１と第２状態Ｓ２とを他の状態に変えて上述のステップＳ１０１〜Ｓ１１１を繰り返し実行することにより、第１状態遷移構造および第２状態遷移構造の所望の状態の組み合わせについて、同時成立性を解析することができる。このような解析を行うことにより、図１３に示すような第１状態遷移構造および第２状態遷移構造の状態間の同時成立性の一覧を作成することができる。なお、図１３に示す例では、第１状態遷移構造における初期状態Ｄｅｆ１からの状態遷移と、第２状態遷移構造における初期状態Ｄｅｆ２からの状態遷移とについては、設計上、常に同じタイミングで発生するため、これ以外の場合は解析を行っていない（図１３の「−」）。このように、予め同時成立性が判明している状態遷移パターンについては、解析をしなくてもよい。
【００３７】
＜適用例＞
状態遷移解析システム１０による、車両搭載の制御システムの状態遷移構造の解析の例を説明する。第１制御システムの例を走行支援システムとし、第２制御システムの例をブレーキ制御システムとする。走行支援システムの状態遷移構造を表す情報の例を図１４に示す。ブレーキ制御システムの状態遷移構造を表す情報の例を図１５に示す。
【００３８】
走行支援システムは、「ブレーキペダルオフ、かつ、車速４０ｋｍ／ｈ以上、かつ、『＋ＲＥＳ』スイッチオン」という遷移条件１−１により、所定の速度内で前走車との車間距離を維持しながら追従走行を行う制御オン状態となる。また、走行支援システムは、「ブレーキペダルオン、または、（シフトポジション『Ｄ』または『Ｓの４レンジ以上』）から他のポジションにシフト、または、『ＣＡＮＣＥＬ』スイッチオン、または、メインスイッチオフ、または、電動パーキングブレーキ作動」という遷移条件１−２により、追従走行制御をキャンセルして制御オフ状態となる。
【００３９】
ブレーキ制御システムは、「ブレーキペダルオン」という遷移条件２−１により、アクチュエータを駆動しブレーキ操作を行う制御オン状態となり、「ブレーキペダルオフ」という遷移条件２−２により、制御オフ状態となる。
【００４０】
上述のステップをこの例に適用する。
（ステップＳ１０１）：入場判定部１２は、走行支援システムの制御オン状態を選択し、その入場条件である遷移条件１−１を特定する。また、入場判定部１２は、ブレーキ制御システムの制御オン状態を選択し、その入場条件である遷移条件２−１を特定する。
【００４１】
入場判定部１２は、走行支援システムの遷移条件１−１とブレーキ制御システムの遷移条件２−１とに共通する因子として「ブレーキペダル」を抽出する。
【００４２】
（ステップＳ１０２）：入場判定部１２は、共通因子があるため、ステップＳ１０３に進む。
【００４３】
（ステップＳ１０３）：入場判定部１２は、走行支援システムの遷移条件１−１とブレーキ制御システムの遷移条件２−１とが、論理的に同値であるか否かを判定する。論理式「〔ブレーキペダルオフ、かつ、車速４０ｋｍ／ｈ以上、かつ、『＋ＲＥＳ』スイッチオン〕≡（ブレーキペダルオン）＝真」は成立しないので、遷移条件１−１と遷移条件２−１とは同値でない。そのため、ステップＳ１０４に進む。
【００４４】
（ステップＳ１０４）：入場判定部１２は、走行支援システムの遷移条件１−１とブレーキ制御システムの遷移条件２−１とが、論理的に同時に成立することがありうるか否かを判定する。論理式「〔ブレーキペダルオフかつ車速４０ｋｍ／ｈ以上かつ『＋ＲＥＳ』スイッチオン〕かつ（ブレーキペダルオン）＝真」において、「ブレーキペダルオフかつブレーキペダルオン」は常に偽であるので、この論理式が成立することはなく、遷移条件１−１と遷移条件２−１とは同時に成立しない。
【００４５】
（ステップＳ１０５）：入場判定部１２は、ステップＳ１０２〜Ｓ１０４での判定結果に基づいて、遷移条件１−１と遷移条件２−１との関係を「不一致」と判定する。
【００４６】
（ステップＳ１０６）−（ステップＳ１１０）：退場判定部１３は、走行支援システムの制御オン状態の退場条件である遷移条件１−２およびブレーキ制御システムの制御オン状態の退場条件である遷移条件２−２を特定する。退場判定部１３は、ステップＳ１０１−Ｓ１０４における入場判定部１２の処理と同様に、遷移条件１−２と遷移条件２−２との関係を判定し、「不一致」と判定する。
【００４７】
（ステップＳ１１１）：同時成立判定部１４は、ステップＳ１０５の入場判定部１２の判定結果「不一致」と、ステップＳ１１０の退場判定部１３の判定結果「不一致」とに対応するタイプを図７のテーブルを参照して特定する。テーブルによれば、この場合の同時成立性は「タイプ５」であり、走行支援システムの制御オン状態とブレーキ制御システムの制御オン状態とは、同時に成立しないと判定することができる。これにより、前車両への追従走行制御とブレーキ操作とが同時に行われるという矛盾した車両動作が発生しないことが検証できる。
【００４８】
（効果）
以上のように、本発明によれば、２つの状態遷移構造にそれぞれ含まれる状態どうしの同時成立性を、入場条件どうし、および、退場条件どうしを論理的に解析することにより、遷移タイミングが同じ場合であっても異なる場合であっても、好適に解析することができる。また、状態遷移構造を表す情報を作成し記憶部に記憶させれば、各状態について順次網羅的にもれなく解析を行うことができるので、車両のような複数のシステムを含む総合システムの堅牢性の検証を好適に行うことができる。
【００４９】
なお、本発明は、状態遷移解析システムとして捉えるだけでなく、状態遷移解析装置の演算部が実行する状態遷移解析方法、プログラム等として捉えることも可能である。
【産業上の利用可能性】
【００５０】
本発明は、車両等の設計に用いる状態遷移解析システムに有用である。
【符号の説明】
【００５１】
１０    状態遷移解析システム
１１    記憶部
１２    入場判定部
１３    退場判定部
１４    同時成立判定部
【図１】
2019185481.tif 000003
【図２】
2019185481.tif 000004
【図３】
2019185481.tif 000005
【図４】
2019185481.tif 000006
【図５】
2019185481.tif 000007
【図６】
2019185481.tif 000008
【図７】
2019185481.tif 000009
【図８】
2019185481.tif 000010
【図９】
2019185481.tif 000011
【図１０】
2019185481.tif 000012
【図１１】
2019185481.tif 000013
【図１２】
2019185481.tif 000014
【図１３】
2019185481.tif 000015
【図１４】
2019185481.tif 000016
【図１５】
2019185481.tif 000017