(57)【要約】【課題】システム上で動作するサービス競合仕様の検討段階であっても、サービス競合の不備を検出するモデル検査方法及びモデル検査装置を提供する。【解決手段】モデル検査装置１０は、モデル生成部１２ａ、モデル検査実行部１２ｂ、競合判定部１２ｃを有する。モデル生成部１２ａは、システムで動作させる２つ以上のサービスから２つのサービスを選択したサービスの組合せ毎のサービス実行の競合条件と、サービスの組合せを任意のタイミングで実行した場合の実行結果が満たすべき制約条件とを含むシステムのモデルを、システムの仕様をもとに生成する。モデル検査実行部１２ｂは、サービス実行の競合条件をもとに、サービスの組合せを任意のタイミングで実行した場合の各実行結果を出力する。競合判定部１２ｃは、モデル検査実行部１２ｂにより出力された各実行結果が制約条件を満たすか否かを判定する。【選択図】図１
2017146728.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータが実行するモデル検査方法であって、
システムで動作させる２つ以上のサービスから２つのサービスを選択したサービスの組合せ毎のサービス実行の競合条件と、前記サービスの組合せを任意のタイミングで実行した場合の実行結果が満たすべき制約条件とを含む前記システムのモデルを、前記システムの仕様をもとに生成する生成ステップと、
前記サービス実行の競合条件をもとに、前記サービスの組合せを任意のタイミングで実行した場合の各実行結果を出力する出力ステップと、
前記出力ステップにより出力された各実行結果が前記制約条件を満たすか否かを判定する判定ステップと
を含んだことを特徴とするモデル検査方法。
【請求項２】
前記実行結果は、任意のタイミングにおける、前記サービスの組合せの実行開始、実行中、実行完了それぞれでの前記システムの出力状態を含む
ことを特徴とする請求項１に記載のモデル検査方法。
【請求項３】
前記実行結果は、前記サービスを実行する際の前提条件を任意に組合せた条件下で前記サービスの組合せを実行した場合の前記システムの出力状態を含む
ことを特徴とする請求項１又は２に記載のモデル検査方法。
【請求項４】
システムで動作させる２つ以上のサービスから２つのサービスを選択したサービスの組合せ毎のサービス実行の競合条件と、前記サービスの組合せを任意のタイミングで実行した場合の実行結果が満たすべき制約条件とを含む前記システムのモデルを、前記システムの仕様をもとに生成する生成部と、
前記サービス実行の競合条件をもとに、前記サービスの組合せを任意のタイミングで実行した場合の各実行結果を出力する出力部と、
前記出力部により出力された各実行結果が前記制約条件を満たすか否かを判定する判定部と
を備えたことを特徴とするモデル検査装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査方法及びモデル検査装置に関する。
【背景技術】
【０００２】
従来から、システム構築の際、システム仕様の検討の段階でシステム仕様の不備を検出するモデル検査が行われている。モデル検査では、システムの動作ロジックを定義する動作モデルを設計書から生成し、システムへの入力（イベント）を定義する入力モデル、システムの初期状態を定義する初期状態モデル、システムの制約条件を仕様書から生成する。モデル検査では、動作モデル、入力モデル、初期状態モデルから作成したシステムの状態遷移を示す状態遷移表を生成する。
【０００３】
そして、モデル検査では、イベント刈り取り順序（システムへのイベントの到着順序）やリソースの割り当て順序等の任意性に着目し、状態遷移表をもとにシステムの振る舞いを網羅した検証モデルを生成する。モデル検査では、システムのあらゆる振る舞いのうち、システムの制約条件を満たさない反例を検出する。そして、反例に基づき、システム仕様の不備が修正される。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】中島  震、“ＳＰＩＮモデル検査  検証モデリング技法”、２００８年４月３０日、株式会社近代科学社
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、上記技術では、システム上で動作する複数のサービスの競合の不備を検出することができない。これは、サービス競合仕様の検討段階では、動作ロジックが未設計であるため、動作ロジックからサービス競合の任意性を抽出できないためである。
【０００６】
本願が開示する実施形態の一例は、上記に鑑みてなされたものであって、システム上で動作するサービス競合仕様の検討段階であっても、サービス競合の不備を検出するモデル検査方法及びモデル検査装置を提供することを目的とする。
【課題を解決するための手段】
【０００７】
本願の実施形態の一例は、システムで動作させる２つ以上のサービスから２つのサービスを選択したサービスの組合せ毎のサービス実行の競合条件と、サービスの組合せを任意のタイミングで実行した場合の実行結果が満たすべき制約条件とを含むシステムのモデルを、システムの仕様をもとに生成する。そして、サービス実行の競合条件をもとに、サービスの組合せを任意のタイミングで実行した場合の各実行結果を出力する。そして、出力された各実行結果が制約条件を満たすか否かを判定する。
【発明の効果】
【０００８】
本願が開示する実施形態の一例によれば、システム上で動作するサービス競合仕様の検討段階であっても、サービス競合の不備を検出するモデル検査方法及びモデル検査装置を提供できる。
【図面の簡単な説明】
【０００９】
【図１】図１は、実施形態に係るモデル検査装置の一例を示すブロック図である。
【図２Ａ】図２Ａは、実施形態に係るシステム初期状態定義モデルの一例を示す図である。
【図２Ｂ】図２Ｂは、実施形態に係るシステム入力定義モデルの一例を示す図である。
【図２Ｃ】図２Ｃは、実施形態に係るサービス競合仕様表の一例を示す図である。
【図２Ｄ】図２Ｄは、実施形態に係るサービス競合検査モデル、動作判定表、制約条件の一例を示す図である。
【図３】図３は、実施形態に係るモデル検査処理の一例を示すフローチャートである。
【図４】図４は、実施形態に係るモデル検査処理の概要の一例を示す図である。
【図５】図５は、実施形態に係るモデル検査の適用例の一例を示す図である。
【図６】図６は、実施形態に係るモデル検査の適用例である電話システムにおけるサービス、プロパティ、出力状態の関連の一例を示す図である。
【図７】図７は、プログラムが実行されることによりモデル検証装置が実現されるコンピュータの一例を示す図である。
【発明を実施するための形態】
【００１０】
以下、本願が開示する実施形態を説明する。なお、以下の実施形態は、一例を示すに過ぎず、本願が開示する技術を限定するものではない。また、以下に示す実施形態、その変形例及び適用例が示す形態は、矛盾しない範囲内で適宜組合せてもよい。以下の実施形態、その変形例及び適用例が示す形態の説明では、重複する同一の構成又は処理は、同一符号を付与して説明を省略する。
【００１１】
［実施形態］
（実施形態に係るモデル検査装置）
図１は、実施形態に係るモデル検査装置の一例を示すブロック図である。実施形態に係るモデル検査装置１０は、複数のサービスを提供するシステム（サーバ）において、サービス仕様間の競合の不備を検査する。モデル検査装置１０は、入力装置２０、出力装置３０と接続される。モデル検査装置１０は、記憶部１１、モデル検査部１２を有する。
【００１２】
記憶部１１は、システム初期状態定義モデル１１ａ、システム入力定義モデル１１ｂ、サービス競合仕様表１１ｃ、サービス仕様競合検査モデル１１ｄ、制約条件１１ｅ、動作判定表１１ｆを保存する。システム初期状態定義モデル１１ａ、システム入力定義モデル１１ｂ、サービス競合仕様表１１ｃ、サービス仕様競合検査モデル１１ｄ、制約条件１１ｅは、入力装置２０から入力された、仕様書モデル検査対象のシステムの仕様情報をもとに生成される。
【００１３】
図２Ａは、実施形態に係るシステム初期状態定義モデルの一例を示す図である。システム初期状態定義モデル１１ａは、モデル検査対象のシステムの初期状態（状態０）を定義するモデルである。システム初期状態定義モデル１１ａは、モデル検査対象のシステムの初期状態を網羅する。例えば、モデル検査対象のシステムの初期状態として“状態Ａ”“状態Ｂ”が存在する場合、図２Ａに示すように、システム初期状態定義モデル１１ａは、“状態Ａ”“状態Ｂ”を含む。なお、実施形態では、モデル検査対象のシステムの初期状態は、一例として“状態Ａ”“状態Ｂ”の２つとするが、これに限らず、システムの仕様情報に応じて、２つ以外の数であってもよい。
【００１４】
図２Ｂは、実施形態に係るシステム入力定義モデルの一例を示す図である。システム入力定義モデル１１ｂは、モデル検査対象のシステムへの入力を定義するモデルである。システム入力定義モデル１１ｂは、モデル検査対象のシステムへの入力を網羅する。例えば、モデル検査対象のシステム上で、“α”“β”“γ”の３つのサービスが動作する場合、図２Ｂに示すように、システム入力定義モデル１１ｂは、これら３つのサービスのうち２つずつのサービスの組合せの“入力１（サービスα，βを入力）”“入力２（サービスβ，γを入力）”“入力３（サービスγ，αを入力）”を含む。なお、実施形態では、モデル検査対象のシステム上で動作するサービスは、“α”“β”“γ”の３つとするが、これに限らず、システムの仕様情報に応じて、３つ以外の数であってもよい。
【００１５】
図２Ｃは、実施形態に係るサービス競合仕様表の一例を示す図である。サービス競合仕様表１１ｃは、モデル検査対象における個々のサービスの競合仕様を定義するモデルである。サービス競合仕様表１１ｃは、例えば、モデル検査対象のシステム上で、“α”“β”“γ”の３つのサービスが動作する場合に、α×β、β×γ、γ×αのそれぞれの競合処理を１つの単位として、それぞれが動作した際の開始の順序、出力の順序、完了の順序、動作及び動作規制等の競合処理仕様をモデル化したものである。競合処理仕様とは、例えば、「α×βの処理中にα×γが動作」、「α×βが先行動作開始するが、β×γが先に終了する」等である。また、競合処理仕様の任意性とは、競合処理の仕様の網羅をいう。
【００１６】
例えば、図２Ｃに示すように、サービス競合仕様表１１ｃは、“α”“β”“γ”の３つのサービスのうちの２つずつのサービスの組合せの“入力１（サービスα，βを入力）”に対して（ａ）“αを動作させ、βは規制する”、“入力２（サービスβ，γを入力）”に対して（ｂ）“γの動作後、βを動作させる”、“入力３（サービスγ，αを入力）”に対して（ｃ）“γの動作後、αを動作させる”を含む。
【００１７】
図２Ｄは、実施形態に係るサービス競合検査モデル、動作判定表、制約条件の一例を示す図である。サービス仕様競合検査モデル１１ｄは、モデル検査対象のシステムの仕様に付随するシステムの任意性を有する振る舞いをモデル化したものである。サービス競合検査モデルにおける各サービスの入力タイミング、出力タイミング等に関し、実装可能な全パターンが後述の制約条件を満たしているかを検査することにより、モデル検査においてサービス競合の観点からシステムの仕様を検証する。システムの仕様情報等から導かれるサービスに係るシステムの各振る舞いにおけるシステムへの入力やシステム状態（出力状態）は、各サービスの仕様により共有して参照、更新される。また、システム状態は、入力に対する出力に該当するシステム状態のうち、実装可能なパターンの全てが試行される。
【００１８】
例えば、図２Ｄに示すように、サービス仕様競合検査モデル１１ｄは、タイミングＴ０からＴ１の間に、“入力１（サービスα，βを入力）”“入力２（サービスβ，γを入力）”“入力３（サービスγ，αを入力）”がシステムへ入力され、各入力と対応する処理が実行されるパターンを示す。サービス仕様競合検査モデル１１ｄは、サービス競合仕様表１１ｃをもとに、システムの振る舞いを例えばモデル記述言語で記述したものである。
【００１９】
ここで、“入力１”と対応する（ａ）“αを動作させ、βは規制する”の開始タイミングをｔ１１、出力タイミングをｔ１２、完了タイミングをｔ１３とする。また、“入力２”と対応する（ｂ）“γの動作後、βを動作させる”の開始タイミングをｔ２１、出力タイミングをｔ２２、完了タイミングをｔ２３とする。また、“入力３”と対応する（ｃ）“γの動作後、αを動作させる”の開始タイミングをｔ３１、出力タイミングをｔ３２、完了タイミングをｔ３３とする。
【００２０】
サービス仕様競合検査モデル１１ｄは、各タイミングｔ１１〜ｔ１３，ｔ２１〜ｔ２３，ｔ３１〜ｔ３３がＴ０≦ｔ１１＜ｔ１２＜ｔ１３≦Ｔ１、Ｔ０≦ｔ２１＜ｔ２２＜ｔ２３≦Ｔ１、Ｔ０≦ｔ３１＜ｔ３２＜ｔ３３≦Ｔ１の順序を保つ限りにおいて、任意のタイミングとなるパターンを網羅する。図２Ｄは、例えば、サービス仕様競合検査モデル１１ｄが網羅するパターンのうち、各タイミングがｔ１１、ｔ１２、ｔ２１、ｔ１３、ｔ２２、ｔ３１、ｔ２３、ｔ３２、ｔ３３の順序で発生するケースを示している。
【００２１】
図２Ｄに示すように、例えば、タイミングｔ１１において（ａ）の処理の開始に応じて、システムの状態が“状態０”（初期状態）から“状態１”へ更新される。そして、タイミングｔ１２において（ａ）の処理の出力に応じて、システムの状態が“状態１”から“状態２”へ更新される。そして、タイミングｔ２１において（ｂ）の処理の開始に応じて、システムの状態が“状態２”から“状態３”へ更新される。そして、タイミングｔ１３において（ａ）の処理の終了に応じて、システムの状態が“状態３”から“状態４”へ更新される。
【００２２】
また、図２Ｄに示すように、タイミングｔ２２において（ｂ）の処理の出力に応じて、システムの状態が“状態４”から“状態５”へ更新される。また、タイミングｔ３１において（ｃ）の処理の開始に応じて、システムの状態が“状態５”から“状態６”へ更新される。また、タイミングｔ２３において（ｂ）の処理の完了に応じて、システムの状態が“状態６”から“状態７”へ更新される。また、タイミングｔ３２において（ｃ）の処理の出力に応じて、システムの状態が“状態７”から“状態８”へ更新される。また、タイミングｔ３３において（ｃ）の処理の完了に応じて、システムの状態が“状態８”から“状態９”へ更新される。
【００２３】
そして、全ての処理が終了した後のシステムの状態“状態９”が検査対象のパターンと対応する動作結果として後述の動作判定表１１ｆへ記録される。このように、各入力と対応する処理が実行されるあらゆるパターンと、それらパターンの実行前後にシステムが取り得る全ての状態とが対応付けられて動作判定表１１ｆへ記録される。そして、制約条件１１ｅと照らし合わされ、制約条件１１ｅを満たさないシステムの状態となるパターンが反例として検出される。
【００２４】
制約条件１１ｅは、システムの仕様書等から導かれる、システムが満たすべき状態や生起してはならないシステムの状態等を、例えば時相論理式で表現したものである。例えば、図２Ｄに示すように、制約条件１１ｅは、“（サービス）α動作時には、必ず（サービス）βは規制（非動作）”等である。
【００２５】
モデル検査部１２は、モデル生成部１２ａ、モデル検査実行部１２ｂ、競合判定部１２ｃを有する。モデル生成部１２ａは、入力装置２０から入力されたシステムの仕様書等に基づく仕様情報から、システム初期状態定義モデル１１ａ、システム入力定義モデル１１ｂ、制約条件１１ｅを生成する。また、モデル生成部１２ａは、システムの仕様書等に基づく仕様情報、システム初期状態定義モデル１１ａ、システム入力定義モデル１１ｂから、サービス競合仕様表１１ｃを生成する。また、モデル生成部１２ａは、サービス競合仕様表１１ｃからサービス仕様競合検査モデル１１ｄを生成する。
【００２６】
モデル検査実行部１２ｂは、サービス仕様競合検査モデル１１ｄが網羅するパターンを実行する。そして、モデル検査実行部１２ｂは、実行した各パターンと、各パターンの実行終了後のシステムの各状態とを対応付けて、動作判定表１１ｆへ記録する。
【００２７】
競合判定部１２ｃは、制約条件１１ｅを参照し、動作判定表１１ｆへ記録された、各パターンの実行終了後のシステムの各状態のうち、制約条件１１ｅを充足しない各パターン及び対応するシステムの状態を検出する。そして、競合判定部１２ｃは、制約条件１１ｅを充足しない各パターン及び対応するシステムの状態に関する情報を、出力装置３０へ出力する。
【００２８】
（実施形態に係るモデル検査処理）
図３は、実施形態に係るモデル検査処理の一例を示すフローチャートである。先ず、モデル生成部１２ａは、システム仕様情報を取得する（ステップＳ１１）。次に、モデル生成部１２ａは、ステップＳ１１で取得したシステム仕様情報から、システム初期状態定義モデル１１ａを生成する（ステップＳ１２）。
【００２９】
次に、モデル生成部１２ａは、ステップＳ１１で取得したシステム仕様情報から、システム入力定義モデル１１ｂを生成する（ステップＳ１３）。次に、モデル生成部１２ａは、ステップＳ１１で取得したシステム仕様情報、システム初期状態定義モデル１１ａ、システム入力定義モデル１１ｂから、サービス競合仕様表１１ｃを生成する（ステップＳ１４）。
【００３０】
次に、モデル生成部１２ａは、ステップＳ１４で生成したサービス競合仕様表１１ｃから、サービス仕様競合検査モデル１１ｄを生成する（ステップＳ１５）。次に、モデル生成部１２ａは、ステップＳ１１で取得したシステム仕様情報から、制約条件１１ｅを生成する（ステップＳ１６）。次に、モデル検査実行部１２ｂは、ステップＳ１５で生成したサービス仕様競合検査モデル１１ｄのモデル検査を実行し、実行終了後のシステムの状態を動作判定表１１ｆへ記録する（ステップＳ１７）。
【００３１】
次に、競合判定部１２ｃは、制約条件１１ｅを参照し、動作判定表１１ｆへ記録された、各パターンの実行終了後のシステムの各状態のうち、制約条件１１ｅを充足しない各パターン及び対応するシステムの状態を検出する競合判定を行う（ステップＳ１８）。次に、競合判定部１２ｃは、制約条件１１ｅを充足しない各パターン及び対応するシステムの状態に関する情報を、出力装置３０へ出力する（ステップＳ１９）。
【００３２】
（実施形態に係るモデル検査処理の概要）
以上の実施形態の概略を、図４を参照して説明する。図４は、実施形態に係るモデル検査処理の概要の一例を示す図である。図４の例では、サービスは、“α＝代表”、“β＝転送”、“γ＝番号拒否”の３つとする。また、サービス競合仕様表１１ｃにおいて、“α×β”の処理において“（ａ）＝代表を動作させ、転送は規制する”、“β×γ”の処理において“（ｂ）＝番号拒否の動作後、転送を動作させる”、“γ×α”の処理において“（ｃ）＝番号拒否の動作後、代表を動作させる”とする。
【００３３】
また、図４の例では、（ａ）〜（ｃ）の処理順序として、“ケース１＝（ｂ）→（ｃ）→（ａ）”、“ケース２＝（ｂ）→（ａ）→（ｃ）”、“ケース３＝（ａ）→（ｃ）→（ｂ）”・・・のケースが存在するとする。また、図４の例では、制約条件１１ｅは、“検査式：「代表動作時には、必ず転送は規制」”である。
【００３４】
そして、“ケース１”の順序“（ｂ）→（ｃ）→（ａ）”で処理が入力された順に競合判定処理を評価してシステムの状態を更新し、最後の処理完了後のシステム状態“α（代表）：動作、β（転送）：規制、γ（番号拒否）：動作”を動作判定表１１ｆへ記録する。同様に、“ケース２”の順序“（ｂ）→（ａ）→（ｃ）”で処理が入力された順に競合判定処理を評価してシステムの状態を更新し、最後の処理完了後のシステム状態“α（代表）：動作、β（転送）：規制、γ（番号拒否）：動作”を動作判定表１１ｆへ記録する。同様に、“ケース３”の順序“（ａ）→（ｃ）→（ｂ）”で処理が入力された順に競合判定処理を評価してシステムの状態を更新し、最後の処理完了後のシステム状態“α（代表）：動作、β（転送）：動作、γ（番号拒否）：動作”を動作判定表１１ｆへ記録する。
【００３５】
そして、動作判定表１１ｆへ記録されたシステム状態のうち、制約条件１１ｅを満たさない反例である“ケース３”を検出する。すなわち、動作判定表１１ｆへ記録されたシステム状態のうち、制約条件１１ｅの反例が存在する場合には、サービス競合仕様に不備があるので、サービス競合仕様表１１ｃ又はシステムの仕様が修正される。
【００３６】
以上の実施形態によれば、複数のサービスを提供するシステムにおいて、サービスの動作ロジックが未設計である仕様設計段階であっても、２つのサービス間の競合仕様（２重サービス競合仕様）を１つの単位として、それらを複数動作させた場合の動作順序、出力順序の任意性に着目してモデル化を行うことで、サービス間の競合仕様の不備を機械的に厳密かつ網羅的に検出することができる。
【００３７】
よって、例えば、サービスα、β、γの３重サービス競合仕様の場合、条件（１）「α×β」、（２）「β×γ」、（３）「γ×α」として、（１）、（２）、（３）をいかなる順序で評価した結果も一致するか検査することで、「α×β×γ」といった複雑な競合条件を考えることなく、３重サービス競合仕様を２重サービス競合仕様へ単純化して検証可能となる。同様に、例えば、４重サービス仕様競合の場合は、条件（４）「α×δ」、（５）「β×δ」、（６）「γ×δ」を追加して検証できる。すなわち、サービス多重競合（３重以上の競合）に対しても、人手で複雑な競合条件を考えることなく、検査が可能となる。
【００３８】
（実施形態に係るモデル検査の適用例）
図５は、実施形態に係るモデル検査の適用例の一例を示す図である。また、図６は、実施形態に係るモデル検査の適用例である電話システムにおけるサービス、プロパティ、出力状態の関連の一例を示す図である。図５及び図６は、電話システムにおけるサービスの競合検証を行う実装例を示す。
【００３９】
図５に示すように、モデル検査対象である電話システムには、“代表”、“転送”、“着信拒否”、・・・のサービスを有する。また、図６に示すように、電話システムの各端末の“プロパティ”として、“呼の属性”、“端末の契約状態”、“各サービスの設定”、“端末通信状態”、・・・等がある。“プロパティ”は、サービスの起動に必要な契約条件や、話中、不在等の端末の条件を定義する情報である。“呼の属性”には、“発呼”“着呼”・・・等がある。“端末の契約状態”には、“端末（ａ）はサービスＡを契約している”“端末（ｂ）はサービスＢを契約している”・・・等がある。“各サービスの設定”には、“転送サービス：圏外転送・話中転送”“指定番号拒否：指定名番号”・・・等がある。“端末通信状態”には、“圏外”“不在”・・・等がある。
【００４０】
また、図６に示すように、電話システムの出力状態として、“端末のサービス動作状態：規制・作動１（優先作動）・作動２（後発作動）”・・・等がある。
【００４１】
例えば、図５に示すように、電話システムの各“サービス”は、配列Ａ１にフラグと共に格納される。また、図５に示すように、電話システムの各“プロパティ”は、配列Ａ２にフラグと共に格納される。“プロパティ”は、例えば電話システムのように、発呼側の電話端末と、着呼側の電話端末が存在する場合には、発呼側の電話端末及び着呼側の電話端末毎に設定される。また、図５に示すように、電話システムの各“出力状態”は、配列Ａ３にフラグと共に格納される。なお、配列Ａ３は、図１に示す動作判定表１１ｆの一態様である。
【００４２】
図５に示すように、モデル検査装置１０（図１）は、モデル検査のステップＳ２１の初期化において、配列Ａ１〜Ａ３の初期化を行い、電話システムが有する全てのサービス、プロパティを配列Ａ１〜Ａ２それぞれへフラグ“０”と共に格納する。また、モデル検査装置１０は、ステップＳ２１の初期化において、配列Ａ３の初期化を行い、電話システムが有する全ての出力状態を配列Ａ３へステータス情報“初期値”と共に格納する。すなわち、モデル検査装置１０は、ステップＳ２１において、サービス、プロパティ、出力状態をそれぞれ配列としてモデル化する。
【００４３】
次に、モデル検査装置１０は、モデル検査のステップＳ２２において、サービス及びプロパティを選択する。モデル検査装置１０は、例えば３重サービス競合仕様検証の場合、サービスの配列から３つのサービスを選択する。そして、モデル検査装置１０は、選択したサービス及びプロパティの配列のフラグを“１”とする。ここで、モデル検査装置１０が選択するサービス及びプロパティの数は、モデル検査対象である電話システムの任意性に鑑み、ランダムである。
【００４４】
次に、モデル検査装置１０は、モデル検査のステップＳ２３において、例えば３重サービス競合を２重サービス競合へ単純化し、ランダムな順序で２重サービス競合を起動、出力、終了することで、サービス多重競合の動作仕様をモデルに組込む。ただし、各２重サービス競合内における起動、出力、終了の順序はこの順序が保たれる。モデル検査装置１０は、ランダムな順序で各２重サービス競合を起動、出力、終了すると、プロパティの値により異なる２重サービス競合の動作結果を出力状態の配列Ａ３の各出力状態のステータスを初期値から更新することで格納する。
【００４５】
次に、モデル検査装置１０は、モデル検査のステップＳ２４において、ステップＳ２３で得られた出力状態の配列Ａ３と、電話システムの仕様から予め生成した検査式とを比較し、検査式を満たさない出力状態を示す配列Ａ３を検出することで、サービス競合仕様の不整合がないかを検証する。
【００４６】
そして、モデル検査装置１０は、ステップＳ２１〜Ｓ２４の処理を、全てのサービスの選択パターン、プロパティの選択パターン、各２重サービスの競合の起動、出力、終了の全てのタイミングについて繰り返し、仕様に付随する任意性の振る舞いをモデル化してサービス競合を網羅的に検証する。
【００４７】
（モデル検証装置の装置構成について）
上記の実施形態、その変形例及び適用例が示す形態で示したモデル検査装置１０の各構成要素は機能概念的なものであり、必ずしも物理的に図示のように構成されていることを要さない。すなわち、モデル検査装置１０の機能の分散及び統合の具体的形態は図示のものに限られず、全部又は一部を、各種の負荷や使用状況等に応じて、任意の単位で機能的又は物理的に分散又は統合して構成することができる。
【００４８】
また、モデル検査装置１０において行われる各処理は、全部又は任意の一部が、ＣＰＵ（Central  Processing  Unit）等の処理装置及び処理装置により解析実行されるプログラムにて実現されてもよい。また、モデル検査装置１０において行われる各処理は、ワイヤードロジックによるハードウェアとして実現されてもよい。
【００４９】
また、上記の実施形態、その変形例及び適用例が示す形態において説明した各処理のうち、自動的に行われるものとして説明した処理の全部又は一部を手動的に行うこともできる。もしくは、上記の実施形態、その変形例及び適用例が示す形態において説明した各処理のうち、手動的に行われるものとして説明した処理の全部又は一部を公知の方法で自動的に行うこともできる。この他、上記及び図示の処理手順、制御手順、具体的名称、各種のデータやパラメータを含む情報については、特記する場合を除いて適宜変更することができる。
【００５０】
（プログラムについて）
図７は、プログラムが実行されることによりモデル検証装置が実現されるコンピュータの一例を示す図である。コンピュータ１０００は、例えば、メモリ１０１０、ＣＰＵ１０２０を有する。また、コンピュータ１０００は、ハードディスクドライブインタフェース１０３０、ディスクドライブインタフェース１０４０、シリアルポートインタフェース１０５０、ビデオアダプタ１０６０、ネットワークインタフェース１０７０を有する。コンピュータ１０００において、これらの各部はバス１０８０によって接続される。
【００５１】
メモリ１０１０は、ＲＯＭ（Read  Only  Memory）１０１１及びＲＡＭ（Random  Access  Memory）１０１２を含む。ＲＯＭ１０１１は、例えば、ＢＩＯＳ（Basic  Input  Output  System）等のブートプログラムを記憶する。ハードディスクドライブインタフェース１０３０は、ハードディスクドライブ１０３１に接続される。ディスクドライブインタフェース１０４０は、ディスクドライブ１０４１に接続される。例えば磁気ディスクや光ディスク等の着脱可能な記憶媒体が、ディスクドライブ１０４１に挿入される。シリアルポートインタフェース１０５０は、例えばマウス１０５１、キーボード１０５２に接続される。ビデオアダプタ１０６０は、例えばディスプレイ１０６１に接続される。
【００５２】
ハードディスクドライブ１０３１は、例えば、ＯＳ（Operating  System）１０９１、アプリケーションプログラム１０９２、プログラムモジュール１０９３、プログラムデータ１０９４を記憶する。すなわち、モデル検査装置１０の各処理を規定するプログラムは、コンピュータ１０００によって実行される指令が記述されたプログラムモジュール１０９３として、例えばハードディスクドライブ１０３１に記憶される。例えば、モデル検査装置１０における機能構成と同様の情報処理を実行するためのプログラムモジュール１０９３が、ハードディスクドライブ１０３１に記憶される。
【００５３】
また、上記の実施形態、その変形例及び適用例が示す形態の処理で用いられる設定データは、プログラムデータ１０９４として、例えばメモリ１０１０やハードディスクドライブ１０３１に記憶される。そして、ＣＰＵ１０２０が、メモリ１０１０やハードディスクドライブ１０３１に記憶されたプログラムモジュール１０９３やプログラムデータ１０９４を必要に応じてＲＡＭ１０１２に読み出して実行する。
【００５４】
なお、プログラムモジュール１０９３やプログラムデータ１０９４は、ハードディスクドライブ１０３１に記憶される場合に限らず、例えば着脱可能な記憶媒体に記憶され、ディスクドライブ１０４１等を介してＣＰＵ１０２０によって読み出されてもよい。あるいは、プログラムモジュール１０９３やプログラムデータ１０９４は、ネットワーク（ＬＡＮ（Local  Area  Network）、ＷＡＮ（Wide  Area  Network）等）を介して接続された他のコンピュータに記憶されてもよい。そして、プログラムモジュール１０９３やプログラムデータ１０９４は、ネットワークインタフェース１０７０を介してＣＰＵ１０２０によって読み出されてもよい。
【００５５】
上記の実施形態、その変形例及び適用例が示す形態は、本願が開示する技術に含まれると同様に、特許請求の範囲に記載された発明とその均等の範囲に含まれるものである。
【符号の説明】
【００５６】
１０  モデル検査装置
１１  記憶部
１１ａ  システム初期状態定義モデル
１１ｂ  システム入力定義モデル
１１ｃ  サービス競合仕様表
１１ｄ  サービス仕様競合検査モデル
１１ｅ  制約条件
１１ｆ  動作判定表
１２  モデル検査部
１２ａ  モデル生成部
１２ｂ  モデル検査実行部
１２ｃ  競合判定部
２０  入力装置
３０  出力装置
【図１】
2017146728.tif 000003
【図２Ａ】
2017146728.tif 000004
【図２Ｂ】
2017146728.tif 000005
【図２Ｃ】
2017146728.tif 000006
【図２Ｄ】
2017146728.tif 000007
【図３】
2017146728.tif 000008
【図４】
2017146728.tif 000009
【図５】
2017146728.tif 000010
【図６】
2017146728.tif 000011
【図７】
2017146728.tif 000012