(57)【要約】  到着する負荷の確率に対してシステムの性能が保証されていることを数理的に証明できる検証システムを提供する。検証システム５０は、述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され検査対象システムが述語で表現されている性能要件を充足することを示す命題を生成する生成部５１と、生成された命題の証明の正否を検証する検証部５２を備える。
2017188037.tif 000002
【特許請求の範囲】
【請求項１】
述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され、前記検査対象システムが前記述語で表現されている性能要件を充足することを示す命題を生成する生成手段と、
生成された前記命題の証明の正否を検証する検証手段を備える
検証システム。
【請求項２】
検査対象システムの構成を示すモデルを数理的なモデルに変換するモデル変換手段を備える
請求項１記載の検証システム。
【請求項３】
生成手段は、検査対象システムにかかる負荷の確率の時系列が合成された述語に数理的なモデルを入力とする
請求項１または請求項２記載の検証システム。
【請求項４】
負荷イベントを示す情報を検査対象システムにかかる負荷の確率の時系列に変換するイベント変換手段を備え、
生成手段は、変換された前記時系列が合成された述語に数理的なモデルを入力とする
請求項３記載の検証システム。
【請求項５】
検査対象システムの構成を示すモデルは、アクティビティ図に記載されているモデル、またはマークアップ言語で記述されているモデルである
請求項１から請求項４のうちのいずれか１項に記載の検証システム。
【請求項６】
性能要件は、高階述語論理における述語で表現されている
請求項１から請求項５のうちのいずれか１項に記載の検証システム。
【請求項７】
述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され前記検査対象システムが前記述語で表現されている性能要件を充足することを示す命題を生成し、
生成された前記命題の証明の正否を検証する
検証方法。
【請求項８】
検査対象システムの構成を示すモデルを数理的なモデルに変換する
請求項７記載の検証方法。
【請求項９】
コンピュータに、
述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され前記検査対象システムが前記述語で表現されている性能要件を充足することを示す命題を生成し、
生成された前記命題の証明の正否を検証する
ことを実行させる検証プログラムを格納する記録媒体。
【請求項１０】
コンピュータに、
検査対象システムの構成を示すモデルを数理的なモデルに変換する変換処理を実行させる
請求項９記載の検証プログラムを格納する記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システムの非機能要件を検証する検証システム等に関する。
【背景技術】
【０００２】
実世界の環境における情報をセンサで計測（センシング）し、センシングにより得られるデータに対して計算処理を実行した上で制御処理を行うシステムがある。システムによる制御結果が大きな影響を及ぼす場合、設計者には、注意深くシステムの設計、開発および検証を行うことが求められる。【０００３】
一般的に、システム要件は、機能要件と非機能要件に分類される。機能要件は、情報システム又はソフトウェアの開発において定義される要件のうち、機能に関する要件である。
機能要件には、扱われるデータの種類や構造、処理内容、画面表示形式、操作方法、および帳票等の出力形式等に関する要件が含まれる。【０００４】
非機能要件は、情報システム又はソフトウェアの開発において定義される要件のうち、機能要件以外の要件全般である。非機能要件には、性能、信頼性、拡張性、運用性、およびセキュリティ等に関する要件が含まれる。非機能要件が充足されているか否かの判定には、待ち行列が用いられるシミュレーション技術が使用されることが多い。【０００５】
システムの設計者には、システムに入力される情報に対する計算処理の負荷を予め予測することが求められる。計算処理の負荷は、イベントの発生タイミング又は処理を要するデータの量に依存する。【０００６】
しかし、設計者がイベントの発生タイミング又は処理を要するデータの量をシステム設計時に予測することは困難である。すなわち、設計者がシステム設計時に計算処理の負荷を予測することは困難である。【０００７】
以下、システムに負荷がかかることを、システムに負荷が到着するという。実世界で発生するイベントに起因する負荷の予測が困難であるため、例えばシステムに到着する負荷の分布を作成し、作成された分布を用いて非機能要件が充足されているか否かを判定する方法が代替策として採用される。【０００８】
上記の代替策で非機能要件が充足されていると判定された場合であっても、作成された分布から外れた負荷は、所定の非機能要件を充足しない可能性がある。充足しない負荷が存在する可能性がある非機能要件を有するシステムが使用されると、実世界に影響を及ぼすインシデントが発生する恐れがある。【０００９】
また、待ち行列理論では、解析的に解くことが可能な関数で表現される分布が知られている。解析的に解くことが可能な関数で表現される分布が用いられると、システムの設計者は、非機能要件が充足されているか否かという問題を解析的に解くことができる。【００１０】
解析的に解くことが困難な関数で表現される分布が用いられる場合、システムの設計者は、例えばモンテカルロ法等でシステムに到着する負荷である到着負荷をサンプリングする。次いで、設計者は、サンプリングの結果に対するシミュレーションを実行することによって、到着負荷全体に対するシステムの性能を統計的に見積る。なお、本明細書において１つの値を関数に適用する操作をサンプリング、計算処理をシミュレーションという。【００１１】
上記の方法でシステム構成が決定されてもシステムの性能は統計的にしか見積られていないため、サンプリングされなかった到着負荷に対するシステムの性能は、完全には保証されていない。【００１２】
例えば、定義域がｘ＝［０，π］であるｓｉｎ（ｘ）の平均値をシミュレーションで求める場合を考える。平均値を求める方法に、例えばｘ＝０からｘ＝πまでｘを０．０１ずつ増加させながらｓｉｎ（ｘ）を計算し、計算結果の平均値を算出する方法がある。【００１３】
しかし、上記のように増加幅が０．０１である場合、ｓｉｎ（ｘ）の正確な平均値は算出されない。正確な平均値を算出するためには、増加幅を無限小の区間にすることが求められる。【００１４】
一方、増加幅が無限小の区間である場合、計算回数が無限になり、シミュレーションが実行不可能になる。すなわち、変数が取り得る値は無限に存在し得るがシミュレーションでは１つの値に対して計算が行われるため、関数に含まれる変数が取り得る全ての値に対するシミュレーションの実行は、原理上不可能である。
【先行技術文献】
【特許文献】
【００１５】
【特許文献１】特許第５８４３２３０号公報
【発明の概要】
【発明が解決しようとする課題】
【００１６】
上記の通り、システムに到着する負荷の分布が解析的に解くことが困難な関数で表現されると、既知の方法では統計的に見積られた性能しか保証されない。既知の方法を用いて、システムに到着する負荷の環境の変化に起因する変化が大きなシステムの性能を網羅的に保証することは困難である。【００１７】
また、分布から外れた到着負荷が所定の割合で存在することを考慮すると、システムに到着する負荷の確率に対してシステムの性能が保証されているか否かが検証された方が、保証の網羅性がより高いシステムが設計される。【００１８】
システムの性能を網羅的に保証するためには、解析的に解くことが可能な数理的なモデルで表現される到着負荷の分布を用いて、システムの性能が保証されているか否かという問題を数理的な手法で解くことが求められる。【００１９】
しかし、数理的な手法で使用される数理的なモデルを数理学の専門家ではない設計者が記述することは困難である。その理由は、数理的なモデルの構築には、数理学の背景知識が要求されるためである。【００２０】
特許文献１には、ハイブリッドシステムの検証方法およびハイブリッドシステムのモデル変換方法が記載されている。特許文献１の検証方法は、ハイブリッドシステムが設計通りに動作するか否かを検証する。【００２１】
特許文献１の検証方法は、ハイブリッドシステムの動作をプログラミング言語でコーディングされたモデルを作成し、モデルのコードの検証条件を示す論理式を生成し、生成された論理式を定理証明器で証明することによって、モデルのコードを検証する。すなわち、特許文献１の検証方法は、ハイブリッドシステムの動作が保証されているか否かという問題を数理的な手法で解いている。【００２２】
しかし、特許文献１のハイブリッドシステムは、連続値と離散値とが相互に影響を与えながら動作するシステムである。すなわち、特許文献１の検証方法では、確率が入力の対象として想定されていない。【００２３】
到着する負荷の確率に対して性能が保証されているか否かを数理的に確かめるには、例えば性能要件を後述する述語論理における述語で表現することが考えられる。その理由は、述語は確率を持つ負荷に対応するように性能要件を表現できるためである。【００２４】
また、特許文献１の検証方法では、ＳｙｓＭＬ（Ｓｙｓｔｅｍｓ  Ｍｏｄｅｌｉｎｇ  Ｌａｎｇｕａｇｅ）で記述された内容を基に数理的なモデルを生成することが想定されていない。【００２５】
［発明の目的］
そこで、本発明は、上述した課題を解決する、到着する負荷の確率に対してシステムの性能が保証されていることを数理的に証明できる検証システム等を提供することを目的とする。
【課題を解決するための手段】
【００２６】
本発明による検証システムの一態様は、述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され検査対象システムが述語で表現されている性能要件を充足することを示す命題を生成する生成部と、生成された命題の証明の正否を検証する検証部を備える。【００２７】
本発明による検証方法の一態様は、述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され検査対象システムが述語で表現されている性能要件を充足することを示す命題を生成し、生成された命題の証明の正否を検証する。【００２８】
本発明による記録媒体に格納された検証プログラムの一態様は、コンピュータに、述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され検査対象システムが述語で表現されている性能要件を充足することを示す命題を生成する生成処理、および生成された命題の証明の正否を検証する検証処理を実行させる。
【発明の効果】
【００２９】
本発明によれば、到着する負荷の確率に対してシステムの性能が保証されていることを数理的に証明できる。
【図面の簡単な説明】
【００３０】
【図１】第１の実施形態の検証システム１００の構成例を示すブロック図である。
【図２】本実施形態の検証システム１００による検証処理の動作を示すフローチャートである。
【図３】第２の実施形態の検証システム１００の構成例を示すブロック図である。
【図４】第２の実施形態の検証システム１００による検証処理の動作を示すフローチャートである。
【図５】検証対象のシステムモデルを表すアクティビティ図である。
【図６】本発明による検証システムの概要を示すブロック図である。
【発明を実施するための形態】
【００３１】
（第１実施形態）
［構成の説明］
以下、本発明の実施形態を、図面を参照して説明する。図１は、第１の実施形態の検証システム１００の構成例を示すブロック図である。図１に示すように、本実施形態の検証システム１００は、モデル変換部１０１と、検証部１０２とを含む。
【００３２】
モデル変換部１０１は、システムモデルを基に負荷関数を生成する機能を有する。モデル変換部１０１には、例えばシステムモデルが記載されたアクティビティ図が入力される。
【００３３】
アクティビティ図は、連続する処理（プロセス）の遷移を表現する図である。アクティビティ図には、所定の事象の開始から終了までに実行される処理が実行順に記載される。
アクティビティ図は、例えばＳｙｓＭＬで記述される。
【００３４】
なお、アクティビティ図は、ＳｙｓＭＬ以外の言語で記述されてもよい。また、モデル変換部１０１には、例えばマークアップ言語で記述されたシステムモデルが入力されてもよい。
【００３５】
モデル変換部１０１は、アクティビティ図に記載されているコンポーネントの識別子と、個々のコンポーネント内のプロセスにおける負荷に対する性能の情報を返す関数とを基に、全てのプロセスにおける負荷に対する性能の情報が統合された情報を返す負荷関数を生成する。生成された負荷関数は、到着負荷の時系列を入力とし、性能の時系列を返す関数である。
【００３６】
モデル変換部１０１は、取り扱いが容易なアクティビティ図から検証可能な負荷関数を生成する。生成された負荷関数が、検証部１０２による検査の対象の関数になる。
【００３７】
検証部１０２は、入力された証明の正否を検証する機能を有する。検証部１０２は、定理証明支援器（図示せず）を含む。検証部１０２は、入力された証明を定理証明支援器に入力し、定理証明支援器に証明の正否を検証させる。
【００３８】
検証部１０２には、生成された負荷関数がモデル変換部１０１から入力される。また、検証部１０２には、要求される性能（以下、要求性能という。）を表す述語が入力される。検証部１０２は、入力された負荷関数を、入力された述語に適用することによって命題を生成する。
【００３９】
また、検証部１０２には、負荷関数が与えられた要求性能を表す述語である命題が成立することを証明する内容が入力される。証明の内容は、例えば設計者によって作成され、検証部１０２に入力される。なお、検証部１０２には、命題が成立しないことを証明する内容が入力されてもよい。
【００４０】
入力された証明が正しければ、検証部１０２は、証明が正しいことを示す検証結果を出力する。また、証明が誤っていれば、検証部１０２は、証明が誤っていることを示す検証結果を出力する。
【００４１】
なお、述語は、数理論理学における記号的形式体系群を意味する述語論理における用語である。例えば、変数ｘの性質Ｐを「Ｐ（ｘ）」と表す場合、「Ｐ」が述語、「Ｐ（ｘ）」が命題にそれぞれ相当する。なお、ｘは変数ではなく、命題でもよい。述語論理において、命題は、真偽が一意に決定される式である。また、命題に含まれる変数を後から与える式が、変数に対する述語である。
【００４２】
すなわち、本実施形態において、検査対象の要求性能は述語論理における述語で表現されている。なお、本実施形態では一階述語論理における述語が使用されるが、要求性能は高階述語論理における述語で表現されてもよい。また、本実施形態で使用される述語は、負荷の確率分布が予め合成された述語である。
【００４３】
検証部１０２には、負荷関数、検査対象の要求性能を表す述語、および作成された証明が入力される。検証部１０２は、例えば入力された情報を定理証明支援器に与えることによって、定理証明支援器に証明の正否を判定させる。なお、定理証明支援器以外の検証部１０２に含まれる構成要素が、証明の正否を判定してもよい。
【００４４】
［動作の説明］
以下、本実施形態の検証システム１００の証明を検証する動作を図２を参照して説明する。図２は、第１の実施形態の検証システム１００による検証処理の動作を示すフローチャートである。
【００４５】
図２に示すように、ステップＳ１０１〜ステップＳ１０４の処理は、モデル変換部１０１により実行される。まず、モデル変換部１０１に、アクティビティ図が入力される。
【００４６】
モデル変換部１０１は、入力されたアクティビティ図が示す内容に対して成分分解を行う（ステップＳ１０１）。成分分解を行うことによって、モデル変換部１０１は、各プロセスにおける負荷の情報、プロセスの識別子、およびプロセスの接続関係を抽出する。
【００４７】
次いで、モデル変換部１０１は、各プロセスにおける負荷の情報を基に負荷関数を生成する（ステップＳ１０２）。
【００４８】
ステップＳ１０２の処理の実行と同時に、モデル変換部１０１は、負荷関数のプレースホルダ、プロセスの識別子、およびプロセスの接続関係を示す各情報を結合することによって、プレースホルダ付き負荷関数を生成する（ステップＳ１０３）。なお、プレースホルダは、後から挿入される内容のために仮に確保された箇所である。
【００４９】
次いで、モデル変換部１０１は、ステップＳ１０２で生成された負荷関数と、ステップＳ１０３で生成されたプレースホルダ付き負荷関数とを合成する（ステップＳ１０４）。
具体的には、モデル変換部１０１は、プレースホルダ付き負荷関数のプレースホルダに対して生成された負荷関数を適用することによって、負荷関数全体を生成する。
【００５０】
図２に示すように、ステップＳ１０５〜ステップＳ１０７の処理は、検証部１０２により実行される。次いで、検証部１０２に、ステップＳ１０４で生成された負荷関数が入力される。入力された負荷関数は、負荷の時系列を入力とし、性能の時系列を返す関数である。
【００５１】
次いで、検証部１０２は、入力された負荷関数に対して、確率に対する高次化処理を行う。高次化処理が行われると、負荷関数は、負荷の確率の時系列を入力とし、性能の確率の時系列を返す関数に変換される。
【００５２】
例えば、高次化処理が行われる前の負荷関数は、［１，２，３，４，５］のような時系列データである負荷の時系列が入力されると、［１，２，３，３，３］のような時系列データである性能の時系列を返す。
【００５３】
しかし、本実施形態における処理の対象である負荷の確率の時系列は、負荷の時系列のデータである［１，２，３，４，５］に確率が付与された［（（０．５，１），（０．５，２）），・・・］のような時系列データである。負荷の確率の時系列のデータにおいて、「０．５」が確率である。
【００５４】
検証部１０２は、例えば入力された負荷関数の構造を各確率分岐上で計算が行われる高次のｍａｐ関数の構造に変換することによって、確率に対する高次化処理を行う。ここで確率分岐とは、ある負荷と当該負荷を発生する確率の組の列のことであり、列の中の要素（ある負荷と当該負荷を発生する確率の組の列）がある確率ごとに分岐した負荷であることを意味する。確率分岐上での計算処理は、例えば１／２の確率で５０、および１／２の確率で１００である場合、それぞれの分岐先で５０に対する計算と１００に対する計算が行われる処理である。
【００５５】
確率分岐上で計算が行われる関数の構造に変換する理由は、例えば分岐を持たない値が入力された場合、単一の値から単一の値を求める処理のみが実行されればよい。しかし、分岐を持つ値が入力された場合、上記のように分岐先の各単一の値から単一の値を求める各処理の実行が求められるためである。
【００５６】
次いで、検証部１０２は、変換された負荷関数を入力された要求性能を表す述語に適用することによって、検証対象の命題を生成する（ステップＳ１０５）。具体的には、検証部１０２は、負荷関数ｘを述語Ｐに入力することによって、命題Ｐ（ｘ）を生成する。
【００５７】
次いで、検証部１０２は、ステップＳ１０５で生成された検証対象の命題と、入力された証明とを、定理証明支援器に送る。検証部１０２は、定理証明支援器に証明の正否を検証させる（ステップＳ１０６）。
【００５８】
次いで、検証部１０２は、定理証明支援器からの応答に基づいて、検証結果を示す情報を生成し、生成された情報を外部に出力する（ステップＳ１０７）。出力した後、検証システム１００は、検証処理を終了する。
【００５９】
［効果の説明］
本実施形態の検証システム１００では、確率分布に従う負荷の変動に対応できるように、確率に対する高次化処理が行われた負荷関数である数理的なモデルが扱われる。確率に対する高次化処理が行われると、負荷の確率分布が合成された述語に負荷関数を入力できるため、検証部１０２は、負荷の確率に対するシステムの性能を網羅的に検査できる。
【００６０】
また、本実施形態の検証システム１００のモデル変換部１０１は、入力された取り扱いが容易なアクティビティ図から、検証対象の負荷関数を生成する。また、検証部１０２は、生成された検証対象の負荷関数を用いて、検証対象の命題を生成できる。よって、システム設計者は、定理証明支援器を用いる場合に準備を要する、作成が困難な数理的なモデルを直接作成せずに済む。
【００６１】
（第２実施形態）
［構成の説明］
次に、本発明の第２の実施形態を、図面を参照して説明する。図３は、第２の実施形態の検証システム１００の構成例を示すブロック図である。図３に示すように、本実施形態の検証システム１００は、モデル変換部１０１と、検証部１０２と、イベント記述変換部１０３とを含む。イベント記述変換部１０３以外の図３に示す検証システム１００の構成は、図１に示す検証システム１００の構成と同様である。
【００６２】
イベント記述変換部１０３には、イベント記述が入力される。イベント記述変換部１０３は、入力されたイベント記述を、到着負荷の確率の時系列に変換する機能を有する。
【００６３】
イベント記述変換部１０３で生成された到着負荷の確率の時系列と合成された要求性能を表す述語は、モデル変換部１０１から検証部１０２に入力された負荷関数が満たすことを要求されている性能を表現している。
【００６４】
第１の実施形態では、所定の到着負荷の確率分布が予め合成された要求性能を表す述語を利用者が指定する。本実施形態では、述語と合成される確率分布を利用者が選択できる。よって、本実施形態の検証部１０２は、第１の実施形態と異なり、到着負荷の確率分布と述語との合成処理を実行する。
【００６５】
検証部１０２は、第１の実施形態の機能と同じ機能も有する。すなわち、検証部１０２は、定理証明支援器を利用して、負荷関数が与えられた要求性能を表す述語である命題の証明を検証することによって、システムが所定の性能要件を充足するか否かを判定できる。
【００６６】
［動作の説明］
以下、本実施形態の検証システム１００の証明を検証する動作を図４を参照して説明する。図４は、第２の実施形態の検証システム１００による検証処理の動作を示すフローチャートである。
【００６７】
図４に示すように、ステップＳ２０１〜ステップＳ２０４の処理は、モデル変換部１０１により実行される。ステップＳ２０１〜ステップＳ２０４の処理は、第１の実施形態におけるステップＳ１０１〜ステップＳ１０４の処理と同様である。
【００６８】
また、図４に示すように、ステップＳ２０５〜ステップＳ２０７の処理は、イベント記述変換部１０３により実行される。
【００６９】
最初に、イベント記述変換部１０３は、事前に規定されている確率分布の選択肢をオペレータに提示する（ステップＳ２０５）。
【００７０】
次いで、オペレータは、提示された選択肢の中から確率分布を１つ指定し、確率分布を選択する（ステップＳ２０６）。または、オペレータは、イベント記述に指定された確率分布を追記することによって、確率分布を選択してもよい。
【００７１】
次いで、イベント記述変換部１０３は、ステップＳ２０６で選択された確率分布を用いて、入力されたイベント記述を到着負荷の確率の時系列に変換する（ステップＳ２０７）。
【００７２】
なお、複数の確率分布が指定された場合、イベント記述変換部１０３は、指定された複数の確率分布が合成された確率分布を用いて、入力されたイベント記述を到着負荷の確率の時系列に変換してもよい。
【００７３】
また、図４に示すように、ステップＳ２０８〜ステップＳ２１０の処理は、検証部１０２により実行される。検証部１０２に、ステップＳ２０４で生成された負荷関数が入力される。入力された負荷関数は、負荷の時系列を入力とし、性能の時系列を返す関数である。
【００７４】
次いで、検証部１０２は、ステップＳ２０７で変換された到着負荷の確率の時系列と、入力された要求性能を表す述語とを合成する。次いで、検証部１０２は、入力された負荷関数を合成された要求性能を表す述語に適用することによって、検証対象の命題を生成する（ステップＳ２０８）。
【００７５】
ステップＳ２０９〜ステップＳ２１０の処理は、第１の実施形態におけるステップＳ１０６〜ステップＳ１０７の処理と同様である。
【００７６】
［効果の説明］
本実施形態の検証システム１００が使用された場合、第１の実施形態で得られる効果に加えて、オペレータが用意する要求性能を表す述語がより容易に記述可能になるという効果が得られる。その理由は、代表的な確率分布が事前に規定され、オペレータが規定された確率分布の中から確率分布を１つ選択するだけで、検証部１０２が到着負荷の確率の時系列と要求性能を表す述語とを合成するためである。
【００７７】
すなわち、オペレータは、到着負荷の確率分布が合成されていない要求性能を表す述語を用意できる。また、確率分布が指定可能であるため、本実施形態の検証システム１００が使用されると、利用者にとっての利便性がより向上する。
【００７８】
以下、一実施形態の具体例を、図面を参照して説明する。図５は、検証対象のシステムモデルを示すアクティビティ図である。図５に示すシステムモデルは、コンポーネント１０と、コンポーネント２０とで構成されている。
【００７９】
また、図５に示すプロセス１１およびプロセス１２は、コンポーネント１０におけるプロセスである。また、図５に示すプロセス２１は、コンポーネント２０におけるプロセスである。
【００８０】
また、図５に示すように、第１入力は、プロセス１１に入力される。また、第２入力は、プロセス１２に入力される。第１入力および第２入力は、負荷の時系列を示す入力情報である。
【００８１】
具体例において、プロセス１１、プロセス１２、およびプロセス２１における負荷に対するスループットを返す各関数を、ｔ１〜ｔ３とする。負荷の時系列を示す入力情報が入力されると、関数ｔ１および関数ｔ２は、プロセス１１、プロセス１２における負荷に対するスループットをそれぞれ返す。
【００８２】
具体的には、時点ａの第１入力である「第１入力［ａ］」の負荷が関数ｔ１に与えられると、プロセス１１における時点ａでのスループットは、ｔ１（第１入力［ａ］）で表現される。なお、ｔ１（第１入力［ａ］）は、時点ａでのプロセス２１への到着負荷の一部である。
【００８３】
同様に、時点ａの第２入力である「第２入力［ａ］」の負荷が関数ｔ２に与えられると、プロセス１２における時点ａでのスループットは、ｔ２（第２入力［ａ］）で表現される。なお、ｔ２（第２入力［ａ］）は、時点ａでのプロセス２１への到着負荷の一部である。
【００８４】
負荷の時系列を示す入力情報が入力されると、関数ｔ３は、プロセス１１、プロセス１２、およびプロセス２１全体における負荷に対するスループットを返す。すなわち、プロセス全体における時点ａでのスループットは、ｔ３（ｔ１（第１入力［ａ］），ｔ２（第２入力［ａ］））で表現される。
【００８５】
上記の内容を踏まえると、プロセス全体におけるスループットを返す負荷関数は、ｔ３（ｔ１（＿．１），ｔ２（＿．２））で表現される。なお、記号＿は、プレースホルダである。
【００８６】
例えば、関数ｔ１〜関数ｔ３が、ラムダ記法が使用された以下の式でそれぞれ表現される場合を考える。
【００８７】
ｔ１＝（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００）・・・式（１）
ｔ２＝（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００）・・・式（２）
ｔ３＝（λｘｙ．ｉｆ  ｘ＜ｙ  ｔｈｅｎ  ｘ  ｅｌｓｅ  ｙ）・・・式（３）
【００８８】
なお、式（１）および式（２）における変数はｘである。式（１）および式（２）は、ｔ１およびｔ２が、ｘが１００より小さい場合はｘを返し、ｘが１００以上の場合は１００を返すことを意味する。
【００８９】
また、式（３）における変数はｘとｙである。式（３）は、ｔ３が、ｘがｙより小さい場合はｘを返し、ｘがｙ以上の場合はｙを返すことを意味する。
【００９０】
また具体例の検証システム１００に入力される要求性能を表す述語が、以下の式で表現される場合を考える。
【００９１】
ａ＝［（１／２，５０），（１／２，１５０）］，∀ｘ，ｘ∈ｔ（ａ，ａ）
→ｍｏｒｅＴｈａｎ（１／２，ｘ＞５０）・・・式（４）
【００９２】
なお、式（４）におけるｍｏｒｅＴｈａｎ（１／２，ｘ＞５０）は、「ｘが５０より大きい確率が１／２より大きい」を意味する。以上の条件の下、検証部１０２が生成する証明される対象の命題は、例えば以下の式で表現される。
【００９３】
ａ＝［（１／２，５０），（１／２，１５０）］，∀ｘ１，ｘ１∈（ｌｉｆｔ（λｘ’ｙ’．ｉｆ  ｘ’＜ｙ’  ｔｈｅｎ  ｘ’  ｅｌｓｅ  ｙ’）（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００）（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００））（ａ，ａ）
→ｍｏｒｅＴｈａｎ（１／２，ｘ１＞５０）・・・式（５）
【００９４】
なお、式（５）におけるｌｉｆｔは、確率を持たない負荷の時系列の入力に対して性能の時系列を返す関数を、確率を持つ負荷の時系列の入力に対して確率を持つ性能の時系列を返す関数に持ち上げる関数である。すなわち、ｌｉｆｔは、高次化処理を行う関数の一種である。また、式（５）は、式（４）における関数ｔに、式（１）〜式（３）で表現される各関数が代入された式である。
【００９５】
式（５）で表現される命題に対する証明を、以下に示すように行う。最初に、式（５）で表現される命題に対して、以下の式で表現される簡約を行う。
【００９６】
（λｘ’ｙ’．ｉｆ  ｘ’＜ｙ’  ｔｈｅｎ  ｘ’  ｅｌｓｅ  ｙ’）（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００）（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００））
→（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００）・・・式（６）
【００９７】
式（６）で表現される簡約が行われると、命題は以下の式で表現される。
【００９８】
ａ＝［（１／２，５０），（１／２，１５０）］，∀ｘ１，ｘ１∈（ｌｉｆｔ（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００））（ａ，ａ）
→ｍｏｒｅＴｈａｎ（１／２，ｘ１＞５０）・・・式（７）
【００９９】
次いで、以下のように式（７）における確率の各分岐先でそれぞれ計算を行う。
【０１００】
ａ＝［（１／２，５０），（１／２，１５０）］，∀ｘ１，ｘ１∈（ｌｉｆｔ（λｘ．ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００））（ａ, ａ）
→∀ｘ１，ｘ１∈（ｌｉｆｔ（λｘ.ｉｆ  ｘ＜１００  ｔｈｅｎ  ｘ  ｅｌｓｅ  １００））（［（１／２，５０），（１／２，１５０）］，［（１／２，５０），（１／２，１５０）］）
→［（１／２，５０），（１／２，１００）］・・・式（８）
【０１０１】
最終的に式（８）は、「１／２の確率で５０、１／２の確率で１００」を意味する。従って、要求性能であるｍｏｒｅＴｈａｎ（１／２，ｘ１＞５０）が充足される。以上により、式（５）で表現される命題が成立することが証明された。
【０１０２】
上記の証明が定理証明支援器に与えられると、定理証明支援器は、正しい証明であると判定する。すなわち、図５に示すシステムモデルで表現される具体例の検査対象のシステムは、要求性能を充足する。
【０１０３】
検証システム１００は、シミュレーションによる統計的な性能検査ではなく、網羅的な性能検査を実行できる。その理由は、性能目標に応じて要求される性能が述語で表現されるため、網羅的な性能検査における証明の正否を定理証明支援器で確認できるためである。
【０１０４】
例えば、検証システム１００の検証部１０２は、プログラミング言語における型情報を用いて全ての確率分岐に対して性能値を統合するモデルを構築する。性能値を統合するモデルが構築されると、既存の定理証明支援器は、述語論理における述語で表現された要求性能が充足されているか否かを網羅的に検査できる。
【０１０５】
また、検証システム１００を使用する設計者には、検証対象のモデルである数理的なモデルの記述に要する数理的な知識が求められない。その理由は、検証システム１００のモデル変換部１０１が、設計対象のシステムを表現したアクティビティ図に基づいて、システムを表す数理的なモデルを生成できるためである。
【０１０６】
検証システム１００のモデル変換部１０１は、例えば一般的に設計に用いられるアノテーション言語であるＵＭＬ（Ｕｎｉｆｉｅｄ  Ｍｏｄｅｌｉｎｇ  Ｌａｎｇｕａｇｅ）で記述され、負荷注釈が与えられたアクティビティ図に基づいて、数理的なモデルを生成する。よって、設計者は、数理的なモデルに関する知識を準備しなくても、検査に要するモデルを構築できる。
【０１０７】
なお、検証システム１００は、例えば、記憶媒体に格納されているプログラムに従って処理を実行するＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）によって実現される。すなわちモデル変換部１０１、検証部１０２、およびイベント記述変換部１０３は、例えば、プログラム制御に従って処理を実行するＣＰＵによって実現される。
【０１０８】
また、検証システム１００における各部は、ハードウェア回路によって実現されてもよい。一例として、モデル変換部１０１、検証部１０２、およびイベント記述変換部１０３が、それぞれＬＳＩ（Ｌａｒｇｅ  Ｓｃａｌｅ  Ｉｎｔｅｇｒａｔｉｏｎ）で実現される。また、それらが１つのＬＳＩで実現されていてもよい。
【０１０９】
次に、本発明の概要を説明する。図６は、本発明による検証システムの概要を示すブロック図である。検証システム５０は、述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され検査対象システムが述語で表現されている性能要件を充足することを示す命題を生成する生成部５１（例えば、検証部１０２）と、生成された命題の証明の正否を検証する検証部５２（例えば、検証部１０２）とを備える。
【０１１０】
そのような構成により、検証システムは、到着する負荷の確率に対してシステムの性能が保証されていることを数理的に証明できる。
【０１１１】
また、検証システム５０は、検査対象システムの構成を示すモデルを数理的なモデルに変換するモデル変換部（例えば、モデル変換部１０１）を備えてもよい。
【０１１２】
そのような構成により、検証システムは、設計者にとっての数理的な知識の準備の手間を省くことができる。
【０１１３】
また、生成部５１は、検査対象システムにかかる負荷の確率の時系列が合成された述語に数理的なモデルを入力してもよい。
【０１１４】
そのような構成により、検証システムは、到着する負荷の確率の時系列が合成された述語を用いてシステムの性能が保証されているか否かを数理的に証明できる。
【０１１５】
また、検証システム５０は、負荷イベントを示す情報を検査対象システムにかかる負荷の確率の時系列に変換するイベント変換部（例えば、イベント記述変換部１０３）を備え、生成部５１は、変換された時系列が合成された述語に数理的なモデルを入力してもよい。
【０１１６】
そのような構成により、検証システムは、発生する負荷イベントに対してシステムの性能が保証されているか否かを数理的に証明できる。
【０１１７】
また、検査対象システムにかかる負荷の確率の時系列は、所定の確率分布に基づいて作成された時系列でもよい。
【０１１８】
そのような構成により、検証システムは、到着する負荷の確率に関する確率分布が考慮された述語を用いてシステムの性能が保証されているか否かを数理的に証明できる。
【０１１９】
また、検査対象システムの構成を示すモデルは、アクティビティ図に記載されているモデル、またはマークアップ言語で記述されているモデルでもよい。
【０１２０】
そのような構成により、検証システムは、設計者が容易に記述可能なモデルを処理の対象にできる。
【０１２１】
また、性能要件は、高階述語論理における述語で表現されていてもよい。
【０１２２】
そのような構成により、検証システムは、検査対象システムがより複雑な性能要件を充足することの証明の正否を検証できる。
【０１２３】
また、検証部５２は、定理証明支援器を用いて命題の証明の正否を検証してもよい。
【０１２４】
そのような構成により、検証システムは、既存の定理証明支援器を用いて証明の正否を検証できる。
【０１２５】
また、生成部５１は、数理的なモデルに対して確率に対する高次化処理を行ってもよい。
【０１２６】
そのような構成により、検証システムは、負荷の時系列を入力とする数理的なモデルを処理の対象にできる。
【０１２７】
本発明は、環境の変化に起因する負荷の変動の大きなシステムに対する網羅的な性能検査に好適に適用される。
【０１２８】
なお、図面中の矢印の方向は、一例を示すものであり、ブロック間の信号の向きを限定するものではない。
【０１２９】
以上、上述した実施形態を模範的な例として本発明を説明した。しかしながら、本発明は、上述した実施形態には限定されない。即ち、本発明は、本発明のスコープ内において、当業者が理解し得る様々な態様を適用することができる。
【０１３０】
この出願は、２０１６年４月２８日に出願された日本出願特願２０１６−０９０２３３を基礎とする優先権を主張し、その開示の全てをここに取り込む。
【符号の説明】
【０１３１】
１０、２０  コンポーネント
１１、１２、２１  プロセス
５０、１００  検証システム
５１  生成部
５２、１０２  検証部
１０１  モデル変換部
１０３  イベント記述変換部
【図１】
2017188037.tif 000003
【図２】
2017188037.tif 000004
【図３】
2017188037.tif 000005
【図４】
2017188037.tif 000006
【図５】
2017188037.tif 000007
【図６】
2017188037.tif 000008
【手続補正書】
【提出日】平成30年9月20日(2018.9.20)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】請求項９
【補正方法】変更
【補正の内容】
【請求項９】
コンピュータに、
述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され前記検査対象システムが前記述語で表現されている性能要件を充足することを示す命題を生成し、
生成された前記命題の証明の正否を検証する
ことを実行させる検証プログラム。
【手続補正２】
【補正対象書類名】特許請求の範囲
【補正対象項目名】請求項１０
【補正方法】変更
【補正の内容】
【請求項１０】
コンピュータに、
検査対象システムの構成を示すモデルを数理的なモデルに変換する変換処理を実行させる請求項９記載の検証プログラム。
【手続補正４】
【補正対象書類名】明細書
【補正対象項目名】００２８
【補正方法】変更
【補正の内容】
【００２８】
本発明による検証プログラムの一態様は、コンピュータに、述語論理における述語に検査対象システムの構成を示すモデルが変換された数理的なモデルが入力され検査対象システムが述語で表現されている性能要件を充足することを示す命題を生成する生成処理、および生成された命題の証明の正否を検証する検証処理を実行させる。
【国際調査報告】
2017188037.tif 000009
2017188037.tif 000010