(57)【要約】【課題】  モデル検査のためのモデル作成に特別のモデル記述言語の習得を要せず、動作仕様だけでなく制約条件も含んだモデルを作成するモデル検査支援装置を提供する。【解決手段】  システムの動作に関する仕様と制約条件とを表形式の情報として受け取る仕様入力部（１ａ）と、この表（２，３，４,１１）から抽出した記述に基づいて検証すべきシステムの動作と制約条件とを含んだモデル検査プログラム（６）を生成するモデル生成部（１ｂ，１ｃ）とを備え、表は、システムの状態遷移を記述する状態遷移表（２）と、システムの状態毎に、システム内の構成要素の取り得る値を記述する制約条件表（４）と、状態遷移表に記述したアクションの内容を記述するアクション表（３）と、システム外の外的作用によって発生する前記イベントの発生条件と当該イベントに対応するシステム内の構成要素の値の変化とを規定するイベント表（１１）とを有するモデル検査支援装置（１）である。【選択図】    図１
2010020555.tif 000002
【特許請求の範囲】
【請求項１】
システムの動作に関する仕様とシステムに求める性質である制約条件とを表形式の情報として受け取る仕様入力部と、
この表から抽出した記述に基づいて検証すべきシステムの動作と制約条件とを含んだモデル検査プログラムを生成するモデル生成部とを備え、
前記表は、
システムで発生するイベントとシステムの各状態に対応して、実行するアクション名と次に遷移する状態とを規定する状態遷移表と、
システムの各状態に対応して、システム内の構成要素がとるべき値を規定する制約条件表と、
前記アクション名に対応して、当該アクションの実行前後で成立していなければならない条件と当該アクションの内容とを、前記構成要素の値によって規定するアクション表と、
システム外の外的作用によって発生する前記イベントの発生条件と当該イベントに対応するシステム内の構成要素の値の変化を規定するイベント表とを有すること
を特徴とするモデル検査支援装置。
【請求項２】
前記モデル検査プログラムは、前記発生条件が成立して外的作用による前記イベントが発生したときは、当該イベントに対応するシステム内の構成要素に前記規定された値を設定するように記述されていることを特徴とする請求項１に記載のモデル検査支援装置。
【請求項３】
前記状態遷移表は、
前記イベントと前記システムの状態との組合せが発生しない不可状態と、
前記イベントと前記システムの状態との組合せが発生してもアクションを実行しない無視状態とを更に規定することを特徴とする請求項１に記載のモデル検査支援装置。
【請求項４】
前記モデル検査プログラムは、外的作用による前記イベントの前記発生条件が成立していないときは当該イベントを発生させないように記述されていることを特徴とする請求項１乃至３のいずれか１項に記載のモデル検査支援装置。
【請求項５】
前記モデル検査プログラムは、外的作用による前記イベントの前記発生条件が規定されていないときは当該イベントを常に発生可能な状態とするように記述されていることを特徴とする請求項４に記載のモデル検査支援装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査のためのモデル作成に特別のモデル記述言語の習得を要せず、動作仕様だけでなく制約条件も含んだモデルを作成することのできるモデル検査支援装置に関する。
【背景技術】
【０００２】
現在では、ソフトウエアは日常の生活を取り巻く様々な装置やシステムに組み込まれ複雑化・大規模化しており、自動車など交通機関等の生命の安全に関わる場合をはじめとしてその信頼性を確保することの重要性が声高く要求されている。
【０００３】
システム開発においては、まずソフトウエアの動作に関する設計が行われ、その後、その設計に基づくソフトウエアの作成及び検査が実行される。そのため、検査段階においてソフトウエアの設計段階で不具合が生じていたことが明らかになった場合は、ソフトウエアの設計にまで遡る修正作業、その修正作業に伴う開発工程の遅延、システム信頼性の低下などの問題が発生する。また人手による検査によってはこれらの設計時の検討の漏れ・設計書記載ミス・仕様の勘違いなどによる設計上の過ちを完全に検出することは困難で  ある。
【０００４】
そこでソフトウエアシステム開発において、設計段階におけるシステムを検証する形式手法のひとつとしてモデル検査技術が知られている。
【０００５】
このモデル検査技術は、状態遷移系としてモデル化されたシステムについて可能な全ての動作シーケンスを生成し、それぞれの動作シーケンスにおいて制約条件が満たされているかどうかを検証して、その結果を出力するものである。
【０００６】
ソフトウエアの作成後の検査工程において不具合が発見されたことによる設計にまで遡る修正作業が発生し、その修正作業に伴う開発工程の遅延が生じることを、未然に防ぐことができる。
【０００７】
また、このように設計段階において自動的・網羅的にモデル検査をすることによってシステムの信頼性を高め、システムの不具合、異常時や想定外の事態によって惹き起こされる不安定な挙動等を未然に防止することが出来る。
【０００８】
ところで、このモデル検査技術を適用するためには、特別のモデル記述言語（例えば、Promela言語）を用いてシステムのモデルを作成する必要があった。そこで、システムの動作に関する設計書からモデル記述言語で書かれたモデルを作成することができるモデル検査支援装置が開示されている（例えば、特許文献１参照）
【特許文献１】特開２００７−１１６０５号公報
【発明の開示】
【発明が解決しようとする課題】
【０００９】
しかし、特許文献１に記載の技術では、モデルを作成するための設計書は、図形形式の「変数の状態遷移関係で表した論理記述」で表現されていなければならず、一般的に作成されている設計書とは異なり、必ずしも使い易いものであるとは言えなかった。さらに、特許文献１に記載のモデル検査支援装置では検査のための制約条件を生成できないため、別途手作業で制約条件を作成することが必要であった。
【００１０】
本発明は、かかる事情に鑑みてなされたものであり、モデル検査のためのモデル作成に特別のモデル記述言語の習得を要せず、動作仕様だけでなく制約条件も含んだモデルを作成することのできるモデル検査支援装置を提供することを目的とする。
【課題を解決するための手段】
【００１１】
上記課題を解決するための、本発明に係るモデル検査支援装置は、システムの動作に関する仕様とシステムに求める性質である制約条件とを表形式の情報として受け取る仕様入力部と、この表から抽出した記述に基づいて検証すべきシステムの動作と制約条件とを含んだモデル検査プログラムを生成するモデル生成部とを備え、前記表は、システムで発生するイベントとシステムの各状態に対応して、実行するアクション名と次に遷移する状態とを規定する状態遷移表と、システムの各状態に対応して、システム内の構成要素がとるべき値を規定する制約条件表と、前記アクション名に対応して、当該アクションの実行前後で成立していなければならない条件と当該アクションの内容とを、前記構成要素の値によって規定するアクション表と、システム外の外的作用によって発生する前記イベントの発生条件と当該イベントに対応するシステム内の構成要素の値の変化を規定するイベント表とを有する。
【発明の効果】
【００１２】
本発明によれば、特別のモデル記述言語の習得を要せずに、動作仕様だけでなく制約条件も含んだモデル検査のためのモデルを作成することができる。
【発明を実施するための最良の形態】
【００１３】
［第１の実施の形態］  
図１は、本発明の実施の形態に係るモデル検査支援装置を用いたモデル検査の流れを示す図である。
【００１４】
ユーザは、システムの設計書に相当する状態遷移表２、アクション表３、制約条件表４、条件判定表５及びイベント表１１を作成し、これらをモデル検査支援装置１に入力する。  
本実施の形態に係るモデル検査支援装置１には、仕様入力部１ａ、検査項目生成部１ｂ、及びモデル記述生成部１ｃが設けられている。そして、モデル検査支援装置１には、更に状態遷移記憶部１ｄ、アクション記憶部１ｅ、制約条件記憶部１ｆ、条件判定記憶部１ｇ、モデル記述言語辞書１ｈ及びイベント記憶部１ｋが設けられている。
【００１５】
仕様入力部１ａは、入力されたこれらの表から所要の情報を抽出して、それぞれ状態遷移記憶部１ｄ、アクション記憶部１ｅ、制約条件記憶部１ｆ、条件判定記憶部１ｇ及びイベント記憶部１ｋに格納する。検査項目生成部１ｂ及びモデル記述生成部１ｃは、状態遷移記憶部１ｄ、アクション記憶部１ｅ、制約条件記憶部１ｆ、条件判定記憶部１ｇ及びイベント記憶部１ｋに格納された情報に基づいて、特別のモデル記述言語で書かれたモデル（以下、「モデル検査プログラム」という。）を生成する。
【００１６】
モデル記述言語辞書１ｈは、モデル検査プログラムを生成する際に参照される辞書であり、これらの表に記載される自然言語で使用される演算子とモデル記述言語で使用される演算子との対応関係を格納している。
【００１７】
なお、検査項目生成部１ｂは主として動作に関する仕様を取扱い、モデル記述生成部１ｃは主として制約条件に関する仕様を取扱うが、実際の動作ではこれらが協働してモデル検査プログラム６を生成する。
【００１８】
生成されたモデル検査プログラム６は、モデル検査器７において検証が行われ、検査結果８として出力される。検査結果８には、モデル検査プログラム６が制約条件を満たしているかどうか、設計内容に矛盾点、不足点が存在するかどうかについての検査結果が記載される。
【００１９】
なお、モデル検査支援装置１、モデル検査器７は、ハードウエアに限られず、ソフトウエアで構成しても良い。また、モデル検査支援装置１に入力される各表２〜５及び１１は、本実施の形態ではExcel（登録商標）を用いて作成しているが、これに限られずWord（登録商標）、Visio（登録商標）等の他の言語処理手段、ツールを用いて作成しても良い。
【００２０】
続いて、モデル検査支援装置１に入力される上述の各表２〜５及び１１について説明する。  
図２は、状態遷移表２の記述例を示す図である。状態遷移表２は、システムの状態遷移を記述した表である。
【００２１】
状態遷移表２には、状態遷移表名欄２ａ、状態名欄２ｂ、入退場アクション欄２ｃ、イベント名欄２ｄ、及びアクション欄２ｅが設けられている。  
状態遷移表名欄２ａには、この状態遷移表の名称が日本語または英数字等による表記で入力される。状態名欄２ｂは、このシステムが取り得る状態毎に分類され、その状態名が日本語または英数字等による表記で入力される。入退場アクション欄２ｃには、上述の状態に入退場する際の動作を規定し、入場アクションと退場アクションとが日本語または英数字等による表記で入力される。イベント名欄２ｄには、このシステムで発生するイベント毎に分類され、そのイベント名が日本語または英数字等による表記で入力される。アクション欄２ｅには、イベントと状態の組合せにおいて実行されるアクションと遷移先の状態名が入力される。
【００２２】
次に、アクション欄２ｅの内容について説明する。アクション欄２ｅは、基本構成として、上段と下段を備えている。
【００２３】
図３は、アクション欄２ｅの下段の内容を説明する図である。  
下段には、所定のイベントと状態の組合せの場合に実行するアクションのアクション名を記載する。このアクション名の処理内容は、後述するアクション表３に規定されている。  
複数のアクションを実行する場合は、このアクション欄２ｅの下段に複数のアクション名を改行して記述すれば良い。さらに、そのアクションを実行するか否かに条件が必要な場合は、その条件（以下、「ガード条件」という）を括弧（［  ］）で囲んで記述し、その後にアクション名を記載すれば良い。
【００２４】
図３に示すアクションでは、「電源ＯＦＦ」の状態で「電源ボタン押下」によるイベントが発生したときは、電源ＯＮ処理を実行するとともに、ガード条件である「ディスク有」が成立している場合は再生初期化処理を実行することが規定されている。
【００２５】
図４は、アクション欄２ｅの上段の内容を説明する図である。  
上段には、下段のアクションを実行した後、次にどの状態に遷移するのかを状態名で記述する。条件によって遷移先が異なる場合は、異なる遷移先毎に改行して記述する。遷移に条件が必要な場合は、ガード条件を括弧（［  ］）で囲んで記述し、その後に遷移先を記載すれば良い。  
図４に示す遷移では、図３に示すアクションが実行された後は、ガード条件「ディスク有」が成立している場合は「停止」状態に遷移し、ガード条件「ディスク無」が成立している場合は「ディスクなし」状態に遷移することが規定されている。
【００２６】
なお、アクション欄２ｅに「／」が記入されている場合は、「無視」として扱われる。「無視」は、所定のイベントと組合せは有り得るが、何も処理をしないことを表す。アクション欄２ｅに「×」が記入されている場合は、「不可」として扱われる。「不可」は、所定のイベントと状態の組合せはありえないことを示している。
【００２７】
図５は、入場アクション、退場アクションの内容を説明する図である。  
入場アクションは、この状態に遷移した際に実行されるアクションであり、退場アクションは次の状態へ遷移する前に実行されるアクションである。  
ここで、複数のアクションを実行する場合は、それらのアクション毎に改行して記述すれば良い。さらに、そのアクションを実行するか否かに条件が必要な場合は、ガード条件を括弧（［  ］）で囲んで記述し、その後にアクション名を記載すれば良い。
【００２８】
アクションの実行は、アクション欄２ｅ下段のアクション→退場アクション→入場アクションの順番で実行される。図５に示す例では、状態１でイベント１が発生した場合、アクション３→アクション２→アクション４の順序で実行される。
【００２９】
なお、アクション欄２ｅの上段に現在の状態名を記述した場合を、「自己遷移」と呼ぶ。自己遷移の場合は状態自体は変化しないものの遷移の処理は行われ、かつ入場アクションと退場アクションが実行される。アクション欄２ｅの上段に「−（ハイフン）」が記述されあるいは空白である場合を、「内部遷移」と呼ぶ。内部遷移の場合は、アクション欄２ｅ下段のアクションは実行されるが、退場アクション、入場アクションは実行されない。
【００３０】
図６は、アクション表３の記述例を示す図である。アクション表３には状態遷移表２のアクション欄２ｅの下段および入退場アクション欄２ｃに記述した「アクション」の内容を「事前条件」、「処理内容」、「事後条件」に分類して、システム内の構成要素の状態を記述する。
【００３１】
アクション表３には、アクション名欄３ａ、事前条件欄３ｂ、処理内容欄３ｃ、及び事後条件欄３ｄが設けられている。  
アクション名欄３ａには、状態遷移表２のアクション欄２ｅの下段および入退場アクション欄２ｃに記載したアクション名と同一の名称が日本語または英数字等による表記で入力される。
【００３２】
事前条件欄３ｂには、アクションの処理内容を実行するために成立していなければならない構成要素の値の条件を記載する。処理内容欄３ｃには、アクションの実行によって構成要素の値をどのように変化させるかを記載する。事後条件欄３ｄには、アクションの内容が実行された後に成立すべき構成要素の値の条件を記載する。  
これら、それぞれの欄内の条件または内容は自然言語、式などで記述することができる。また、それぞれの欄内に複数の条件または内容がある場合には、改行して記述すれば良い。条件または内容がない場合は、その欄には「−（ハイフン）」あるいは空白を記述する。
【００３３】
ここで、図６の事前条件欄３ｂ及び事後条件欄３ｄに記載されている「＝」は「条件」を表し、処理内容欄３ｃに記載されている「←」は、「代入」を表している。
【００３４】
図６に示すアクションでは、次のことが規定されている。「ディスク回転開始処理」を実行するためには、事前条件として、構成要素である「ディスク」の値が「あり」でかつ「ディスク回転」の値が「停止」にあることが必要である。そして、処理内容は、「ディスク回転」の値を「回転中」とすることであり、その処理の結果である事後条件は、「ディスク回転」の値が「回転中」となっていることが必要である。
【００３５】
図７は、条件判定表５の記述例を示す図である。条件判定表５には、状態遷移表２の各欄の括弧内に記載したガード条件の内容を記述する。  
条件判定表５は、条件判定名欄５ａ及び条件内容欄５ｂを備えている。  
条件判定名欄５ａには、状態遷移表２の各欄の括弧内に記載したガード条件の名称が日本語または英数字等による表記で入力される。  
条件内容欄５ｂには、条件判定名の条件判定内容を記載する。これは、具体的な値、数式などの他、自然言語を用いて内容を記述しても良い。内容がない場合は、その欄には「−（ハイフン）」あるいは空白を記述する。
【００３６】
例えば、図７では、「開始トラックである」という条件は、構成要素「トラック番号」の値が「１」となっていることであり、「開始トラックでない」という条件は、構成要素「トラック番号」の値が「１より大きい」ことであることが規定されている。
【００３７】
図８は、制約条件表４の記述例を示す図である。制約条件表４には、検証対象のシステムの各状態における構成要素が取り得る値を記述する。  
制約条件表４には、構成要素名欄４ａ、状態名欄４ｂ、及び制約条件内容欄４ｃが設けられている。  
構成要素名欄４ａには、各構成要素の名称が日本語または英数字等による表記で入力される。状態名欄４ｂには、状態遷移表２の状態名と同じ名称を記載する。制約条件内容欄４ｃには、ある構成要素がある状態でどのような値になっていなければないかという制約条件を記述する。これは、具体的な値や名称などの他に自然言語で記述しても良い。
【００３８】
例えば、図８では、状態「電源ＯＦＦ」では、構成要素「電源」の値は「ＯＦＦ」、構成要素「音声出力」の値は「なし」、構成要素「ディスク回転」の値は「停止」となっていなければならず、構成要素「ディスク」、「トラック番号」、「総トラック数」の値には制約がないことが規定されている。
【００３９】
図９は、イベント表１１の記述例を示す図である。イベント表１１には、イベントが発生するための条件と、イベントの発生によるシステム内の構成要素の値の変化が記述される。
【００４０】
イベント表１１には、イベント名欄１１ａ、発生条件欄１１ｂ及び作用内容欄１１ｃが設けられている。  
イベント名欄１１ａには、状態遷移表２のイベント名欄２ｄに記載したイベント名と同一の名称が日本語または英数字等による表記で入力される。発生条件欄１１ｂには、そのイベントが発生するために成立していなければならない条件、即ち、発生条件が記載される。作用内容欄１１ｃには、イベントが発生したことによるシステム内の構成要素の値の変化、即ち作用内容が記載される。この作用内容は、システムが能動的に変化させたものでなく、ユーザによる操作などの外的作用によって変化したものである。
【００４１】
図９に示すイベント表１１によれば、イベント「ディスク挿入」は、既にディスクがＣＤプレーヤ内にある場合には発生せず、イベント「トラック終端到達」は、ディスクがＣＤプレーヤ内にある場合しか発生しない。  
ここで、イベント「ディスク挿入」「トラック終端到達」以外のイベントについては、発生条件が指定されていないが、これはイベント「ディスク挿入」「トラック終端到達」以外のイベントはいつでも発生することができることを表している。
【００４２】
次に、本発明の実施の形態に係るモデル検査支援装置を用いてモデル検査プログラムを生成する動作について説明する。  
図１０は、モデル検査プログラムの生成手順を示すフロー図である。
【００４３】
ステップＳ０１において、ユーザは状態遷移表２、アクション表３、制約条件表４及びイベント表１１をモデル検査支援装置１に入力する。  
図１１は、モデル検査支援装置１に入力される各表の記載例を示す図である。本図では電源ボタンのＯＮ・ＯＦＦ、ディスクの挿入、次トラックボタン押下による動作について説明するが、説明の簡略化のため条件判定表５を用いない状態での動作について記載している。
【００４４】
なお、本実施の形態では、状態遷移表２、アクション表３、制約条件表４及びイベント表１１は、上述のようにＥｘｃｅｌ（登録商標）等の他の言語処理手段やツールを用いて生成するが、入力方法については種々の形態をとる事ができる。例えば、ユーザが不図示の入力装置からデータを入力しても良く、作成済みの各表を不図示の記憶媒体を介して入力しても良く、外部の他システムから不図示の通信回線を介して作成済みの各表をモデル検査支援装置１に伝送しても良い。また、状態遷移表２以外は、必要なデータが入力されれば、必ずしも表形式で作成されなくても良い。
【００４５】
モデル検査支援装置１では、仕様入力部１ａが起動して、入力された各表からデータを抽出して、それぞれ状態遷移記憶部１ｄ、アクション記憶部１ｅ、制約条件記憶部１ｆ、条件判定記憶部１ｇ及びイベント記憶部１ｋに格納する。この際に、図２に示す状態遷移表２のアクション欄２ｅの上段に記述された遷移先の状態名が状態名欄２ｂに記述されているかを確認する。アクション欄２ｅの上段に記述された遷移先の状態名が状態名欄２ｂに存在しない場合には、仕様入力部１ａが異常と判断し、モデル検査プログラムを生成せずに動作を終了する。同様に、状態遷移表２のアクション欄２ｅの下段に記述されたアクション名がアクション表３のアクション表名欄３ａに記述されているか、状態遷移表２のアクション欄２ｅの上段及び下段に括弧（［  ］）で囲んで記述されたガード条件が条件判定表５の条件判定名欄５ａに記述されているか、アクション表３の事前条件欄３ｂ、処理内容欄３ｃ、事後条件欄３ｄ及び条件判定表５の条件内容欄５ｂに記述された構成要素名が制約条件表４の構成要素名欄４ａに記述されているか、またイベント表１１のイベント名欄１１ａに記載したイベント名が状態遷移表２のイベント名欄２ｄに記述されているかを確認し、存在しない場合には仕様入力部１ａがエラーを異常と判断し、モデル検査プログラムを生成せずに動作を終了する。
【００４６】
検査項目生成部１ｂ及びモデル記述生成部１ｃは、状態遷移記憶部１ｄ、アクション記憶部１ｅ、制約条件記憶部１ｆ、条件判定記憶部１ｇ及びイベント記憶部１ｋに格納された各表のデータに基づいて、モデル検査プログラム６を生成する。アクションや制約条件、条件判定の記述において自然言語が用いられている場合には、適宜、モデル記述言語辞書1ｈを参照し、対応するモデル記述言語に変換する。
【００４７】
なお、以下特に明示しない場合は、検査項目生成部１ｂ及びモデル記述生成部１ｃが協働してモデル検査プログラムの各部を生成するものとする。
【００４８】
ステップＳ０２において、モデル検査プログラム６の内、図２３に示す状態遷移部６ｃの作成を開始する。先ず、状態遷移記憶部１ｄに格納された状態遷移表２のイベント名欄２ｄに記載されているイベント名毎に、そのイベントを処理するブロックをモデル検査プログラム６に生成する。  
図１２では、イベント「電源ボタンＯＮ」、「電源ボタンＯＦＦ」、「ディスク挿入」、「次トラックボタン押下」の異なるブロックが生成されている。即ち、発生したイベントを表す変数eventの値によってブロックが分けられている。
【００４９】
ステップS０３において、生成したそれぞれのブロックの内部に、状態遷移記憶部１ｄに格納された状態遷移表２の状態名欄２ｂにある状態ごとのブロックを生成する。  
図１３では、状態名である「電源ＯＦＦ状態」、「待機状態」、「ディスクあり状態」のブロックが生成されている。即ち、現在の状態を表す変数stateによって、さらに３つのブロックに分けられている。
【００５０】
ステップS０４において、生成した状態の各ブロックに、状態遷移記憶部１ｄに格納された状態遷移表２のアクション欄２ｅの記述に従い、ステップＳ０６で作成するアクション部６ａの呼び出し処理を生成する。  
図１４では、イベントが「電源ボタンＯＮ」で状態が「電源ＯＦＦ状態」のブロックに、処理内容「ランプ点灯処理」の呼出しと遷移先「待機状態」が記載されている。また、イベントが「電源ボタンＯＦＦ」で状態が「待機状態」のブロックに、処理内容「ランプ消灯処理」の呼出しと遷移先「電源ＯＦＦ状態」が記載されている。さらに、イベントが「電源ボタンＯＦＦ」で状態が「ディスクあり状態」のブロックに、処理内容「ディスク排出処理」、「ランプ消灯処理」の呼出しと遷移先「電源ＯＦＦ状態」が記載されている。
【００５１】
ステップＳ０５において、状態遷移記憶部１ｄに格納された状態遷移表２の状態名欄２ｂにある状態ごとのブロックを新たに生成する。そして、生成した状態のブロックに、ステップS０７で作成する制約条件検査部６ｂの呼出処理を生成する。即ち、生成した状態毎に制約条件の良否が検査される。    
図１５では、状態名である「電源ＯＦＦ状態」、「待機状態」「ディスクあり状態」のブロックが生成されている。即ち、遷移先を表す変数nextstateによって場合わけがなされ、遷移先の状態ごとにブロックが生成されている。そして、そのブロック毎に状態名が制約条件を検査するための呼出名として作成されている。
【００５２】
ステップS０６において、モデル検査プログラム６の内、アクション部６ａの作成を開始する。アクション記憶部１ｅに格納されたアクション表３のアクション名欄３ａに記載されたアクション名でブロックを分けて作成する。そして、生成したブロックにアクション記憶部１ｅに格納されたアクション表３の記述に従って、内部の処理を生成する。  
図１６では、アクション名の「次トラック処理」、「ディスク受入処理」に対応してブロックが作成されている。そして、「次トラック処理」のブロックに、アクション記憶部１ｅに格納された事前条件欄３ｂの内容がモデル記述言語であるPromela言語を用いてassert文として生成される。処理内容欄３ｃの内容がPromela言語を用いて変換して生成される。事後条件欄３ｄの内容がPromela言語を用いてassert文として生成される。「ディスク受入処理」のブロックについても、同様に処理される。
【００５３】
なお、assert文として生成される内容は、例えば、事前条件であれば、処理を実施する前には「トラック番号は総トラック数より少なくなければならない」と解釈される。
【００５４】
ここまでの処理によって、モデル検査プログラムの内、アクション部６ａが作成された。
【００５５】
ステップS０７において、モデル検査プログラム６の内、制約条件検査部６ｂの作成を開始する。制約条件記憶部１ｆに格納された制約条件表４の状態名欄４ｂに記載された状態名でブロックを分けて作成する。
【００５６】
図１７では、状態名の「電源ＯＦＦ状態」、「待機状態」、「ディスクあり状態」に対応してブロックが作成されている。
【００５７】
ステップＳ０８において、生成したブロックに制約条件検査のために制約条件記憶部１ｆに格納された制約条件内容欄４ｃの記述を用いたブロックを生成する。  
図１８では、「電源ＯＦＦ状態」のブロックに、制約条件である「ランプ」が「消灯」、「ディスク」が「なし」、「トラック番号」が「０」、「電源ボタン」が「押上」でなければならないことを規定するassert文が生成される。また、「待機状態」のブロックに、制約条件である「ランプ」が「点灯」、「ディスク」が「なし」、「トラック番号」が「０」、「電源ボタン」が「押下」でなければならないことを規定するassert文として生成される。  
このように、状態毎に複数の構成要素を制約条件として記述することになる。
【００５８】
ここまでの処理によって、モデル検査プログラム６の内、制約条件検査部６ｂが作成された。
【００５９】
ステップＳ０９において、イベント記憶部１ｋに格納されたイベント表１１のイベント名欄１１ａに記載されたイベントごとのブロックを生成する。生成したブロックにイベント記憶部１ｋに格納された作用内容欄１１ｃに従った内部の処理を記述して、イベント内容部６ｆを作成する。
【００６０】
図１９では、イベント名の「電源ボタンＯＮ」、「電源ボタンＯＦＦ」、「ディスク挿入」、「次トラックボタン押下」に対応してブロックが生成されている。  
そして図２０では、生成したブロック「電源ボタンＯＮ」の内部の処理として「電源ボタン＝押下」、「電源ボタンＯＦＦ」の内部の処理として「電源ボタン＝押上」が記載されている。ここで、作用内容の記載がない「ディスク挿入」、「次トラックボタン押下」では、ブロックのみが生成されている。
【００６１】
ステップＳ１０において、モデル検査プログラムの内、イベントを非決定的に発生させるイベント発生部６ｄを、状態遷移記憶部１ｄに格納された状態遷移表２のイベント名欄２ｄを用いて生成する。更に、各イベントの発生条件にイベント記憶部１ｋに格納されたイベント表１１の発生条件欄１１ｂに記載された条件を付与し、イベント内容部の呼出処理を生成する。
【００６２】
図２１では、イベントを表す変数eventの値に「電源ボタンON」「電源ボタンOFF」「ディスク挿入」「次トラックボタン押下」を設定している。そして、イベント表１１でイベント発生条件が指定されているイベント「電源ボタンＯＮ」、「電源ボタンＯＦＦ」に関しては、その発生条件が出力され、イベント発生条件が指定されていないイベント「ディスク挿入」、「次トラックボタン押下」に関しては、常に発生可能であることを示す「true」が出力される。  
そして、図２２では、そのイベント発生部６ｄにイベント作用内容の呼び出し部分が生成される。
【００６３】
図２３は、上述の手順によって作成されたモデル検査プログラム６の基本構成を示す図である。  
状態遷移表２、アクション表３、制約条件表４及びイベント表１１に基づいて、それらのデータ間の対応付けがなされたアクション部６ａ、制約条件検査部６ｂ、状態遷移部６ｃ、イベント発生部６ｄ及びイベント内容部６ｆが生成されている。なお、条件判定部６ｅについては後で詳細に説明する。
【００６４】
なお、状態遷移部６ｃ、アクション部６ａ、制約条件検査部６ｂ、イベント発生部６ｄイベント内容部６ｆを生成する順序については、本実施の形態に限られない。
【００６５】
なお、モデル検査プログラムの生成にあたり、変数や定数、プロセス等の宣言については、それを使用するモデル記述言語の規約に基づいて適宜行うものとする。
【００６６】
[第２の実施の形態]
第２の実施の形態では、モデル検査プログラムの生成において、条件判定表５、状態遷移表２の入退場アクションなどを処理する動作について説明する。従って、第１の実施の形態と同一の部位には同一の符号を付してその詳細の説明は省略する。
【００６７】
図２４は、モデル検査支援装置１に入力される各表の記載例を示す図である。図１１に示す第１の実施の形態と比して、条件判定表５が読み込まれる点と、状態遷移表２には「電源ＯＦＦ状態」のアクション欄２ｅにガード条件として[ディスク無]、[ディスク有]が記載されている点が異なっている。
【００６８】
図１０に示すモデル検査プログラム生成フローのステップＳ０４において、生成した状態の各ブロックに、状態遷移記憶部１ｄに格納されている状態遷移表２のアクション欄２ｅにある各欄の内容を記載する。  
図２５では、イベントが「電源ボタンＯＮ」で状態が「電源ＯＦＦ状態」のブロックに、処理内容「ランプ点灯処理」、遷移先「[ディスク無]待機状態」と「[ディスク有]ディスクあり状態」が記載されている。  
先ず、状態遷移表２の状態名欄２ｂにある状態ごとのブロックを新たに生成する。そして、生成した状態のブロックにアクション欄２ｅ下段にある「ランプ点灯処理」の呼出処理を記載する。
【００６９】
次に、アクション欄２ｅ上段の条件を判定する条件判定部６ｅの呼出処理を生成し、その判定結果によって遷移先を変化させる処理を記載する。図２５では、「ディスク無」が成立する場合には遷移先は「待機状態」となり、「ディスク有」が成立する場合には遷移先は「ディスクあり状態」であることが規定されている。
【００７０】
図２６では、イベントが「ディスク挿入」で状態が「電源ＯＦＦ状態」のブロックに、処理内容「[ディスク無]ディスク受入処理」と「ランプ点灯処理」、遷移先「ディスクあり状態」が記載されている。
【００７１】
状態遷移表２のアクション欄２ｅ下段で条件判定が使用されている場合は、その条件を判定する条件判定部６ｅの呼出処理を生成し、その判定結果によって対応するアクションを実行するか否かを変化させる処理を記載する。図２６では、「ディスク無」が成立する場合にのみ「ディスク受入処理」が実行されることが規定されている。
【００７２】
次に条件判定表５の処理について説明する。  
図１０に示すモデル検査プログラム生成フローのステップＳ０８が終了した後に、条件判定表５の処理を実行する。
【００７３】
条件判定表処理では、条件判定記憶部１ｇに格納されている条件判定表５の条件判定名でブロックを生成し、生成したブロック内部に条件判定表５の内容に従って処理名を記載する。  
図２７では、条件判定名の「ディスク有」、「ディスク無」に対応してブロックが作成され、それぞれのブロックに、条件判定表５の内容が規定されている。
【００７４】
なお、この条件判定表５に基づいて生成されたプログラムの部分は、図２３に示すモデル検査プログラム６に条件判定部６ｅとして追加される。この条件判定部６ｅは、状態遷移部６ｃの前に生成される。
【００７５】
次に、「不可」と「無視」について説明する。  
「不可」は、アクション欄２ｅに「×」が記入されている場合であり、この「不可」となっているイベントと状態の組合せはありえないことを示している。
【００７６】
図２８では、「待機状態」と「ディスクあり状態」とでは、イベント「電源ボタンＯＮ」が発生してはならず、「電源ＯＦＦ状態」では、イベント「電源ボタンＯＦＦ」が発生してはならないことが記載されている。  
アクション欄２ｅが「不可」となっている場合は、ステップＳ０４において生成した状態の各ブロックにはassert文が挿入される。これによって、このブロックが実行されてはならないことが表される。
【００７７】
「無視」は、アクション欄２ｅに「／」が記入されている場合であり、この「無視」となっているイベントと状態の組合せはあり得るが、何も処理をしないことを示している。  
この場合には、そのアクション欄２ｅに対応するブロックには何も書き込まれない。
【００７８】
次に入退場アクションについて説明する。  
入場アクションはこの状態に遷移した際に実行されるアクションであり、退場アクションは次の状態へ遷移する前に実行されるアクションである。  
図２９に示す状態遷移表２では、「電源ＯＦＦ状態」へ遷移する際には、入場アクションとして「ランプ消灯処理」が実行され、「電源ＯＦＦ状態」から他の状態へ遷移する際には、退場アクションとして「ランプ点灯処理」が実行されることが規定されている。
【００７９】
この入退場アクションが状態遷移表２に記載されていた場合、図２３に示すモデル検査プログラム６の状態遷移部の最後に入退場アクションを処理するブロックが生成される。入場アクションの処理ブロック、退場アクションの処理ブロックの内部には、状態遷移表２の状態に対応するブロックが生成され、その中に入場アクション欄、退場アクション欄に記述された内容がモデル記述言語を用いて生成される。
【００８０】
続いて、イベント表１１の役割について、キッチンタイマに組み込むプログラムの検査を例として詳細に説明する。
【００８１】
図３０は、キッチンタイマ２０の構成を示すブロック図である。  
キッチンタイマ２０には、スタートボタン２１、ストップボタン２２及びアラーム（警報器）２３が設けられている。そして、ＣＰＵ２５が、スタートボタン２１、ストップボタン２２の操作信号を受け取って、タイマ２６との間で情報の授受を行い、アラーム２３の警報吹鳴動作を制御する。
【００８２】
キッチンタイマ２０の仕様は次のとおりである。  
スタートボタン２１を押下すると、タイマ２６が起動し、一定時間が経過するとアラーム２３が鳴動する。アラーム２３の鳴動中にストップボタン２２を押下するとアラーム２３の鳴動が停止する。アラーム２３の鳴動中に一定時間が経過するとアラーム２３の鳴動が停止する。  
アラーム２３の鳴動が停止した後は、タイマ２６は停止しており、タイマ２６の起動には再びスタートボタン２１を押下する。スタートボタン２１の押下後、アラーム２３の鳴動前にストップボタン２２を押下すると、タイマ２６は停止する。
【００８３】
キッチンタイマ２０に内蔵されているタイマ２６の仕様は次のとおりである。  
タイマ２６がＣＰＵ２５からのカウンタ設定信号を受け取ると、タイマ２６は直ちにカウントダウンを開始する。タイマ２６に対してＣＰＵ２５が割込許可信号を出力していた場合は、タイマ２６はカウントがゼロになるとタイマ割込信号をＣＰＵ２５に出力する。
【００８４】
タイマ割込信号がＣＰＵ２５に出力されても、タイマ２６は自動的に割込禁止にならない。再びカウンタ設定がされれば、タイマ２６は直ちにカウントダウンを開始し、タイマ割込信号を発生する。
【００８５】
図３１は、キッチンタイマ２０を設計した例を示す図である。  
上述の動作を規定した、状態遷移表２、制約条件表３、アクション表４及びイベント表１１の内容が示されている。この各表に従って生成されたモデル検査プログラム６をモデル検査器７で検査した結果は「良好」であり、不具合個所は存在していない。
【００８６】
しかし、イベント表１１を用いずに、即ち発生条件欄１１ｂ、作用内容欄１１ｃをブランクとして生成されたモデル検査プログラム６では、モデル検査器７での検査において、従来装置の場合、次のようなエラーが指摘される。
【００８７】
それは、「待機中」の状態で「スタートボタン押下」イベントが発生しないうちに「タイマ割込」イベントが発生し「アラーム中」の状態に遷移したケースで、割込みがDISABLEとなっているというものである。即ち、制約条件表３では、「アラーム中」の状態において割込はENABLEとなっていなければならないと定義されていることに違反しているとの警告である。  
しかしながら、そもそも「待機中」の状態において「スタートボタン押下」イベントが発生する前には「タイマ割込許可」アクションは実行されていないため「タイマ割込」イベントが発生することは不合理である。即ち、モデル検査装置７は、有りえない事象を検知してエラーを発生していることになる。
【００８８】
この理由は、全てのイベントが常に発生し得るものとして検査を進めたため、本来発生し得ない状況でのイベント発生を契機とした制約条件違反が誤って検出されたことによる。一般的に次のような状況において同様の誤検出の可能性がある。  
即ち、これまで検査対象システム内の構成要素の値はシステムの能動的な処理（アクション）によってのみ変化した。システムが「閉じた系」である場合には、システム内部で構成要素の値は整合がとれている。しかし、システムが「開いた系」であり、システム外部からの作用（外的作用）によってシステム内の構成要素の値が受動的に変化する可能性がある場合、構成要素の値が矛盾する結果、制約条件の違反が誤って検出される可能性がある。
【００８９】
以上のような従来装置の不具合を排除するために、発明者らはエラー発生防止の要件について根本に立ち返った検討を重ね、つぎのような対応策を立案した。  
(1)あり得ないイベント発生による誤った制約違反の検出を排除するため、イベントの発生条件を指定可能とする。  
(2)システム内の構成要素の値の不正による誤った制約違反の検出を排除するため、イベント発生に伴うシステム内の構成要素の値の変化を定義可能とする。
【００９０】
イベント表１１は、この外的作用による不具合を排除するために設けられたものである。  これによって、システムとシステムに作用する外部とを一つの閉じた系として検査することにより、開いた系であるシステムのみを検査対象とした場合に生じた誤った制約違反の検出をなくすことができる。
【００９１】
図３１に示すイベント表１１では、「割込」がENABLEのときのみ「タイマ割込」イベントが発生可能となるように「発生条件」が定義されている。これによって、状態遷移表２と組み合わせて解釈すると、「スタートボタン押下」イベントが発生し、「タイマ割込許可」アクションを実行した後にのみ「タイマ割込」イベントが発生可能と定義されている。  
なお、「タイマ割込」イベント発生に伴うシステム内の構成要素の値の変化は、「作用内容」で定義することができる。
【００９２】
さらにこのイベント表１１を使用することによって、「不可」と「無視」の検査機能を充実することが可能となる。  
上述のようにこれまでは、全てのイベントが常に発生し得るものとして検査を進めたため、到達することのない「不可」も常に到達可能となっていた。従って、到達することのある「無視」と区別した検査ができなかった。  
ところで、イベント表１１において、イベントの発生条件を指定可能としたことによって、「不可」と「無視」とを区別し、不可への到達性の検査が可能となる。
【００９３】
図３２は、イベント表を利用した不可への非到達性検査例を示す図である。  
この自動販売機では、硬貨を投入できるのは、自動販売機に保持中の硬貨が無いか１枚だけ保持している場合である。従って、自動販売機に保持中の硬貨が２枚以上ある場合に「百円硬貨投入」イベントが発生することはない。しかしながら、これまでの検査ではこの「不可」も到達可能となっていたため、設計上に問題があるかどうかをその都度確認する必要があった。  
これに対し、図３２に示すようにイベント表１１の「百円硬貨投入」イベントの発生条件に、「保持中の硬貨が２枚未満」と定義することによって、不可への非到達性が実現されているかどうかを検査することが可能となる。
【００９４】
［実施の形態の効果］  
本実施の形態のモデル検査支援装置では、以下に示す特徴的な機能を備えている。
【００９５】
モデル検査プログラムの生成に必要なデータは、設計書の形式で作成されている。例えば、状態遷移表のフォーマットは、組込み系の開発において一般的に使用されている設計書の書き方に対応している。  
このように、ドキュメントからモデル検査プログラムを自動生成できるためモデル記述言語の習得が不要となっている。
【００９６】
また、設計書からモデル検査プログラムを自動生成することにより、設計書の作成後に、人手によるモデル検査プログラムの作成を経ることなく、直ちにモデル検査を実施することができる。
【００９７】
また、独自のアクション表と制約条件表とを導入し、モデル検査プログラムの生成に必要なデータとして制約条件の記載を可能としている。この結果、検証すべき制約条件をモデル検査プログラムの中に自動で生成することができる。
【００９８】
制約条件表では、システムに求められる性質が、システムの状態と構成要素の値の組合せによって明確に示される。そのため、制約条件の記載漏れによって、仕様があいまいになることを防ぐことができる。
【００９９】
アクション表では、アクションの内容だけではなく、事前条件と事後条件について記述することにより、動作仕様だけではなく制約条件についても簡潔に漏れなく記述し、モデル検査によって確認することができる。
【０１００】
イベント表では、イベントごとの発生条件を指定可能とすることによってあり得ないイベント発生による誤った制約違反の検出を排除することができ、更に「不可セル」への非到達性の検査を可能とすることができる。また、イベント発生に伴うシステム内の構成要素の値の変化を定義可能とすることによって、システム内の構成要素の値の不正による誤った制約違反の検出を排除することができる。
【０１０１】
本実施の形態に係るモデル支援装置はこのような特徴を有しているが、もちろんモデル記述言語を習得している人も有効に利用することが可能である。例えば、モデル検査プログラムの生成に必要なデータは、モデル記述言語（例えば、Promela言語）で記載しても良い。図３３には、アクション表の、「事前条件」、「処理内容」、「事後条件」をモデル記述言語で作成した例を示している。モデル記述言語を使うことで、自然言語よりも単純で厳密な記述をすることができる。
【０１０２】
なお、上述の実施の形態で説明した各機能は、ハードウエアを用いて構成しても良く、また、ソフトウエアを用いて各機能を記載したプログラムをコンピュータに読み込ませて実現しても良い。また、各機能は、適宜ソフトウエア、ハードウエアのいずれかを選択して構成するものであっても良い。
【０１０３】
更に、各機能は図示しない記録媒体に格納したプログラムをコンピュータに読み込ませることで実現させることもできる。ここで本実施の形態における記録媒体は、プログラムを記録でき、かつコンピュータが読み取り可能な記録媒体であれば、その記録形式は何れの形態であってもよい。
【０１０４】
なお、この発明は、上記実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合せにより種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。更に、異なる実施形態に亘る構成要素を適宜組み合せてもよい。
【図面の簡単な説明】
【０１０５】
【図１】本発明の実施の形態に係るモデル検査支援装置を用いたモデル検査の流れを示す図。
【図２】状態遷移表の記述例を示す図。
【図３】アクション欄の下段の内容を説明する図。
【図４】アクション欄の上段の内容を説明する図。
【図５】入場アクション、退場アクションの内容を説明する図。
【図６】アクション表の記述例を示す図。
【図７】条件判定表の記述例を示す図。
【図８】制約条件表の記述例を示す図。
【図９】イベント表の記述例を示す図。
【図１０】モデル検査プログラムの生成手順を示すフロー図。
【図１１】モデル検査支援装置に入力される各表の記載例を示す図。
【図１２】モデル検査プログラムの作成状況を示す図。
【図１３】モデル検査プログラムの作成状況を示す図。
【図１４】モデル検査プログラムの作成状況を示す図。
【図１５】モデル検査プログラムの作成状況を示す図。
【図１６】モデル検査プログラムの作成状況を示す図。
【図１７】モデル検査プログラムの作成状況を示す図。
【図１８】モデル検査プログラムの作成状況を示す図。
【図１９】モデル検査プログラムの作成状況を示す図。
【図２０】モデル検査プログラムの作成状況を示す図。
【図２１】モデル検査プログラムの作成状況を示す図。
【図２２】モデル検査プログラムの作成状況を示す図。
【図２３】モデル検査プログラムの基本構成を示す図。
【図２４】モデル検査支援装置に入力される各表の記載例を示す図。
【図２５】モデル検査プログラムの作成状況を示す図。
【図２６】モデル検査プログラムの作成状況を示す図。
【図２７】モデル検査プログラムの作成状況を示す図。
【図２８】モデル検査プログラムの基本構成を示す図。
【図２９】モデル検査プログラムの基本構成を示す図。
【図３０】キッチンタイマの構成を示すブロック図。
【図３１】キッチンタイマを設計した例を示す図。
【図３２】イベント表を利用した不可セルへの非到達性検査例を示す図。
【図３３】アクション表をモデル記述言語で作成した例を示す図。
【符号の説明】
【０１０６】
１…モデル検査支援装置、１ａ…仕様入力部、１ｂ…検査項目生成部、１ｃ…モデル記述生成部、１ｄ…状態遷移記憶部、１ｅ…アクション記憶部、１ｆ…制約条件記憶部、１ｇ…条件判定記憶部、１ｈ…モデル記述言語辞書、１ｋ…イベント記憶部、２…状態遷移表、２ａ…状態遷移表名欄、２ｂ…状態名欄、２ｃ…入退場アクション欄、２ｄ…イベント名欄、２ｅ…アクション欄、３…アクション表、３ａ…アクション名欄、３ｂ…事前条件欄、３ｃ…処理内容欄、３ｄ…事後条件欄、４…制約条件表、４ａ…構成要素名欄、４ｂ…状態名欄、４ｃ…制約条件内容欄、５…条件判定表、５ａ…条件判定名欄、５ｂ…条件内容欄、６…モデル検査プログラム、６ａ…アクション部、６ｂ…制約条件検査部、６ｃ…状態遷移部、６ｄ…イベント発生部、６ｅ…条件判定部、７…モデル検査器、８…検査結果、１１…イベント表、１１ａ…イベント名欄、１１ｂ…発生条件欄、１１ｃ…作用内容欄。
【図１】
2010020555.tif 000003
【図２】
2010020555.tif 000004
【図３】
2010020555.tif 000005
【図４】
2010020555.tif 000006
【図５】
2010020555.tif 000007
【図６】
2010020555.tif 000008
【図７】
2010020555.tif 000009
【図８】
2010020555.tif 000010
【図９】
2010020555.tif 000011
【図１０】
2010020555.tif 000012
【図１１】
2010020555.tif 000013
【図１２】
2010020555.tif 000014
【図１３】
2010020555.tif 000015
【図１４】
2010020555.tif 000016
【図１５】
2010020555.tif 000017
【図１６】
2010020555.tif 000018
【図１７】
2010020555.tif 000019
【図１８】
2010020555.tif 000020
【図１９】
2010020555.tif 000021
【図２０】
2010020555.tif 000022
【図２１】
2010020555.tif 000023
【図２２】
2010020555.tif 000024
【図２３】
2010020555.tif 000025
【図２４】
2010020555.tif 000026
【図２５】
2010020555.tif 000027
【図２６】
2010020555.tif 000028
【図２７】
2010020555.tif 000029
【図２８】
2010020555.tif 000030
【図２９】
2010020555.tif 000031
【図３０】
2010020555.tif 000032
【図３１】
2010020555.tif 000033
【図３２】
2010020555.tif 000034
【図３３】
2010020555.tif 000035