(57)【要約】  仕様構成装置は、システムの動的な振る舞いを、システムの状態とイベントによる状態の遷移の組み合わせにより記述した遷移モデルを入力する遷移モデル入力部、イベントによる遷移に伴うデータ値の更新を記述した処理モデルを入力する処理モデル入力部、システムが満たすべきデータ値の条件を状態に対応付けて記述した検証条件を入力する検証条件入力部、遷移モデルと処理モデルを共通のイベントで関連付けることにより、遷移モデルと処理モデルを結合した結合モデルを生成するモデル結合部、および、結合モデルをデータフロー解析し、状態について検証条件が満たされることを検証するデータフロー解析部を有する。
2016151710.tif 000002
【特許請求の範囲】
【請求項１】
システムの動的な振る舞いを、前記システムの状態とイベントによる前記状態の遷移の組み合わせにより記述した遷移モデルを入力する遷移モデル入力部、
前記イベントによる前記遷移に伴うデータ値の更新を記述した処理モデルを入力する処理モデル入力部、
前記システムが満たすべき前記データ値の条件を前記状態に対応付けて記述した検証条件を入力する検証条件入力部、
前記遷移モデルと前記処理モデルを共通の前記イベントで関連付けることにより、前記遷移モデルと前記処理モデルを結合した結合モデルを生成するモデル結合部、および、
前記結合モデルをデータフロー解析し、前記状態について前記検証条件が満たされることを検証するデータフロー解析部を有することを特徴とする仕様構成装置。
【請求項２】
前記モデル結合部は、前記遷移モデルの前記イベントと前記処理モデルの前記イベントが一致するとき、前記遷移モデルから抽出した前記状態をノードとし、前記イベントをエッジとする有向グラフを構成し、開始状態と終了状態に対応する新たなノードを付加し、前記有向グラフと新たな前記ノードを新たなエッジで結ぶことにより、前記結合モデルを生成することを特徴とする請求項１に記載の仕様構成装置。
【請求項３】
前記データフロー解析部は、前記有向グラフの上に、前記処理モデルに記述された前記データ値の更新に基づいて、前記データの値の変化を付加し、前記データの値の変化が前記データ値の条件を満たすことを検証することを特徴とする請求項２に記載の仕様構成装置。
【請求項４】
前記遷移モデルが並行動作を含む場合に、モデル検査法を利用したデッドロック検査をするためのデッドロック検査モデルを生成するデッドロック検査モデル生成部をさらに有することを特徴とする請求項１に記載の仕様構成装置。
【請求項５】
前記デッドロック検査モデルは、前記結合モデルに対応するプロセスの記述、前記プロセスの間の同期をとる連携プロセスの記述、および前記プロセスの間の共有情報の記述を含むことを特徴とする請求項４に記載の仕様構成装置。
【請求項６】
前記データフロー解析部による、前記処理モデルに記述された前記データ値の更新に基づいた前記データ値の変化に関する情報を、前記デッドロック検査で用いることを特徴とする請求項４に記載の仕様構成装置。
【請求項７】
仕様構成装置による仕様構成方法であって、前記仕様構成装置は、
システムの動的な振る舞いを、前記システムの状態とイベントによる前記状態の遷移の組み合わせにより記述した遷移モデルを入力し、
前記イベントによる前記遷移に伴うデータ値の更新を記述した処理モデルを入力し、
前記システムが満たすべき前記データ値の条件を前記状態に対応付けて記述した検証条件を入力し、
前記遷移モデルと前記処理モデルを共通の前記イベントで関連付けることにより、前記遷移モデルと前記処理モデルを結合した結合モデルを生成し、
前記結合モデルをデータフロー解析し、前記状態について前記検証条件が満たされることを検証することを特徴とする仕様構成方法。
【請求項８】
前記仕様構成装置は、前記遷移モデルの前記イベントと前記処理モデルの前記イベントが一致するとき、前記遷移モデルから抽出した前記状態をノードとし、前記イベントをエッジとする有向グラフを構成し、開始状態と終了状態に対応する新たなノードを付加し、前記有向グラフと新たな前記ノードを新たなエッジで結ぶことにより、前記結合モデルを生成することを特徴とする請求項７に記載の仕様構成方法。
【請求項９】
前記仕様構成装置は、前記有向グラフの上に、前記処理モデルに記述された前記データ値の更新に基づいて、データと前記データの値の変化を付加し、前記データと前記データの値の変化が前記データ値の条件を満たすことを検証することを特徴とする請求項８に記載の仕様構成方法。
【請求項１０】
前記仕様構成装置は、前記遷移モデルが並行動作を含む場合に、モデル検査法を利用したデッドロック検査をするためのデッドロック検査モデルを生成することを特徴とする請求項７に記載の仕様構成方法。
【請求項１１】
前記デッドロック検査モデルは、前記結合モデルに対応するプロセスの記述、前記プロセスの間の同期をとる連携プロセスの記述、および前記プロセスの間の共有情報の記述を含むことを特徴とする請求項１０に記載の仕様構成方法。
【請求項１２】
前記仕様構成装置は、前記処理モデルに記述された前記データ値の更新に基づいた前記データ値の変化に関する情報を、前記デッドロック検査で用いることを特徴とする請求項１０に記載の仕様構成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システム設計の初期工程においてシステムの仕様を検証し、その構成を支援する装置および方法に関わる。
【背景技術】
【０００２】
従来、組込みシステムやビジネスシステムの開発では、システムを熟知した設計者がソフトウェアを開発するのが通例であった。このため、もしシステム設計の初期工程（以下、上流工程と呼ぶ）で曖昧さや誤りが存在したとしても、後のソフトウェア開発工程で発見し修正することができ、開発後のシステムの運用段階まで持ち越され欠陥として発見されることは少なかった。しかし、システムが複雑になるにつれて設計者がシステム全体を把握することが困難になり、ソフトウェア開発工程での修正に依存した方法では欠陥が除去しきれなくなりつつある。【０００３】
このような背景から現在では、上流工程で誤りを除去し、ソフトウェア開発工程での手戻りを減らすことが、ソフトウェアの信頼性と生産性を向上させるうえで有効であると考えられている。上流工程の誤り除去を実現するため、上流工程の仕様記述と仕様の整合性確認が重要であり、上流工程に適した仕様記述法の利用が進んでいる。仕様は一般に、システムが扱うデータに関する記述、システムが実行する処理に関する記述、及びシステムの動的な振舞いに関する記述から構成される。上流工程では、処理に関する記述にはユースケース、振舞いに関する記述には処理フロー図が使われる一方、データに関する記述は抽象化されてユースケースに埋め込まれることが多い。【０００４】
上流工程の仕様における、処理に関する記述、動的な振舞いに関する記述の間には関連があり、システムの仕様はこれらの総体として表現される。しかし、各記述をまたがった仕様の整合性のチェックは困難であり、記述間の不整合による欠陥が除ききれなかった。これに対し特許文献１では、状態遷移表、アクション表、条件判定表、および制約条件表の４つの表に仕様を記述した後、それらを結合して１つの形式的なモデルを構成し、整合性を検証する方法が開示されている。【０００５】
具体的には、動的な振舞いを状態遷移表に、処理をアクション表に、遷移条件を条件判定表に記述し、制約条件表に記述したデータと状態の対応をチェックする。状態遷移表は、状態、イベント、及び遷移に加えて、遷移が起こるガード条件、及び遷移にともなうアクションから構成される。アクション表は、アクションに関して、アクションを起こすための事前条件、アクション後に成立すべき事後条件、アクションによる要素の値の更新を表す処理内容から構成される。条件判定表は、アクションと遷移が実行可能か否かの判定条件を表現し、ガード条件と事前条件から構成される。制約条件表は要素の値を状態ごとに記述する。【０００６】
特許文献１の装置は、記述された仕様から１つの形式的なモデルを生成する。このモデルをモデル検査器に入力し、モデル検査器を使って整合性を検証することにより、記述された仕様の不整合を機械的に検出する。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特開２００９−１５７６６１公報
【発明の概要】
【発明が解決しようとする課題】
【０００８】
特許文献１に記載された仕様記述方法によれば、システムがある状態にあるときイベントが発生すると、システムは、状態とイベントに対して指定されたアクションを実行し、指定された状態に遷移する。アクションまたは遷移が実行可能か否かは、条件判定表の記述によって判定される。これは、プログラムモジュールの呼び出しをアクションと対応付け易い点で、設計工程で実装の仕様を記述するのに適していると考えられる。【０００９】
一方、上流工程の仕様記述の観点からは、イベントとアクションの区分が煩雑である。設計工程での仕様記述が計算機における実装方法の明確化を目的とするのに対し、上流工程での仕様記述は、人のための処理概要の明確化を目的としており、人が把握容易な仕様記述であることが求められる。例えば上記の場合、どのような時に何が起こり、その結果どのような効果が得られるか、が簡潔に表現できれば良い。特許文献１の方法では、できごとをイベントに、処理をアクションに分離しているため、人が仕様を把握するにはイベント名とアクション名の照合が必要であるとともに、アクションあるいは遷移が実行可能かどうかを判定するために条件判定表を参照する必要がある。このことは、人が仕様を直感的に把握することを難しくしている。人が把握しにくい仕様から形式的なモデルを生成し、整合性を検証すると、仕様の不整合が多く検出される。【００１０】
また、モデル検査器に入力するためのモデル作成支援装置の提供を目的としており、モデル検査器を使って検証することが前提である。モデル検査は、すべての状態遷移の組み合わせについて網羅的に検査するので、並行動作を含むシステムの仕様検証には有効な検証方法であるが、並行動作を含まないシステムの仕様不整合の検出には効率が悪い。【００１１】
そこで、システム設計の初期工程おいて、人（設計者）が記述した仕様の整合性を効率的に検証できることが求められる。
【課題を解決するための手段】
【００１２】
開示する仕様構成装置は、システムの動的な振る舞いを、システムの状態とイベントによる状態の遷移の組み合わせにより記述した遷移モデルを入力する遷移モデル入力部、イベントによる遷移に伴うデータ値の更新を記述した処理モデルを入力する処理モデル入力部、システムが満たすべきデータ値の条件を状態に対応付けて記述した検証条件を入力する検証条件入力部、遷移モデルと処理モデルを共通のイベントで関連付けることにより、遷移モデルと処理モデルを結合した結合モデルを生成するモデル結合部、および、結合モデルをデータフロー解析し、状態について検証条件が満たされることを検証するデータフロー解析部を有する。
【発明の効果】
【００１３】
開示する仕様構成装置によれば、システム設計の初期工程おいて、人が記述した仕様を効率的に検証できる。
【図面の簡単な説明】
【００１４】
【図１】仕様構成装置における仕様構成方法を示すフロー図である。
【図２】仕様構成装置の構成を示す図である。
【図３】遷移モデルの記述例を示す図である。
【図４】処理モデルの記述例を示す図である。
【図５】検証条件の記述例を示す図である。
【図６】モデルの結合部のフロー図である。
【図７】結合モデルの例を示す図である。
【図８】データフロー解析部のフロー図である。
【図９】データフロー解析部の手続き１の手順を示すフロー図である。
【図１０】データフロー解析部の手続き２の手順を示すフロー図である。
【図１１】データフロー解析部の手続き３の手順を示すフロー図である。
【図１２】データフロー解析部の手続き４の手順を示すフロー図である。
【図１３】データフロー解析部が生成するデータ値の例を示す図である。
【図１４】データフロー解析部が生成するデータ遷移グラフの例を示す図である。
【図１５】デッドロック検査モデル生成部のフロー図である。
【図１６】デッドロック検査モデル生成部の手続きＡの手順を示すフロー図である。
【図１７】デッドロック検査モデル生成部の手続きＢの手順を示すフロー図である。
【図１８】デッドロック検査モデル生成部の手続きＣの手順を示すフロー図である。
【図１９】デッドロック検査モデル生成部の手続きＤの手順を示すフロー図である。
【図２０】デッドロック検査モデル生成部が生成するデッドロック検査モデルの例を示す図である。
【発明を実施するための形態】
【００１５】
利用者は、遷移モデルと処理モデルと検証条件を入力し、遷移モデルと処理モデルの間に不整合が無いこと、および別途入力した検証条件が満たされることを、仕様構成装置を用いて検証する。また、遷移モデルが複数の状態遷移系列に関わる並行動作を含むとき、状態遷移が進行しないデッドロックが各状態遷移系列の実行順序によって起こらないことを、仕様構成装置が生成するデッドロック検査モデルについて検査する。
【００１６】
図１は、仕様構成装置における仕様構成方法を示すフロー図である。利用者は仕様構成装置に、遷移モデルを入力し（ステップ１）、処理モデルを入力し（ステップ２）、検証条件を入力する（ステップ３）。これらの入力は、どのような順序で行われても良い。また、検証条件の入力は、次のステップ４の後でも良い。
【００１７】
仕様構成装置は、入力された遷移モデルと処理モデルを照合し、両者を結合したモデルを生成する（ステップ４）。仕様構成装置は、結合されたモデルのデータフローを解析し、処理モデルの処理を遷移モデルの順序で実行することが可能であり、さらに検証条件が満たされることを検証する（ステップ５）。
【００１８】
仕様構成装置は、検証条件が満たされることを判定し（ステップ６）、検証条件が満たされない場合には、不整合箇所出力（ステップ７）へ進む。検証条件が満たされている場合には、仕様構成装置は、並行動作の有無を判定する（ステップ８）。並行動作が無い場合には、入力されたモデルは整合しているので、仕様構成装置は処理を終了する。
【００１９】
モデルに並行動作が含まれている場合には、仕様構成装置は、デッドロックの有無を検査するためのデッドロック検査モデルを生成する（ステップ９）。仕様構成装置は、たとえば、ＳＰＩＮモデル（Mordechai Ben-Ari著 中島震監訳 谷津弘一、野中哲、足立太郎共訳：SPINモデル検査入門、オーム社  2010年）のような一般のモデル検査器を用いて、デッドロックの有無を検査する（ステップ１０）。仕様構成装置は、デッドロックの有無を判定し（ステップ１１）、デッドロックがある場合には不整合箇所出力を実行する（ステップ７）。デッドロックが無い場合には、仕様構成装置は、入力されたモデルは整合しているとして、処理を終了する。
【００２０】
図２は、仕様構成装置の構成を示す図であり、図１の各ステップに対応した構成要素を持つ。仕様構成装置２１は、検証結果２７とデッドロック検査モデル２１０を出力する。
【００２１】
遷移モデル入力部２２は、利用者からの遷移モデルを入力する。図２では、仕様構成装置２１を利用者が操作して遷移モデルを入力する形態について図示しているが、この形態に限らず、利用者が予め記述した遷移モデルを、ファイル等を通じて入力する形態でも良い。また、遷移モデルの入力の際に、処理モデルや検証条件を参照して利用者の入力を支援する形態であっても良い。これは、処理モデル入力部２３、検証条件入力部２４についても同様である。
【００２２】
処理モデル入力部２３は、利用者からの処理モデルを入力する。検証条件入力部２４は、利用者からの検証条件を入力する。
【００２３】
モデル結合部２５は、入力された遷移モデルと処理モデルを結合したモデルを生成する。データフロー解析部２６は、モデル結合部２５で生成されたモデルについてデータフローを解析し、処理モデルの処理を遷移モデルの順序で実行することが可能であり、さらに検証条件が満たされることを検証する。仕様構成装置２１は、データフロー解析部２６による検証結果２７を出力する。
【００２４】
デッドロック検査モデル生成部２８であり、一般のモデル検査器を利用してデッドロック検査を行うための、モデル検査器が処理できる形式にモデルを変換する。なお、デッドロック検査の入力は必ずしも検証済モデルである必要はなく、遷移モデルと処理モデルから改めて生成しても良い。
【００２５】
仕様構成装置２１は、デッドロック検査モデル生成部２８が生成したデッドロック検査モデル２９を出力する。利用者は、デッドロック検査モデル２９をモデル検査器２１０に入力し、デッドロック検査結果２１１を得る。
【００２６】
図３は、利用者が入力する遷移モデルの記述例を示す図である。遷移モデルは、上流工程で使われる処理フローに準ずる形式で、処理の流れを記述したものである。ＳＩは開始状態３１、ＳＥは終了状態３２を表し、処理の流れは開始状態３１から始まり、一連の処理を経由して、終了状態３２に至れば終了する。
【００２７】
四角形３２〜３６は処理を示し、ここではイベントと呼ぶ。矢印は次に実行すべき処理を表し、ここでは遷移と呼ぶ。矢印と矢印を繋ぐ丸は、ここでは状態と呼ぶ。
【００２８】
図３の遷移モデルが表す処理フローは、次の通りである。開始状態３１から処理が始まり、受付区分判定新規３２および受付区分判定更改３３のいずれかの処理が実行された後、契約書作成３４が実行される。その後、契約者情報登録３６が実行されて終了状態３７に至るか、申込区分変更３５により再び受付区分判定新規３２および受付区分判定更改３３のいずれかの処理に戻る。
【００２９】
遷移モデルには、このような処理フローを複数記述することができる。すなわち、互いに交わることのない、開始状態から終了状態への一連の処理が、複数存在し得る。その場合、それらの処理フローは並行動作するものとみなす。ここで、異なる一連の処理フローの間に共通のイベントが出現する場合、処理フローは共通のイベントを通じて同期すると考える。
【００３０】
このような複数記述は、大きな１つの処理フローを複数の処理フローに分割して記述できるので利便性が高いが、処理の実行順序に依存してデッドロックが起きる可能性がある。仕様構成装置２１は、遷移モデルに並行動作を含む場合にデッドロックが起こらないことを、図１のステップ１０で検査する。
【００３１】
遷移モデルの記述形式は、図３のような図形式に限定されるものではなく、状態とイベントによる遷移が記述できるものであれば、テキスト形式や表形式でも良い。
【００３２】
図４は、利用者が入力する処理モデルの記述例を示す図である。処理モデルは、上流工程で使われるユースケース図の事前事後記述に準ずる形式で、処理を実行するためのデータ値の条件と、処理後のデータ値を記述する。遷移モデルと同様に、処理モデルに記述する処理を、ここではイベントと呼ぶ。遷移モデルのイベントと処理モデルのイベントは一致しなければならず、仕様構成装置２１は、図１のステップ４でモデルを結合する際にチェックする。
【００３３】
受付区分判定新規４１の処理は、データ申込区分の値が新規であるとき、データ受付区分の値が新規になることを表す、ここでは、処理の前提となるデータ値の記述を条件部、処理によって設定されるデータ値の記述を帰結部と呼ぶ。
【００３４】
受付区分判定更改４２の処理は、帰結部で２つのデータに値を設定している。これは、データ受付区分の値が更改になるとともに、データ契約書の値が確定になることを表す。
【００３５】
契約書作成４３a、４３bの処理は、１つの処理を複数の項目に分割して記述した例である。契約書作成４３aはデータ受付区分の値が新規のとき契約書の値を確定にすることを、契約書作成４３bはデータ受付区分の値が更改のとき何もしないことを表す。
【００３６】
図４の処理モデルは、さらに受付区分変更４４a、４４bの処理、および契約者情報登録４５の処理を記述している。
【００３７】
処理の条件部の記載項目は複数個であっても良く、また０個であっても良い。条件部の記載が０個の場合、条件が常に成り立つとみなす。また、条件部の記載が複数の場合、それらの条件が全て成り立つことが処理の前提となる。条件部にはデータ値に関する論理式が記載されていても良い。
【００３８】
帰結部も同様に、記載項目は複数個であっても良く、また０個であっても良い。複数個の場合には、それらの値が同時に設定されることを、契約書作成４３bの例のように、０個の場合には何もしないことを表す。
【００３９】
処理モデルの記述形式は、図４のような表形式に限定されるものではなく、イベントが起こるためのデータ値の条件とイベント後のデータ値の条件が記述できるものであれば、テキスト形式や図形式でも良い。
【００４０】
図５は、利用者が入力する検証条件の記述例を示す図である。検証条件は、図３の遷移モデルの状態に対応付けて、処理がその状態まで進行した場合に期待されるデータ値を列挙する。
【００４１】
図５では、図３の遷移モデルが表す処理が終了状態まで進んだとき、すなわち一連の処理が終わったとき、データ契約者情報の値が確定である（５１）ことを要求している。同様に、図３の遷移モデルが表す処理が終了状態まで進んだとき、申込区分の値が新規かつ受付区分の値が新規、または、申込区分の値が更改かつ受付区分の値が更改である（５２）ことを要求している。後者のように、検証条件には論理式が記載されていても良い。
【００４２】
検証条件の記述形式は、図５のような図形式に限定されるものではなく、期待されるデータ値を状態に関連付けて記述できるものであれば、テキスト形式や表形式でも良い。
【００４３】
図６は、モデルの結合部２５のフロー図（図１のステップ４の遷移モデルと処理モデルの結合手順を示すフロー図）である。この手順により、入力された遷移モデルと処理モデルを照合して、１つのモデルにまとめ上げる。
【００４４】
モデルの結合部２５は、遷移モデルからイベントを抽出し（ステップ６１）、処理モデルからイベントを抽出する（ステップ６２）。モデルの結合部２５は、これらのイベントが一致するかを判定し（ステップ６３）、不一致であれば、不一致であることを出力して（ステップ６７）、終了する。
【００４５】
遷移モデルのイベントと処理モデルのイベントが一致するならば、モデルの結合部２５は、遷移モデルから状態を抽出し（ステップ６４）、状態をノード、イベントをエッジとする有向グラフを構成する（ステップ６５）。モデルの結合部２５は、構成した有向グラフに、開始状態と終了状態に対応するノードを付加し、エッジで結ぶ（ステップ６６）。
【００４６】
このようにして遷移モデルと処理モデルを結合して構成したモデルを、ここでは結合モデルと呼ぶ。遷移モデルには一般に複数の処理フローが含まれ得るので、１つの結合モデルには複数の有向グラフが存在し得る。
【００４７】
図７は、結合モデルの例を示した図である。この例は、図３の遷移モデルと図４の処理モデルに対応しており、結合モデルは１つの有向グラフからなる。図７で、円は有向グラフのノードを、矢印はエッジを表す。エッジのラベル（名称）は、イベント名である。
【００４８】
図８は、データフロー解析部２６のフロー図（図１のステップ５のデータフロー解析の手順を示すフロー図）である。データフロー解析部２６は、遷移モデルと処理モデルを結合した有向グラフの上に、データとその値の変化を付加する。このとき、有向グラフのノードである状態には一般に複数のデータ値の組が対応付くので、データフロー解析部２６はそれらを処理する方法を与える。また、図７のように、有向グラフは一般に分岐や合流、繰り返しを含むので、処理済のデータ値の組を繰り返し処理することを防ぐ方法も与える。
【００４９】
データフロー解析部２６は、有向グラフの全てのノードに、複数のデータ値の組を格納する格納領域Ｄを割り当てる（ステップ８１）。割り当てたＤの初期値は、空とする。データフロー解析部２６は、開始状態に対応するノードの格納領域Ｄに、初期データ値の組を格納する（ステップ８２）。
【００５０】
一般に初期データ値の組は複数あり、それらの各々について、データフロー解析部２６は、処理モデルの処理を遷移モデルの順で実行した際のデータ値の変化を解析する。データフロー解析部２６は、この解析を、手続き１を呼び出すことで実行する（ステップ８３）。
【００５１】
ステップ８３が終了すると、各ノードにデータ値の組が付加されているので、データフロー解析部２６は、これらが検証条件を満たすことを検証する。この検証のために、データフロー解析部２６は、検証条件に指定された格納領域Ｄにある全てのデータ値の組を得（ステップ８４）、それが検証条件を満たすかを判定する（ステップ８５）。
【００５２】
検証条件が満たされない場合、データフロー解析部２６は、不具合であることを出力し（ステップ８６）、終了する。検証条件が満たされた場合には、遷移モデルと処理モデルは整合するとして、データフロー解析部２６は、終了する。
【００５３】
図９は、データフロー解析部２６の手続き１の手順を示すフロー図である。手続き１は、データフロー解析を実行する手続き２を、全ての初期データの組について呼び出す（ステップ９１）。
【００５４】
手続き１は、手続き２が処理するノードnと処理するデータ値の組dを、初期データの組に設定する。具体的には、nを開始ノードに設定し（ステップ９２）、dを初期データの組として設定し（ステップ９３）、手続き２を呼び出す（ステップ９４）。
【００５５】
図１０は、データフロー解析２６の手続き２の手順を示すフロー図である。手続き２では、与えられたノードnとデータ値の組dに対して、イベントによって遷移する先のノードにおけるデータ値の組を、nにおいて起こり得る全てのイベントについて計算する。
【００５６】
このため、手続き２は、ノードnから外向きのエッジを得る（ステップ１０１）。外向きのエッジが存在するならば（ステップ１０２）、nから外向きの全てのエッジについて順に（ステップ１０３）、処理するエッジをeとして（ステップ１０４）手続き３を呼び出す（ステップ１０５）。
【００５７】
ステップ１０２において、nからの外向きのエッジが存在しない場合はnからの遷移先がないことを意味するので、手続き２は、nが終了状態であるかを判定（ステップ１０６）し、終了状態であれば、終了し、終了状態でなければ、遷移モデルが不整合であることを出力する（ステップ１０７）。
【００５８】
図１１は、データフロー解析２６の手続き３の手順を示すフロー図である。手続き３は、与えられたエッジeとデータ値の組dに対して処理モデルを参照し、dの下で起こり得るeを選択して、遷移後のデータ値を計算する。
【００５９】
一般に、同一のイベントに対して処理モデルの項目は複数存在するので、与えられたエッジeとデータ値の組dに対して遷移先が複数存在し得る。手続き３は、それら全ての遷移先についてデータ値の組を計算する。
【００６０】
このため、手続き３は、eに対応するイベントから処理モデルの項目の条件部がdにマッチする項目を選ぶ（ステップ１１１）。そのような項目が存在するならば（ステップ１１２）、手続き３は、それらの項目全てについて（ステップ１１３）、手続き４を呼び出す（ステップ１１４）。
【００６１】
一方、条件部がdにマッチする処理モデルの項目が一つもない場合には、遷移モデルの処理フローの通りに処理を進めることができないことを意味するので、手続き３は、処理モデルが不整合であることを出力（ステップ１１５）する。
【００６２】
図１２は、データフロー解析部２６の手続き４の手順を示すフロー図である。手続き４は、与えられたデータ値の組dとノードn、エッジeから遷移先のデータ値の組を計算して遷移先のノードの格納領域Ｄに加えるとともに、ノードを遷移先のノードに進めて、データフロー解析部２６の手続き２を再帰的に呼び出す。
【００６３】
具体的には、手続き４は、手続き３で選び出した処理モデルの項目の帰結部とdから、遷移先のデータ値の組dn+1を計算する（ステップ１２１）。手続き４は、エッジeをたどって遷移先ノードn+1を得る（ステップ１２２）とともに、ノードn+1に対応付けられたデータ値の格納領域Dn+1を得る（ステップ１２３）。
【００６４】
手続き４は、Dn+1にデータ値の組dn+1が存在するかを判定し（ステップ１２４）、存在しないならば、dn+1をDn+1に加え、dnからdn+1へエッジを張る（ステップ１２５）。これでノードnからエッジeによるデータ値の組dnの変化に関する処理の一つが終わったのでノードを一つ進め、n+1をn、d+1をdとして手続き２を呼び出す（ステップ１２６）。
【００６５】
一方、ステップ１２４でDn+1にdn+1が存在する場合には、ノードn+1でデータ値の組dn+1に関する解析が既に終了していることを意味するので、手続き４は、dnからdn+1へのエッジを張り（ステップ１２７）、終了する。
【００６６】
図１２では、データ値の組がどのように変化したかを記録するため、ステップ１２５とステップ１２７で、手続き４はdnからdn+1へのエッジを張っている。これにより、状態をノード、イベントをエッジとする有向グラフとは別に、データ値の組をノード、イベントをエッジとする有向グラフが構成される。以下では、これをデータ遷移グラフと呼ぶ。データ遷移グラフは、データ値の組の変化の追跡を容易にするとともに、デッドロック検証の際の検証効率を向上する。
【００６７】
図１３は、データフロー解析部２６が生成するデータ値の組の例を示す図である。この図は、図３の遷移モデルおよび図４の処理モデルの例に対応する。
【００６８】
図１３の吹き出しは、各ノードに対応付けられた格納領域Dを表す。Dの中の＜と＞で囲まれた符号の組は、その状態における各データ値の組を表し、図中では＜申込区分、受付区分、契約書、契約者情報＞の順である。-は値が決まっていないことを表す。
【００６９】
吹き出し１３１は、開始状態に２つの初期データの組＜新規、-、-、-＞と＜更改、-、-、-＞が存在することを示す。これは、開始状態では申込区分が新規であること以外はデータの値が決まっていないデータ値の組と、申込区分が更新であること以外はデータの値が決まっていないデータ値の組が存在することを表す。
【００７０】
吹き出し１３２は、開始状態の次の状態におけるデータ値の組を示す。開始状態からのデータ値の組に加えて、イベント申込区分変更により戻ったデータ値の組があるため、４つのデータ値の組が存在する。吹き出し１３５はイベント契約者情報登録の後のデータ値の組であり、吹き出し１３６は終了状態におけるデータ値の組である。
【００７１】
図５の検証条件の例では、終了状態において契約者情報は確定であること（５１）、申込区分は新規であり受付区分も新規であることまたは申込区分は更改であり受付区分も更改であること（５２）を要求しており、吹き出し１３６がこの条件を満たしていることは容易に検証できる。この検証は、図８のステップ８４およびステップ８５で実行される。
【００７２】
図１４は、データフロー解析部２６が生成するデータ遷移グラフの例を示す図である。図１３の吹き出し１３１の２つの初期データ値の組は、図１４ではノード１４１とノード１４２に対応する。同様に、吹き出し１３２はノード１４３からノード１４６、吹き出し１３３はノード１４７からノード１４９、吹き出し１３４はノード１４１０からノード１４１１、吹き出し１３５はノード１４１２からノード１４１３、吹き出し１３６はノード１４１４からノード１４１５に対応する。
【００７３】
図１４では、図１２のステップ１２５とステップ１２７でdnからdn+1へのエッジを張った結果を示している。これにより、データ値の組をノード、イベントをエッジとするデータ遷移グラフが構成される。データ遷移グラフは、データ値の組がどのように変化したかを記録しており、デッドロック検査モデル生成部２８が使用するために、仕様構成装置２１のメモリに格納される。
【００７４】
図１５は、デッドロック検査モデル生成部２８のフロー図（図１のステップ９のデッドロック検査モデルを生成する手順を示すフロー図）である。仕様構成装置２１は、遷移モデルが並行動作を含むとき、すなわち遷移モデルの中に独立した処理フローが複数存在するときに、それらの間のデッドロックの有無を、モデル検査器２１０を使って検査する。図１５は、モデル検査器２１０の入力となるデッドロック検査モデル２９を生成する手順を示す。
【００７５】
デッドロック検査モデル２９は、各処理フローから生成した結合モデルに対応するプロセスの記述と、それらの間の同期をとる連携プロセスの記述、およびプロセス間の共有情報の記述を含む。このため、デッドロック検査モデル生成部２８は、手続きＡを呼び出してプロセス間共有情報を生成し（ステップ１５１）、次に手続きＢを呼び出して連携プロセス記述を生成する（ステップ１５２）。その後、全ての結合モデルについて（ステップ１５３）、手続きＣを呼び出してプロセスの記述を生成する（ステップ１５４）。
【００７６】
図１６は、デッドロック検査モデル生成部２８の手続きＡの手順を示すフロー図である。手続きＡは、プロセス間で共有される、イベント受け渡しチャネルと状態変数の記述を生成する。このため、手続きＡは全ての結合モデルについて（ステップ１６１）、イベントを受け渡すチャネルを生成し（ステップ１６２）、状態変数を生成する（ステップ１６３）。また、データ遷移グラフのデータノードに付番し、状態変数の値とする（ステップ１６４）。
【００７７】
図１７は、デッドロック検査モデル生成部２８の手続きＢの手順を示すフロー図である。手続きＢは、連携プロセスの記述を生成する。連携プロセスは、各結合モデルのデータ遷移グラフの情報を下に、発生し得るイベントを生成し、チャネルを通じて各結合モデルから生成されたプロセスに送信する。
【００７８】
手続きＢは、プロセスの枠組みを生成し（ステップ１７１）、全てのイベントeについて（ステップ１７２）、ステップ１７３からステップ１７４を実行する。すなわち、全てのデータ遷移グラフについて、eを外向きエッジとするデータノードを抽出し（ステップ１７３）、eに関わる全ての結合モデルで状態変数の値が、抽出したデータノードであるときイベントeを発生させる文を生成する（ステップ１７４）。発生させたイベントを、チャネルを通じて各プロセスに送信する文を生成する（ステップ１７５）。
【００７９】
図１８は、デッドロック検査モデル生成部２８の手続きＣの手順を示すフロー図である。手続きＣは、並行動作する各結合モデルについて、プロセスの記述を生成する。
【００８０】
手続きＣは、チャネルを通じてイベントを受信する文を生成する（ステップ１８１）。手続きＣは、初期状態に対応して、状態変数にデータ遷移モデルの開始データノードを代入する文を生成する（ステップ１８２）とともに、終了状態に対応して状態変数の値がデータ遷移モデルの終了データノードである文を生成する（ステップ１８３）。なお、初期値が複数ある場合にはデータ遷移モデルの開始データノードが複数存在するが、プロセスの記述は結合モデルに対して生成するので、それらの開始データノードに遷移するダミーの開始ノードを１つ設定する。
【００８１】
手続きＣは、初期状態と終了状態の中間にあるデータノードに関する記述を生成するため、開始データノードと終了データノードを除く全てのデータノードについて手続きＤを呼び出す（ステップ１８４）。
【００８２】
図１９は、デッドロック検査モデル生成部２８の手続きＤの手順を示すフロー図である。手続きＤは、データ遷移グラフをもとに、イベントによる遷移を記述する。
【００８３】
手続きＤは、データ遷移グラフのデータノードから外向きエッジと遷移先ノードを抽出する（ステップ１９１）。手続きＤは、状態変数の値が外向きエッジを持つデータノードでありイベントが外向きエッジであるとき、状態変数を遷移先ノードで置き換える文を生成する（ステップ１９２）。手続きＤは、データ遷移グラフのデータノードに名前をつけ、状態変数の値とする（ステップ１９３）。
【００８４】
図２０は、デッドロック検査モデル生成部２８が生成したデッドロック検査モデル２９の例を示す図である。デッドロック検査モデル２０１は、例えばこのようなテキスト形式で出力される。このデッドロック検査モデル２０１は、プロセス間で共有される情報の記述（２０２）、連携プロセスの記述（２０３）、及び各結合モデルに対応するプロセスの記述（２０４a、２０４b）を含む。
【００８５】
プロセス間で共有される情報の記述（２０２）は、デッドロック検査モデル生成部２８の手続きＡ（図１６）で生成される。この例では、結合モデルＡとＢに対して、チャネルcAとcB、及び状態変数stateAとstateBが作成される。
【００８６】
連携プロセスの記述（２０３）は、デッドロック検査モデル生成部２８の手続きＢ（図１７）で生成される。この例では、Ａがa1、Ｂがb1にあるとき、共有イベントe1を、チャネルを通じて送信する。一方、Ａがa2にあるとき、Ｂに関わらずイベントe2を、チャネルを通じて送信する。e2は、Ａの遷移に関わるイベントであり、共有イベントではない。
【００８７】
プロセスの記述（２０４a、２０４b）は、デッドロック検査モデル生成部２８の手続きＣ（図１８）と手続きＤ（図１９）で生成される。各プロセスは、まず状態変数を初期状態に設定する。その後、チャネルを通じてイベントを受信し、現在の状態変数の値と受信したイベントから遷移先状態を決定し、状態変数に代入する。
【００８８】
デッドロック検査モデル２９では、プロセスが共有イベントの発生を待つ、一方で対応するプロセスが他の共有イベントの発生を待つ、またはイベント発生を終了した際に、デッドロックが起こる。このように構成したデッドロック検査モデル２９をモデル検査器２１０に入力し、デッドロックの有無を検査する。
【００８９】
本実施形態の仕様構成装置によれば、システム設計の初期工程おいて、人が記述した仕様を効率的に検証できる。
【００９０】
また、上流工程の設計者は処理フローとユースケースに相当する方法で仕様を記述し、それらの間の整合性を検証できるので、組込みシステムやビジネスシステムなどの分野において、複雑なシステムの上流設計を信頼性高く効率的に行うことができる。
【符号の説明】
【００９１】
２１：仕様構成装置、  ２２：遷移モデル入力部、２３：処理モデル入力部、２４：検証条件入力部、２５：モデル結合部、２６：データフロー解析部、２７：検証結果、２８：デッドロック検査モデル生成部、２９：デッドロック検査モデル、２１０：モデル検査器、２１１検証結果。
【図１】
2016151710.tif 000003
【図２】
2016151710.tif 000004
【図３】
2016151710.tif 000005
【図４】
2016151710.tif 000006
【図５】
2016151710.tif 000007
【図６】
2016151710.tif 000008
【図７】
2016151710.tif 000009
【図８】
2016151710.tif 000010
【図９】
2016151710.tif 000011
【図１０】
2016151710.tif 000012
【図１１】
2016151710.tif 000013
【図１２】
2016151710.tif 000014
【図１３】
2016151710.tif 000015
【図１４】
2016151710.tif 000016
【図１５】
2016151710.tif 000017
【図１６】
2016151710.tif 000018
【図１７】
2016151710.tif 000019
【図１８】
2016151710.tif 000020
【図１９】
2016151710.tif 000021
【図２０】
2016151710.tif 000022
【手続補正書】
【提出日】平成28年12月14日(2016.12.14)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
システムの動的な振る舞いを、前記システムの状態とイベントによる前記状態の遷移の組み合わせにより記述した遷移モデルを入力する遷移モデル入力部、
前記イベントによる前記遷移に伴うデータ値の更新を記述した処理モデルを入力する処理モデル入力部、
前記システムが満たすべき前記データ値の条件を前記状態に対応付けて記述した検証条件を入力する検証条件入力部、
前記遷移モデルと前記処理モデルを共通の前記イベントで関連付けることにより、前記遷移モデルと前記処理モデルを結合した結合モデルを生成するモデル結合部、および、
前記結合モデルをデータフロー解析し、前記状態について前記検証条件が満たされることを検証するデータフロー解析部を有することを特徴とする仕様構成装置。
【請求項２】
前記モデル結合部は、前記遷移モデルの前記イベントと前記処理モデルの前記イベントが一致するとき、前記遷移モデルから抽出した前記状態をノードとし、前記イベントをエッジとする有向グラフを構成し、開始状態と終了状態に対応する新たなノードを付加し、前記有向グラフと新たな前記ノードを新たなエッジで結ぶことにより、前記結合モデルを生成することを特徴とする請求項１に記載の仕様構成装置。
【請求項３】
前記データフロー解析部は、前記有向グラフの上に、前記処理モデルに記述された前記データ値の更新に基づいて、前記データ値を付加し、付加した前記データ値が前記データ値の条件を満たすことを検証することを特徴とする請求項２に記載の仕様構成装置。
【請求項４】
前記遷移モデルが並行動作を含む場合に、モデル検査法を利用したデッドロック検査をするためのデッドロック検査モデルを生成するデッドロック検査モデル生成部をさらに有することを特徴とする請求項１に記載の仕様構成装置。 
【請求項５】
前記デッドロック検査モデルは、前記結合モデルに対応するプロセスの記述、前記プロセスの間の同期をとる連携プロセスの記述、および前記プロセスの間の共有情報の記述を含むことを特徴とする請求項４に記載の仕様構成装置。
【請求項６】
前記データフロー解析部による、前記処理モデルに記述された前記データ値の更新に基づいた前記データ値の変化に関する情報を、前記デッドロック検査で用いることを特徴とする請求項４に記載の仕様構成装置。
【請求項７】
仕様構成装置による仕様構成方法であって、前記仕様構成装置は、
システムの動的な振る舞いを、前記システムの状態とイベントによる前記状態の遷移の組み合わせにより記述した遷移モデルを入力し、
前記イベントによる前記遷移に伴うデータ値の更新を記述した処理モデルを入力し、
前記システムが満たすべき前記データ値の条件を前記状態に対応付けて記述した検証条件を入力し、
前記遷移モデルと前記処理モデルを共通の前記イベントで関連付けることにより、前記遷移モデルと前記処理モデルを結合した結合モデルを生成し、
前記結合モデルをデータフロー解析し、前記状態について前記検証条件が満たされることを検証することを特徴とする仕様構成方法。
【請求項８】
前記仕様構成装置は、前記遷移モデルの前記イベントと前記処理モデルの前記イベントが一致するとき、前記遷移モデルから抽出した前記状態をノードとし、前記イベントをエッジとする有向グラフを構成し、開始状態と終了状態に対応する新たなノードを付加し、前記有向グラフと新たな前記ノードを新たなエッジで結ぶことにより、前記結合モデルを生成することを特徴とする請求項７に記載の仕様構成方法。
【請求項９】
前記仕様構成装置は、前記有向グラフの上に、前記処理モデルに記述された前記データ値の更新に基づいて、前記データ値を付加し、付加した前記データ値が前記データ値の条件を満たすことを検証することを特徴とする請求項８に記載の仕様構成方法。
【請求項１０】
前記仕様構成装置は、前記遷移モデルが並行動作を含む場合に、モデル検査法を利用したデッドロック検査をするためのデッドロック検査モデルを生成することを特徴とする請求項７に記載の仕様構成方法。
【請求項１１】
前記デッドロック検査モデルは、前記結合モデルに対応するプロセスの記述、前記プロセスの間の同期をとる連携プロセスの記述、および前記プロセスの間の共有情報の記述を含むことを特徴とする請求項１０に記載の仕様構成方法。
【請求項１２】
前記仕様構成装置は、前記処理モデルに記述された前記データ値の更新に基づいた前記データ値の変化に関する情報を、前記デッドロック検査で用いることを特徴とする請求項１０に記載の仕様構成方法。
【国際調査報告】
2016151710.tif 000023
2016151710.tif 000024
2016151710.tif 000025
2016151710.tif 000026