JP7799643B2 - 仕様検証支援装置、方法、およびプログラム - Google Patents

Description

本開示は、情報システムのシステム仕様を検証する技術に関する。

情報システムの開発においては、情報システムを調達する依頼者の要求を開発者が聞き取ってシステム仕様として記述し、依頼者と開発者とでシステム仕様を確認したうえで、システム仕様に従って情報システムを設計し作成する。システム仕様の誤りは情報システムの不具合の原因となるため、システム開発においてシステム仕様の検証は重要である。

システム仕様の記述には状態遷移モデルが用いられる場合がある。状態遷移モデルは、情報システムを構成する各オブジェクトについて、オブジェクトが取り得る状態と、オブジェクトに対して発生するイベントと、イベントによる状態の遷移とを表現するモデルである。状態遷移モデルは状態遷移図や状態遷移表として記述される。

特許文献１には、状態遷移表を編集するための装置が開示されている。特許文献１の状態遷移表編集装置は、システムの検証者が、シーケンス図に基づく観点によって、状態遷移仕様の簡略化を指定することができるようにし、その検証者が、正しく状態遷移仕様の簡略化を行えるようにするものである。状態遷移表編集装置は、シーケンス図を表示し、状態遷移表の縮退の観点とシーケンス図における縮退対象部分とを入力させ、入力された状態遷移表の縮退の観点とシーケンス図における縮退対象部分とに基づいて、状態遷移表の縮退内容を決定し、オリジナル状態遷移表を表すデータから、縮退後の状態遷移表のデータを生成する。

特開２０１０－２５０４２２号公報

特許文献１の開示によれば、検証者が指定した観点によって状態遷移表を簡略化することによりシステムの検証を支援することができる。しかしながら、システム仕様に状態遷移モデルが示されるオブジェクトは個々に独立したものとして管理される。そのため、オブジェクトやその状態の個数が増えると、状態や遷移の抜け漏れ、状態間の矛盾などシステム仕様に内在する誤りが見落とされる場合がある。

本開示に含まれるひとつの目的は、システム仕様の検証において誤りの見落としの低減を可能にする技術を提供することである。

本開示に含まれるひとつの態様による仕様検証支援装置は、情報システムの仕様検証を支援する仕様検証支援装置であって、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付ける仕様登録部と、前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する仕様検証部と、を有する。

本開示に含まれるひとつの態様による仕様検証支援方法は、情報システムの仕様検証を支援する仕様検証支援方法であって、プロセッサとメモリとを備える装置が、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する、ことを実行する。

本開示に含まれるひとつの態様による仕様検証支援プログラムは、情報システムの仕様検証を支援する仕様検証支援プログラムであって、プロセッサとメモリとを備える装置に、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する、ことを実行させる。

本開示のひとつの態様によれば、システム仕様の検証において違反の見落としを低減することが可能となる。

本開示の実施形態の少なくとも一つに対応する、仕様検証支援装置のハードウェア構成例を示す概念図である。 本開示の実施形態の少なくとも一つに対応する、定式化仕様データの内部構造を示す概念図である。 本開示の実施形態の少なくとも一つに対応する、システム仕様確定プロセスを例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、定式化仕様データのフォーマットを例示する概念図である。 本開示の実施形態の少なくとも一つに対応する、システム仕様登録を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、システム仕様登録を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、イベント登録（標準）処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、イベント登録（標準）処理の処理例を示す図である。 本開示の実施形態の少なくとも一つに対応する、イベント登録（例外）処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、イベント登録（例外）処理の処理例を示す図である。 本開示の実施形態の少なくとも一つに対応する、イベント登録（副イベント）処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、イベント登録（副イベント）処理の処理例を示す図である。 本開示の実施形態の少なくとも一つに対応する、イベント登録（手続き結果）処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、イベント登録（手続き結果）処理の処理例を示す図である。 本開示の実施形態の少なくとも一つに対応する、制約条件登録処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、システム検証処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、仕様検証結果データのフォーマットを例示する概念図である。 本開示の実施形態の少なくとも一つに対応する、システム比較検証処理を例示するフローチャートである。 本開示の実施形態の少なくとも一つに対応する、仕様比較結果データのフォーマットを例示する概念図である。

以下、本発明の実施形態について図面を参照して説明する。なお以下に説明する実施例は、特許請求の範囲に係る発明を限定するものではない。また実施例において説明されている諸要素およびその組み合わせの全ては発明の解決手段に必須であるとは限らない。

図１は、本開示の実施形態の少なくとも一つに対応する、仕様検証支援装置のハードウェア構成例を示す概念図である。

仕様検証支援装置１は、図示を省略するプロセッサとメモリとを備える。

プロセッサは、例えばＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）、ＭＰＵ（Ｍｉｃｒｏ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）、ＧＰＵ（Ｇｒａｐｈｉｃｓ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）、ＦＰＧＡ（Ｆｉｅｌｄ－Ｐｒｏｇｒａｍｍａｂｌｅ Ｇａｔｅ Ａｒｒａｙ）等で構成される。

メモリは、プログラムやデータを記憶する装置であり、例えば、Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ（ＲＡＭ）、Ｒｅａｄ Ｏｎｌｙ Ｍｅｍｏｒｙ（ＲＯＭ）、不揮発性半導体メモリ（Ｎｏｎ－Ｖｏｌａｔｉｌｅ ＲＡＭ（ＮＶＲＡＭ））である。

メモリは、例えば、Ｈａｒｄ Ｄｉｓｃ Ｄｒｉｖｅ（ＨＤＤ）、Ｓｏｌｉｄ Ｓｔａｔｅ Ｄｒｉｖｅ（ＳＳＤ）、ストレージシステム、Ｉｎｔｅｇｒａｔｅｄ Ｃｉｒｃｕｉｔ（ＩＣ）カード、Ｓｅｃｕｒｅ Ｄｉｇｉｔａｌ（ＳＤ）メモリカードや光学式記録媒体（Ｃｏｍｐａｃｔ Ｄｉｓｃ（ＣＤ）、Ｄｉｇｉｔａｌ Ｖｅｒｓａｔｉｌｅ Ｄｉｓｃ（ＤＶＤ）など）などの記録媒体の読み取りおよび書き込み装置であってもよい。

プロセッサが、メモリに格納されている仕様検証支援プログラム等の各種プログラムを読み出して実行することにより、データ管理部１０と、仕様登録部２０と、仕様検証部３０と、仕様比較部４０とを実現する。

データ管理部１０は、仕様検証支援装置１が備えるメモリまたは仕様検証支援装置１から見た外部装置が備える記憶装置に保存されたデータである、システム仕様１１０と、仕様検証結果データ１２０と、仕様比較結果データ１３０とを管理する。

システム仕様１１０は、１以上の情報システムに対応する、定式化仕様データを含む。定式化仕様データとは、情報システムの仕様に係るデータが、所定の基準に従って一つのデータ構造として定式化されたものをいう。情報システムの仕様に係るデータとは、例えば自然文形式のデータやＵＭＬ形式のデータ等を意味するが、これらの形式のデータには限られない。図示した例においては、システム仕様１１０は、システム１用の定式化仕様データ１１１と、システム２用の定式化仕様データ１１２とを含む。システム仕様１１０は、他のシステム用の定式化仕様データを同様に含んでいてもよい。

仕様登録部２０は、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様１１１Ａと、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約１１１Ｂとについて登録を受け付ける。

すなわち、状態遷移仕様１１１Ａとイベント制約１１１Ｂは、仕様登録部２０が登録したデータである。

仕様検証部３０は、状態遷移仕様１１１Ａにおいて違反事項に該当するイベントの発生がないかを検証する。

すなわち仕様検証部３０は、状態遷移仕様１１１Ａとイベント制約１１１Ｂのデータを取得し、状態遷移仕様１１１Ａにおいて、イベント制約１１１Ｂによって規定される違反事項に該当するイベントの発生の有無を検証し、結果を仕様検証結果データ１２０として出力する。

仕様比較部４０は、状態遷移仕様１１１Ａと比較するための比較用状態遷移仕様を予め記憶し、状態遷移仕様１１１Ａと比較用状態遷移仕様とを比較して差異を抽出する。

仕様比較部４０は、複数の仕様の間で、状態遷移仕様を比較する。図１においては、システム１定式化仕様データ１１１に含まれる状態遷移仕様１１１Ａと、システム２定式化仕様データ１１２に含まれる状態遷移仕様（比較用状態遷移仕様に相当）とを比較する。ここで、仕様登録部２０が登録したシステム１定式化仕様データ１１１およびシステム２定式化仕様データ１１２は、いずれも所定の基準に従って定式化されている。そのため、前述の比較を機械的に行うことが可能となる。仕様比較部４０は、比較結果、すなわち状態遷移仕様と比較用状態遷移仕様との比較によって抽出された差異に係るデータを、仕様比較結果データ１３０として出力する。

仕様検証支援装置１は、上述の構成要素の他に、入力装置と、出力装置と、通信装置とのうち少なくとも一つ以上を備えてもよい。仕様検証支援装置１が備えるプロセッサ、メモリ、入力装置、出力装置、および通信装置は、バスなどの通信手段を介して互いに通信可能に接続されている。

入力装置はユーザからの入力を受け付ける装置である。入力装置は、例えば、キーボード、マウス、タッチパネル、カードリーダ、音声入力装置等である。

出力装置はユーザに処理経過や処理結果などの各種情報を提供する装置である。出力装置は、例えば、画面表示装置（Ｌｉｑｕｉｄ Ｃｒｙｓｔａｌ Ｄｉｓｐｌａｙ（ＬＣＤ）、Ｈｅａｄ Ｍｏｕｎｔｅｄ Ｄｉｓｐｌａｙ（ＨＭＤ）など）、音声出力装置、印字装置等である。

通信装置は、Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ（ＬＡＮ）やＩｎｔｅｒｎｅｔなどの通信手段を介した他の装置との間の通信を実現する有線または無線方式の通信インターフェースであり、例えば、Ｎｅｔｗｏｒｋ Ｉｎｔｅｒｆａｃｅ Ｃａｒｄ（ＮＩＣ）、無線通信モジュール、Ｕｎｉｖｅｒｓａｌ Ｓｅｒｉａｌ Ｉｎｔｅｒｆａｃｅ（ＵＳＢ）モジュール、シリアル通信モジュールである。

なお、仕様検証支援装置１は通信装置を介して、他の装置との間で情報の入力や出力を行う構成としてもよい。

図２は、本開示の実施形態の少なくとも一つに対応する、定式化仕様データの内部構造を示す概念図である。

図２の定式化仕様データは、例えば図１のシステム１定式化仕様データ１１１などに対応する。１つの情報システムの仕様を、少なくとも、複数のモデルと、モデル間イベントとに基づいて表現したものが、定式化仕様データである。

モデルは、例えば電子商取引システムにおける「受注」などの１つの処理のまとまりに対応する。モデルは、状態遷移仕様データと、イベント制約データとを含む。モデルとモデルとの間が、モデル間イベントによって接続される。

状態遷移仕様データは、複数のモデルのそれぞれにイベントによる状態の遷移を規定するデータである。イベントは、情報システムにおいて発生する何らかのイベントやアクションを意味する。例えば、商品の発送ＯＫを示すメッセージを受信することや、商品の発送指示を示すメッセージを他の処理部、装置またはシステムに送信すること等が、ここでいうイベントに該当する。イベントには、モデルの状態遷移により、他のモデルに発生するイベントが含まれる。

イベント制約データは、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したデータである。

図２に概念的に示したように、情報システムの仕様が、複数のモデルをモデル間イベントで接続するという所定の基準によって定式化されることにより、その仕様における考慮抜けや漏れを発見しやすくなる。また、上述のように定式化された仕様データは、統一された基準によって構造化されているものであるため、複数の情報システムの間で仕様の比較をすることが容易となる。なお、このような定式化仕様データのより具体的なフォーマットの例については、図４に基づいて後述する。

図３は、本開示の実施形態の少なくとも一つに対応する、システム仕様確定プロセスを例示するフローチャートである。以下、仕様検証支援装置１、仕様登録部２０、仕様検証部３０、または仕様比較部４０を処理主体として記載する各処理は、各処理主体が機械的に処理を行うものであってもよく、必要に応じて担当者などのユーザに対しユーザ入力を求めて、ユーザが入力した情報を利用して処理を行うものであってもよい。

担当者（人間）が、情報システムのシステム仕様を自由形式で記述する（Ｓ１１）。自由形式は、例えばＵＭＬ形式や自然文形式などであってよい。

仕様登録部２０はシステム仕様登録を行う（Ｓ１２）。システム仕様は定式化された形式で登録される。ステップＳ１２の詳細な処理については後述する。

仕様検証部３０はシステム仕様検証を行う（Ｓ１３）。ステップＳ１３の詳細な処理については後述する。

仕様比較部４０はシステム仕様比較検証を行う（Ｓ１４）。ステップＳ１４の詳細な処理については後述する。

図４は、本開示の実施形態の少なくとも一つに対応する、定式化仕様データのフォーマットを例示する概念図である。

定式化仕様データは、イベント情報と、モデル情報と、状態遷移情報と、イベント制約情報とを含む。なお、状態遷移情報は図１の状態遷移仕様１１１Ａに、イベント制約情報は図１のイベント制約１１１Ｂに、それぞれ対応する。

イベント情報は項目として、イベント名と、業務手続名と、モデル名と、標準／例外区分と、主／副区分とを有する。

モデル情報は項目として、モデル名を有する。

状態遷移情報は項目として、イベント名と、業務手続名と、モデル名と、状態名と、イベント結果と、遷移先状態名とを有する。

イベント制約情報は報項目として、イベント名と、業務手続名と、制約種別と、制約内容とを有する。

図５は、本開示の実施形態の少なくとも一つに対応する、システム仕様登録を例示するフローチャートである。図６は、本開示の実施形態の少なくとも一つに対応する、システム仕様登録を例示するフローチャートである。図５および図６に記載のシステム仕様登録処理は、図３のステップＳ１２に相当する。

まず、仕様登録部２０が、自由形式の仕様記述から、イベントを取出す（Ｓ２１）。

仕様登録部２０は、当該イベントの対象となるモデルが既にあるか否かを判定する（Ｓ２２）。既にある場合はステップＳ２３に、ない場合はステップＳ２４に、処理がそれぞれ遷移する。

ステップＳ２３において仕様登録部２０は、既に存在するモデルを、当該イベントの対象となるモデルとして決定する。

ステップＳ２４において仕様登録部２０は、当該イベントの対象となるモデルを新規登録する。

ステップＳ２５において仕様登録部２０は、業務手続名を決定する。ステップＳ２６において仕様登録部２０は、イベント名を決定する。

仕様登録部２０は、当該イベントは正常時に必要な処理か否かを判定する（Ｓ２７）。当該イベントが正常時には必ず行う処理である場合は、ステップＳ２８に処理が遷移し、仕様登録部２０が当該イベントの標準／例外区分を「標準」と決定する。当該イベントが、エラー発生時に行う処理であるか、又は、正常時の処理だが必ず行うとは限らない処理である場合は、ステップＳ２９に処理が遷移し、仕様登録部２０が当該イベントの標準／例外区分を「例外」と決定する。

ステップＳ２８またはＳ２９の後、図６に示すステップＳ３１へと処理が遷移する。

ステップＳ３１において仕様登録部２０は、当該イベントは対象となるモデルの一部の属性の状態を変更するイベントであるか否かを判断する。当該イベントがモデルの状態を変更するイベントである場合は、ステップＳ３２に処理が遷移し、仕様登録部２０が当該イベントの主／副区分を「主イベント」と決定する。当該イベントがモデルの一部の属性の状態を変更するイベントである場合は、ステップＳ３３に処理が遷移し、仕様登録部２０が当該イベントの主／副区分を「副イベント」と決定する。

なお、イベントの主／副区分の区分けは必須ではない。ある複数のイベントについて、モデルの一部の属性の状態を変更するにすぎないような場合にまで、それぞれのイベントを別種類のイベントであると解釈した場合、イベントの種類が膨大となり、処理負荷が大きくなる。これを避ける観点から、モデルの一部の属性の状態を変更するにすぎないようなイベントについては、主イベントから派生した副イベントとして管理する。これにより、処理負荷の増大を抑えることができる。

ステップＳ３４において仕様登録部２０は、自由形式の仕様記述に、未処理のイベントがあるか否かを判定する。未処理のイベントが残っている場合、図５のステップＳ２１へと処理が遷移し、仕様登録部２０が未処理の次のイベントを取出して処理を行う。未処理のイベントが残っていない場合、ステップＳ３５へと処理が遷移する。

仕様登録部２０は、イベント登録（標準）処理を行う（Ｓ３５）。仕様登録部２０は、イベント登録（例外）処理を行う（Ｓ３６）。仕様登録部２０は、イベント登録（副イベント）処理を行う（Ｓ３７）。

仕様登録部２０は、イベント登録（手続き結果）処理を行う（Ｓ３８）。仕様登録部２０は、制約条件登録処理を行う（Ｓ３９）。

ステップＳ３５からＳ３９の詳細な処理については、それぞれ後述する。

図７は、本開示の実施形態の少なくとも一つに対応する、イベント登録（標準）処理を例示するフローチャートである。なお、イベント登録（標準）処理は、図６のステップＳ３５に相当する。

仕様登録部２０は、対象モデルにイベント（標準）を登録する（Ｓ４１）。

仕様登録部２０は、未登録のイベントがあるか否かを判定する（Ｓ４２）。未登録のイベントがある場合、ステップＳ４１に戻って仕様登録部２０が次のイベントを登録する。未登録のイベントがない場合、ステップＳ４３に処理が遷移する。

ステップＳ４３において仕様登録部２０は、イベントによるモデルの状態遷移を決定する。すなわち、そのイベントにより、対象とするモデルの状態がどのように遷移するのかを決定する。この決定処理は、仕様登録部２０が担当者に、イベントによるモデルの状態遷移を入力または選択させるような情報をモニタなどの出力装置に出力し、ユーザ入力を受け付ける等の手段によって行われてよい。例えば、担当者は入力装置を用いてイベント間の順序を指定する。仕様登録部２０は、指定された順序に応じて状態遷移を決定する。

仕様登録部２０は、状態遷移が未登録のイベントがあるか否かを判定する（Ｓ４４）。状態遷移が未登録のイベントがある場合、ステップＳ４３に処理が戻る。状態遷移が未登録のイベントがない場合、図７に示した処理は終了となる。

図８は、本開示の実施形態の少なくとも一つに対応する、イベント登録（標準）処理の処理例を示す図である。モデル（注文）に、番号１から番号５までの標準イベントを追加した場合を例示している。

モデル（注文）の状態は、初期状態のＳ０、受注状態のＳ１、在庫確認済状態のＳ２、発送準備済状態のＳ３、発送済状態のＳ４、および完了状態のＳ５の、計６種類の状態があり、何らかのイベントの発生に応じて、状態が遷移する。

モデル（注文）に、図７に示したフローに従ってイベントが５つ登録された。例えば、番号１として、以下のようなイベントが登録された。
イベント：注文発生
業務手続：受注入力
モデル：注文
標準／例外区分：標準

同様に番号２から番号５までのイベントも登録された結果が、図８には示されている。登録されたデータにおける「手続き結果」の欄はこの時点で空欄である。状態遷移（図８のステップＳ４３参照）の欄には、図８に示されているような設定値が設定される。例えば、状態Ｓ０においてイベント「注文発生」が起こった場合、状態はＳ０からＳ１へと遷移する。状態遷移の欄における「Ｅ」は、エラーを意味している。例えば状態Ｓ４（発送済み）において、発送準備イベントが発生するのはおかしい。このような場合、情報システムは何らかのエラー処理を行う必要があるので、状態遷移の欄には設定値として「Ｅ」を設定する。状態遷移の欄における設定値「－」は、そもそも当該状態遷移が起こり得ないことを示している。

図９は、本開示の実施形態の少なくとも一つに対応する、イベント登録（例外）処理を例示するフローチャートである。なお、イベント登録（例外）処理は、図６のステップＳ３６に相当する。

仕様登録部２０は、対象モデルにイベント（例外）を登録する（Ｓ５１）。

仕様登録部２０は、未登録のイベントがあるか否かを判定する（Ｓ５２）。未登録のイベントがある場合、ステップＳ５１に戻って仕様登録部２０が次のイベントを登録する。未登録のイベントがない場合、ステップＳ５３に処理が遷移する。

ステップＳ５３において仕様登録部２０は、イベント（例外）によるモデルの状態遷移を決定する。すなわち、その例外イベントにより、対象とするモデルの状態がどのように遷移するのかを決定する。この決定処理は、仕様登録部２０が担当者に、イベントによるモデルの状態遷移を入力または選択させるような情報をモニタなどの出力装置に出力し、ユーザ入力を受け付ける等の手段によって行われてよい。例えば、担当者は入力装置を用いてイベント間の順序を指定する。仕様登録部２０は、指定された順序に応じて状態遷移を決定する。

仕様登録部２０は、状態遷移が未登録のイベントがあるか否かを判定する（Ｓ５４）。状態遷移が未登録のイベントがある場合、ステップＳ５３に処理が戻る。状態遷移が未登録のイベントがない場合、ステップＳ５５に処理が遷移する。

ステップＳ５５において仕様登録部２０は、イベント（例外）によりモデルに追加される状態があるか否かを判定する。追加される状態がある場合はステップＳ５６に処理が遷移する。追加される状態がない場合、図９に示した処理は終了となる。

ステップＳ５６において仕様登録部２０は、モデルに状態を追加し、イベント（標準）による状態の遷移を決定する。

図１０は、本開示の実施形態の少なくとも一つに対応する、イベント登録（例外）処理の処理例を示す図である。モデル（注文）に、番号６の例外イベントを追加した場合を例示している。

モデル（注文）の状態は、上述したように初期状態のＳ０、受注状態のＳ１、在庫確認済状態のＳ２、発送準備済状態のＳ３、発送済状態のＳ４、および完了状態のＳ５の計６種類の状態があり、何らかのイベントの発生に応じて、状態が遷移する。モデル（注文）には、図７に示したフローに従って標準イベントが既に５つ登録済みである。

モデル（注文）に、図９に示したフローに従って例外イベントが新たに１つ登録された。例えば、番号６として、以下のようなイベントが登録された。

イベント：キャンセル
業務手続：－
モデル：注文
標準／例外区分：例外

番号６の例外イベントが登録された結果が、図１０に示されている。登録されたデータにおける「手続き結果」の欄はこの時点で空欄である。状態遷移の欄における設定値「Ｅ」「－」などの意味は、図８を参照して上述したものと同じであるため、詳しい説明は省略する。

なお、例外イベントによって、モデルの状態遷移に追加が必要な場合は、追加が行われる（図９のステップＳ５６参照）。図示は省略するが、例えば状態Ｓ６が新たに追加される。このとき仕様登録部２０は、状態Ｓ６についての状態遷移も決定する。言い換えると、状態Ｓ６の欄にも設定値を設定する。

図１１は、本開示の実施形態の少なくとも一つに対応する、イベント登録（副イベント）処理を例示するフローチャートである。なお、イベント登録（副イベント）処理は、図６のステップＳ３７に相当する。

仕様登録部２０は、対象モデルと副モデルに副イベントを登録する（Ｓ６１）。なお、副モデルについては図１２を参照して後述する。

仕様登録部２０は、未登録の副イベントがあるか否かを判定する（Ｓ６２）。未登録の副イベントがある場合、ステップＳ６１に戻って仕様登録部２０が次の副イベントを登録する。未登録の副イベントがない場合、ステップＳ６３に処理が遷移する。

ステップＳ６３において仕様登録部２０は、副イベントによる対象モデルの状態遷移を決定する。すなわち、その副イベントにより、対象とするモデルの状態がどのように遷移するのかを決定する。この決定処理は、仕様検証支援装置１が担当者に、副イベントによるモデルの状態遷移を入力または選択させるような情報をモニタなどの出力装置に出力し、ユーザ入力を受け付ける等の手段によって行われてよい。例えば、担当者は入力装置を用いてイベント間の順序を指定する。仕様登録部２０は、指定された順序に応じて状態遷移を決定する。

仕様登録部２０は、対象モデルに遷移先（状態遷移）が未登録の副イベントがあるか否かを判定する（Ｓ６４）。遷移先（状態遷移）が未登録の副イベントがある場合、ステップＳ６３に処理が戻る。遷移先（状態遷移）が未登録の副イベントがない場合、ステップＳ６５に処理が遷移する。

ステップＳ６５において仕様登録部２０は、副イベントによる副モデルの状態遷移を決定する。すなわち、その副イベントにより、対象とする副モデルの状態がどのように遷移するのかを決定する。この決定処理は、仕様登録部２０が担当者に、副イベントによる副モデルの状態遷移を入力または選択させるような情報をモニタなどの出力装置に出力し、ユーザ入力を受け付ける等の手段によって行われてよい。例えば、担当者は入力装置を用いてイベント間の順序を指定する。仕様登録部２０は、指定された順序に応じて状態遷移を決定する。

仕様登録部２０は、副モデルに遷移先（状態遷移）が未登録の副イベントがあるか否かを判定する（Ｓ６６）。遷移先（状態遷移）が未登録の副イベントがある場合、ステップＳ６５に処理が戻る。遷移先（状態遷移）が未登録の副イベントがない場合、図１１に示した処理は終了となる。

図１２は、本開示の実施形態の少なくとも一つに対応する、イベント登録（副イベント）処理の処理例を示す図である。

図１０に示した登録状態から、図１１に示したイベント登録（副イベント）処理を行った結果、対象モデルにイベント「入金」とイベント「返金」とが追加された。番号７がイベント「入金」である。番号８がイベント「返金」である。また、副モデルに、対象モデルに追加されている番号１～番号８と同様のイベントが追加された。

ここで、副モデルについて説明する。副モデルは、対象モデル（主モデル）から派生したモデルを意味する。仕様登録部２０は、モデルごとに状態遷移を登録して管理するため、対象モデルの数が増加するほど、定式化仕様データ（図２参照）は構造が複雑なものとなり、定式化仕様データに基づいた各種の処理についても処理負荷が大きなものとなる。そこで、対象モデルと一部の属性が異なるに過ぎないようなモデルについては、主モデルとしては扱わず、主モデルに従属する派生モデル（副モデル）として扱う。そして、状態遷移仕様は、モデル（主モデル）の特定の状態から派生する副次的な状態をモデルの副モデルの状態として遷移を規定する。これにより、モデルの種類の爆発的な増加が抑えられ、処理負荷を低減させることができる。

図１２に示した例においては、主モデルであるモデル（注文）の状態は、初期状態のＳ０、受注状態のＳ１、在庫確認済状態のＳ２、発送準備済状態のＳ３、発送済状態のＳ４、および完了状態のＳ５の計６種類の状態があり、何らかのイベントの発生に応じて、状態が遷移する。一方、主モデルであるモデル（注文）から派生した副モデル（入金状態）は、初期状態のＳＳ０、入金待ち状態のＳＳ１、入金済み状態のＳＳ２、返金待ち状態のＳＳ３、および返金済み状態のＳＳ４の計５種類の状態があり、何らかのイベントの発生に応じて、状態が遷移する。

モデル（注文）と、モデル（注文）から派生した副モデル（入金処理）に、図１１に示したフローに従って副イベントが登録された。例えば、以下のような副イベント「入金」が登録される。

イベント：入金
業務手続：－
モデル：注文
標準／例外区分：標準
主／副区分：副

なお、副イベント「返金」も、同様に登録される。

これらの副イベントが登録された結果を、図１２は示している。状態遷移の欄における設定値「Ｅ」「－」などの意味は、図８を参照して上述したものと同じであるため、詳しい説明は省略する。状態遷移の欄における設定値「（ＳＳ）」は、主モデルにおいて状態遷移が発生するのではなく、発生したイベントを副モデルの方で管理することを意味している。

図１３は、本開示の実施形態の少なくとも一つに対応する、イベント登録（手続き結果）処理を例示するフローチャートである。なお、イベント登録（手続き結果）処理は、図６のステップＳ３８に相当する。

図６のステップＳ３７の終了時点では、モデル（主モデルおよび副モデル）における手続き結果の欄は空欄であった。イベント登録（手続き結果）処理により、手続き結果の欄に設定値が設定されることになる。

仕様登録部２０は、対象モデルの手続結果を記載（設定）する（Ｓ７１）。

仕様登録部２０は、対象モデルに手続結果が未記載の行があるか否かを判定する（Ｓ７２）。未記載の行がある場合、ステップＳ７１に戻って仕様登録部２０が次の手続結果を記載する。未記載の行がない場合、ステップＳ７３に処理が遷移する。

仕様登録部２０は、イベントを分割し、手続結果と状態遷移を決定する（Ｓ７３）。

仕様登録部２０は、対象モデルに手続結果と状態遷移が未記載の行があるか否かを判定する（Ｓ７４）。未記載の行がある場合、ステップＳ７３に戻る。未記載の行がない場合、ステップＳ７５に処理が遷移する。

仕様登録部２０は、対象モデルに追加する状態があるか否かを判定する（Ｓ７５）。追加する状態がある場合、ステップＳ７６に処理が遷移する。追加する状態がない場合、図１３に示した処理は終了となる。

ステップＳ７６において仕様登録部２０は、対象モデルに状態を追加し、追加された状態について、既存（既登録）のイベントによる状態遷移を決定する（Ｓ７６）。

図１４は、本開示の実施形態の少なくとも一つに対応する、イベント登録（手続き結果）処理の処理例を示す図である。

ステップＳ７１において、モデル「注文」の手続結果欄に記載がなされる。記載とは、設定値を設定することを意味する。ここで、イベント「発送準備」が発生した場合の情報システム側での業務手続は在庫確認である。現実には常に在庫があるとは限らないので、業務手続の手続結果は在庫ありの場合と在庫なしの場合の２つに分割される。また、着荷についても、現実には全ての荷物が届く場合と、一部の荷物だけが届く（他の一部の荷物は別のタイミングで届く）場合とがあるため、手続結果は一部着荷の場合と全部着荷の場合の２つに分割される。このように、イベント発生時の具体的な業務手続を考えるとその手続の結果が２以上の結果に分岐するような場合に、イベントの分割が行われる。図１４に示した一例として、ステップＳ７３の処理によって、番号２のイベント「発送準備」が、番号２、番号２－１、番号２－２、および番号２－３の４つのイベントへと分割された。その上で、手続結果と状態遷移とがそれぞれ決定され、設定値として設定された。

ステップＳ７５において、モデル「注文」には入荷待ちの状態を追加する必要があると判定されたため、ステップＳ７６で、状態Ｓ１１（入荷待ち）が追加されている。追加された状態Ｓ１１（入荷待ち）の既存のイベントによる状態遷移が設定値として設定される。ここでいう既存のイベントは、番号１～番号８の各イベントを指しており、分割後の番号２－１、２－２、２－３のイベントも更に含まれる。

すなわち仕様登録部２０は、モデルへのイベントに対応する業務手続に複数の手続結果が存在する場合に、状態遷移仕様において、モデルへのイベントを手続結果に対応する複数のイベントに分割し、イベントが複数に分割されたことに伴って追加となる状態と、該追加となる状態に関連する状態の遷移とを状態遷移仕様に登録することを受け付ける。

図１５は、本開示の実施形態の少なくとも一つに対応する、制約条件登録処理を例示するフローチャートである。なお、制約条件登録処理は、図６のステップＳ３９に相当する。

仕様登録部２０は、イベント制約（発生順序）を登録する（Ｓ８１）。より具体的には、あるイベントの発生時には既に発生済みである必要がある、前提条件となるイベントが何であるかをシステム仕様１１０に登録する。例えば、入金イベントの前に、注文発生イベントが既に発生済みである必要がある。そのため、注文発生イベントが発生していないにもかかわらず、入金イベントが発生するような場合を仕様の矛盾点として抽出できるように、上記のイベント制約を登録する。

複数のイベントの発生の順序を規定する上記のイベント制約を、第１制約と表記する。後述のステップＳ９２において仕様検証部３０は、状態遷移仕様において第１制約に規定された順序と異なる順序でイベントが発生することがあるか否か確認する。

仕様登録部２０は、イベント制約（発生時期）を登録する（Ｓ８２）。より具体的には、イベントが発生する具体的な時期をシステム仕様１１０に登録する。これにより、登録されている時期とは異なる時期に発生したイベントを、仕様の矛盾点として抽出できるようになる。

イベントの発生する時期を規定する上記のイベント制約を、第２制約と表記する。後述のステップＳ９２において仕様検証部３０は、状態遷移仕様において第２制約に規定された時期と異なる時期にイベントが発生することがあるか否か確認する。

仕様登録部２０は、イベント制約（モデルＣＲＵＤ）を登録する（Ｓ８３）。ＣＲＵＤとは、作成（Ｃｒｅａｔｅ）、参照（Ｒｅｆｅｒ）、更新（Ｕｐｄａｔｅ）、および削除（ＤｅｌｅｔｅのＤ）の頭文字を繋げた造語である。つまり、仕様登録部２０は対象モデルについて、イベントの発生に応じた情報システムの処理において、どのような情報やオブジェクト等が作成、参照、更新または削除されるかをシステム仕様１１０に登録しておく。これにより、複数のイベントを時系列に沿って並べた時に、ＣＲＵＤの観点から明らかに不合理な並びを仕様の矛盾点として抽出できるようになる。例えば、ある情報をまだ作成（Ｃ）していないのに、その情報を参照（Ｒ）、更新（Ｕ）、または削除（Ｄ）するようなイベントの並びは明らかに不合理である。また、ある情報を削除（Ｄ）した後に、その情報を参照（Ｒ）または更新（Ｕ）するようなイベントの並びは明らかに不合理である。このような明らかに不合理なイベントの並びとなっているか否かのチェックを行う際に、登録されたＣＲＵＤの情報が用いられる。

すなわち、モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれる。モデルによる情報の作成、読み出し、更新、削除の順序を規定する上記のイベント制約を、第３制約と表記する。後述のステップＳ９２において仕様検証部３０は、状態遷移仕様において第３制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する。

仕様登録部２０は、イベント制約（副モデルＣＲＵＤ）を登録する（Ｓ８４）。登録される情報の内容は、ステップＳ８３と同様である。ステップＳ８４では、副モデルについて、イベントの発生に応じた情報システムの処理において、どのようなデータが作成、参照、更新または削除されるかをシステム仕様１１０に登録しておく。

すなわち、副モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれる。副モデルによる情報の作成、読み出し、更新、削除の順序を規定するイベント制約を、第４制約と表記する。後述のステップＳ９２において仕様検証部３０は、状態遷移仕様において第４制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する。

図１６は、本開示の実施形態の少なくとも一つに対応する、システム検証処理を例示するフローチャートである。システム検証処理は、図３のステップＳ１３に相当する。

仕様検証部３０は、未設定事項をチェックする（Ｓ９１）。例えば仕様検証部３０は、各イベントに対して、対応する対象モデルまたは副モデルにおいて状態遷移先が設定されていない箇所があった場合に、その箇所を矛盾点として抽出する。

仕様検証部３０は、制約違反をチェックする（Ｓ９２）。より具体的には、仕様検証部３０は、システム仕様１１０に登録された定式化仕様データに基づいて、イベントと状態遷移のすべての組み合わせをチェックする。このすべての組み合わせのチェックにおいて、仕様登録部２０が登録した各種のイベント制約（図１５を参照）に基づく不整合が発見された場合には、その不整合を矛盾点として抽出する。

仕様検証部３０は、矛盾点を出力する（Ｓ９３）。すなわち、ステップＳ９１またはステップＳ９２で抽出された矛盾点を、出力装置を介して出力する。例えば出力装置がモニタである場合は、抽出された矛盾点のリストなどをチェック結果としてモニタに表示させる。

出力された矛盾点を示す情報に基づいて、担当者が矛盾点を修正する。担当者による修正入力に基づいて、仕様登録部２０が図５から図１５を参照して上述したのと同様にして、各種の情報をシステム仕様１１０に登録する（Ｓ９４）。

図１７は、本開示の実施形態の少なくとも一つに対応する、仕様検証結果データのフォーマットを例示する概念図である。

仕様検証結果データ１２０は仕様矛盾情報を含む。仕様矛盾情報は、ステップＳ９３の矛盾点出力処理において用いられる。図１６は、仕様矛盾情報のうち、状態遷移についての矛盾点を表現したフォーマットを示している。

図１７に示したフォーマットの仕様矛盾情報は、項目として、モデル１と、状態名１と、モデル２と、状態名２と、発生イベント名と、遷移不能理由とを有する。すなわち、モデル１のある状態（状態名１）から、モデル２のある状態（状態名２）へと遷移することに失敗した場合の、その遷移の原因となった発生イベント名と、状態遷移ができなかった理由とが、仕様矛盾情報として仕様検証結果データ１２０に記録される。なお、同一のモデル内での状態遷移に係る矛盾点については、モデル１もしくはモデル２の項目を空欄にするか、または、モデル１に設定されたものと同じモデルをモデル２に設定すればよい。

なお、仕様矛盾情報のフォーマットは、図１７に示したものには限定されず、矛盾の内容に応じたフォーマットを当業者が適宜設定してよい。

図１８は、本開示の実施形態の少なくとも一つに対応する、システム仕様比較検証処理を例示するフローチャートである。システム仕様比較検証処理は、図３のステップＳ１４に相当する。

仕様比較部４０は、システム仕様比較処理を行う（Ｓ１０１）。システム仕様比較処理の詳細については後述する。システム仕様比較処理の結果は、仕様比較結果データ１３０として記憶され、データ管理部１０が仕様比較結果データ１３０を管理する。

仕様比較部４０は、システム仕様の相違点を出力する（Ｓ１０２）。すなわち、ステップＳ１０１で抽出されたシステム仕様の相違点を、出力装置を介して出力する。例えば出力装置がモニタである場合は、抽出された相違点のリストなどをチェック結果としてモニタに表示させる。

出力された相違点を示す情報に基づいて、担当者がシステム仕様を修正する。担当者による修正入力に基づいて、仕様登録部２０が図５から図１５を参照して上述したのと同様にして、各種の情報をシステム仕様１１０に登録する（Ｓ１０３）。

次に、システム仕様比較処理の詳細について説明する。システム仕様比較は、図２に示した定式化仕様データに基づいて、複数のシステムの仕様の間で行われる。例えば、図１に示したシステム１定式化仕様データ１１１と、システム２定式化仕様データ１１２とが比較される。なお、３種類以上のシステムの仕様を同時に比較してもよい。以下は、２種類のシステムの仕様を比較する場合を例として説明する。

仕様比較部４０は、モデル構成を比較する（Ｓ１１１）。より具体的には、システム内に存在するモデルの一覧を、複数のシステムの仕様間で比較する。この比較は、状態遷移仕様に存在するモデルの一覧と比較用状態遷移仕様に存在するモデルの一覧とを比較してモデルの過不足を抽出するモデル構成比較に相当する。

仕様比較部４０は、イベント構成を比較する（Ｓ１１２）。より具体的には、各モデルに対するイベントの一覧を、複数のシステムの仕様間で比較する。この比較は、状態遷移仕様に存在する各モデルについてモデルに対応する比較用状態遷移仕様に存在するモデルとイベントの一覧を比較してイベントの過不足を抽出するイベント構成比較に相当する。

仕様比較部４０は、状態構成を比較する（Ｓ１１３）。より具体的には、モデル毎に状態の一覧を、複数のシステムの仕様間で比較する。この比較は、状態遷移仕様に存在する各モデルについて当該モデルに対応する比較用状態遷移仕様に存在するモデルと状態の一覧を比較して状態の過不足を抽出する状態構成比較に相当する。

仕様比較部４０は、遷移先構成を比較する（Ｓ１１４）。より具体的には、モデル毎に同じイベントが発生した場合の遷移先を、複数のシステムの仕様間で比較する。この比較は、状態遷移仕様に存在する各モデルについて、当該モデルに対応する比較用状態遷移仕様に存在するモデルと、互いに対応するイベントに対する遷移先の状態を比較して遷移先の差異を抽出する遷移先比較に相当する。

仕様比較部４０は、制約を比較する（Ｓ１１５）。より具体的には、登録されているイベント制約（違反事項）の一覧を、複数のシステムの仕様間で比較する。

ここで、イベント制約に係るデータも含んだシステムの仕様は、上述の定式化仕様データとして、所定の基準に従ったフォーマットでシステム仕様１１０内に予め記憶されている。そのため仕様比較部４０は、複数のシステムの仕様間での上述のような比較を、機械的に実行することができる。

上述の制約の比較は、比較用状態遷移仕様に対応するイベント制約である比較用イベント制約を予め記憶し、仕様比較部４０が、状態遷移仕様に対応するイベント制約と、比較用イベント制約との違反事項の一覧を比較して違反事項の過不足を抽出する制約比較に相当する。

図１９は、本開示の実施形態の少なくとも一つに対応する、仕様比較結果データのフォーマットを例示する概念図である。

仕様比較結果データ１３０は、仕様矛盾情報と、相違点情報（モデル構成比較）と、相違点情報（イベント構成比較）と、相違点情報（状態構成比較）と、相違点情報（遷移先比較）と、相違点情報（制約比較）とを含む。なお、図１９に示した各情報の区分けおよび情報のフォーマットはあくまで一例であり、取得したい仕様比較結果の内容に応じた区分けおよびフォーマットを、当業者が適宜設定してよい。

仕様矛盾情報は、項目として、システム名１と、システム名２と、相違点情報とを含む。仕様矛盾情報における相違点情報は、相違点情報（モデル構成比較）、相違点情報（イベント構成比較）、相違点情報（状態構成比較）、相違点情報（遷移先比較）、および相違点情報（制約比較）のうち少なくとも一以上に対応する。

相違点情報（モデル構成比較）は、項目として、モデル名と、無い側のシステム名とを含む。例えばシステムＡにはモデル「入金」があるが、システムＢにはモデル「入金」がない場合、相違点情報（モデル構成比較）は、（入金，システムＢ）という情報になる。なお、「無い側のシステム名」という項目の扱いは、後述する他の相違点情報についても同様であるため、重複を避ける観点から以後は詳しい説明を省略する。

相違点情報（イベント構成比較）は、項目として、イベント名と、業務手続名と、モデル名と、無い側のシステム名とを含む。

相違点情報（状態構成比較）は、項目として、モデル名と、状態名と、無い側のシステム名とを含む。

相違点情報（遷移先比較）は、項目として、イベント名と、業務手続名と、モデル名と、状態名と、システム１の遷移先と、システム２の遷移先とを含む。ここでいう遷移先とは、遷移先の状態（状態名）を意味する。

相違点情報（制約比較）は、項目として、イベント名と、業務手続名と、制約種別と、制約内容と、無い側のシステム名とを含む。制約種別とは、例えば図１５における「発生順序」「発生時期」「モデルＣＲＵＤ」「副モデルＣＲＵＤ」などの種別を意味する。

上述した本発明の実施形態は、本発明の説明のための例示であり、本発明の範囲をそれらの実施形態にのみ限定する趣旨ではない。当業者は、本発明の範囲を逸脱することなしに、他の様々な態様で本発明を実施することができる。

以上のように、情報システムの仕様検証を支援する仕様検証支援装置１が、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものでありイベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様１１１Ａと、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約１１１Ｂとについて登録を受け付ける仕様登録部２０を有する。仕様検証支援装置１が、状態遷移仕様１１１Ａにおいて違反事項に該当するイベントの発生がないか検証する仕様検証部３０を有する。これにより、モデルの状態遷移により他のモデルに発生するイベントを含めた状態遷移仕様を登録し、システム仕様の検証において、状態遷移仕様によって違反事項に該当するイベントの発生がないか確認するので、システム仕様の誤りの見落としを低減することができる。

仕様検証支援装置１が、状態遷移仕様１１１Ａと比較するための比較用状態遷移仕様を予め記憶し、状態遷移仕様１１１Ａと比較用状態遷移仕様とを比較して差異を抽出する仕様比較部４０を更に有する。これにより、例えば実績のある同種の情報システムの状態遷移仕様と比較して差異を提示して、システム仕様の誤りの発見を支援することができる。

仕様比較部４０は、状態遷移仕様１１１Ａに存在するモデルの一覧と比較用状態遷移仕様に存在するモデルの一覧とを比較してモデルの過不足を抽出するモデル構成比較と、状態遷移仕様１１１Ａに存在する各モデルについて当該モデルに対応する比較用状態遷移仕様に存在するモデルとイベントの一覧を比較してイベントの過不足を抽出するイベント構成比較と、状態遷移仕様１１１Ａに存在する各モデルについて当該モデルに対応する比較用状態遷移仕様に存在するモデルと状態の一覧を比較して状態の過不足を抽出する状態構成比較と、状態遷移仕様１１１Ａに存在する各モデルについて、当該モデルに対応する比較用状態遷移仕様に存在するモデルと、互いに対応するイベントに対する遷移先の状態を比較して遷移先の差異を抽出する遷移先比較と、の少なくとも１つを実行する。これにより、状態遷移仕様と比較用状態遷移仕様とでモデルを比較して差異を提示して、システム仕様の各モデルに関する誤りの発見を支援することができる。

比較用状態遷移仕様に対応するイベント制約である比較用イベント制約を予め更に記憶する。仕様比較部４０は、状態遷移仕様１１１Ａに対応するイベント制約と、比較用イベント制約との違反事項の一覧を比較して違反事項の過不足を抽出する制約比較を更に実行する。これにより、状態遷移仕様と比較用状態遷移仕様とでイベントの違反事項を提示して、システム仕様のイベント制約に関連する誤りの発見を支援することができる。

イベント制約は、複数のイベントの発生の順序を規定する第１制約を含む。仕様検証部３０は、状態遷移仕様１１１Ａにおいて第１制約に規定された順序と異なる順序でイベントが発生することがあるか否か確認する。これにより、イベントの発生順序に関するシステム仕様の誤りを容易に発見することができる。

イベント制約は、イベントの発生する時期を規定する第２制約を含む。仕様検証部３０は、状態遷移仕様１１１Ａにおいて第２制約に規定された時期と異なる時期にイベントが発生することがあるか否か確認する。これにより、イベントの発生時期に関するシステム仕様の誤りを容易に発見することができる。

モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれる。イベント制約は、モデルによる情報の作成、読み出し、更新、削除の順序を規定する第３制約を含む。仕様検証部３０は、状態遷移仕様において第３制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する。これにより、あるモデルにて作成された情報を他のモデルにより読み出されるといったモデル間にまたがるイベントの順序の整合性を検証することができる。

状態遷移仕様１１１Ａは、モデルの特定の状態から派生する副次的な状態をモデルの副モデルの状態として遷移を規定する。これにより、モデル間のイベントを含めた状態遷移仕様において、モデルの状態とイベントとの組み合わせ数が爆発的に増大することを防止できる。

副モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれる。イベント制約は、副モデルによる情報の作成、読み出し、更新、削除の順序を規定する第４制約を含む。仕様検証部３０は、状態遷移仕様において第４制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する。これにより、副モデルを含めてイベントの順序の整合性を検証することができる。

仕様登録部２０は、モデルへのイベントに対応する業務手続に複数の手続結果が存在する場合に、状態遷移仕様１１１Ａにおいて、モデルへのイベントを手続結果に対応する複数のイベントに分割し、イベントが複数に分割されたことに伴って追加となる状態と、該追加となる状態に関連する状態の遷移とを状態遷移仕様１１１Ａに登録することを受け付ける。これにより、モデルの状態遷移により他のモデルに発生するイベントを含めたシステム仕様の検証を実行可能な状態遷移仕様の登録を支援することができる。

情報システムの仕様検証を支援する仕様検証支援方法において、プロセッサとメモリとを備える装置１が、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものでありイベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様１１１Ａと、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約１１１Ｂとについて登録を受け付け、状態遷移仕様１１１Ａにおいて違反事項に該当するイベントの発生がないか検証する、ことを実行する。これにより、モデルの状態遷移により他のモデルに発生するイベントを含めた状態遷移仕様を登録し、システム仕様の検証において、状態遷移仕様によって違反事項に該当するイベントの発生がないか確認するので、システム仕様の誤りの見落としを低減することができる。

情報システムの仕様検証を支援する仕様検証支援プログラムが、プロセッサとメモリとを備える装置１に、複数のモデルのそれぞれにイベントによる状態の遷移を規定するものでありイベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様１１１Ａと、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約１１１Ｂとについて登録を受け付け、状態遷移仕様において違反事項に該当するイベントの発生がないか検証する、ことを実行させる。これにより、モデルの状態遷移により他のモデルに発生するイベントを含めた状態遷移仕様を登録し、システム仕様の検証において、状態遷移仕様によって違反事項に該当するイベントの発生がないか確認するので、システム仕様の誤りの見落としを低減することができる。

１…仕様検証支援装置、１０…データ管理部、２０…仕様登録部、３０…仕様検証部、４０…仕様比較部

Claims (11)

1. 情報システムの仕様検証を支援する仕様検証支援装置であって、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付ける仕様登録部と、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する仕様検証部と、
   前記状態遷移仕様と比較するための比較用状態遷移仕様を予め記憶し、前記状態遷移仕様と前記比較用状態遷移仕様とを比較して差異を抽出する仕様比較部と、
   を有する仕様検証支援装置。
2. 前記仕様比較部は、
   前記状態遷移仕様に存在するモデルの一覧と前記比較用状態遷移仕様に存在するモデルの一覧とを比較してモデルの過不足を抽出するモデル構成比較と、
   前記状態遷移仕様に存在する各モデルについて当該モデルに対応する前記比較用状態遷移仕様に存在するモデルとイベントの一覧を比較してイベントの過不足を抽出するイベント構成比較と、
   前記状態遷移仕様に存在する各モデルについて当該モデルに対応する前記比較用状態遷移仕様に存在するモデルと状態の一覧を比較して状態の過不足を抽出する状態構成比較と、
   前記状態遷移仕様に存在する各モデルについて、当該モデルに対応する前記比較用状態遷移仕様に存在するモデルと、互いに対応するイベントに対する遷移先の状態を比較して遷移先の差異を抽出する遷移先比較と、
   の少なくとも１つを実行する、
   請求項１に記載の仕様検証支援装置。
3. 前記比較用状態遷移仕様に対応するイベント制約である比較用イベント制約を予め更に記憶し、
   前記仕様比較部は、前記状態遷移仕様に対応するイベント制約と、前記比較用イベント制約との違反事項の一覧を比較して違反事項の過不足を抽出する制約比較を更に実行する、
   請求項１に記載の仕様検証支援装置。
4. 情報システムの仕様検証を支援する仕様検証支援装置であって、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付ける仕様登録部と、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する仕様検証部と、
   を有し、
   前記モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれ、
   前記イベント制約は、モデルによる情報の作成、読み出し、更新、削除の順序を規定する第３制約を含み、
   前記仕様検証部は、前記状態遷移仕様において前記第３制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する、
   仕様検証支援装置。
5. 情報システムの仕様検証を支援する仕様検証支援装置であって、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付ける仕様登録部と、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する仕様検証部と、
   を有し、
   前記仕様登録部は、モデルへのイベントに対応する業務手続に複数の手続結果が存在する場合に、前記状態遷移仕様において、前記モデルへの前記イベントを前記手続結果に対応する複数のイベントに分割し、前記イベントが複数に分割されたことに伴って追加となる状態と、該追加となる状態に関連する状態の遷移とを前記状態遷移仕様に登録することを受け付ける、
   仕様検証支援装置。
6. 情報システムの仕様検証を支援する仕様検証支援方法であって、
   プロセッサとメモリとを備える装置が、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証し、
   前記状態遷移仕様と比較するための比較用状態遷移仕様を予め記憶し、前記状態遷移仕様と前記比較用状態遷移仕様とを比較して差異を抽出する、
   ことを実行する、仕様検証支援方法。
7. 情報システムの仕様検証を支援する仕様検証支援方法であって、
   プロセッサとメモリとを備える装置が、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する、
   ことを実行する方法であり、
   前記モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれ、
   前記イベント制約は、モデルによる情報の作成、読み出し、更新、削除の順序を規定する第３制約を含み、
   前記状態遷移仕様において前記第３制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する、
   仕様検証支援方法。
8. 情報システムの仕様検証を支援する仕様検証支援方法であって、
   プロセッサとメモリとを備える装置が、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する、
   ことを実行する方法であり、
   モデルへのイベントに対応する業務手続に複数の手続結果が存在する場合に、前記状態遷移仕様において、前記モデルへの前記イベントを前記手続結果に対応する複数のイベントに分割し、前記イベントが複数に分割されたことに伴って追加となる状態と、該追加となる状態に関連する状態の遷移とを前記状態遷移仕様に登録することを受け付ける、
   仕様検証支援方法。
9. 情報システムの仕様検証を支援する仕様検証支援プログラムであって、
   プロセッサとメモリとを備える装置に、
   複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、
   前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証し、
   前記状態遷移仕様と比較するための比較用状態遷移仕様を予め記憶し、前記状態遷移仕様と前記比較用状態遷移仕様とを比較して差異を抽出する、
   ことを実行させるための、仕様検証支援プログラム。
10. 情報システムの仕様検証を支援する仕様検証支援プログラムであって、
    プロセッサとメモリとを備える装置に、
    複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、
    前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する、
    ことを実行させるためのプログラムであり、
    前記モデルには、イベントの発生に応じて、情報の生成、参照、更新、または削除を行うモデルが含まれ、
    前記イベント制約は、モデルによる情報の作成、読み出し、更新、削除の順序を規定する第３制約を含み、
    前記状態遷移仕様において前記第３制約に規定された順序と異なる順序で情報の作成、読み出し、更新、または削除が行われることがあるか否か確認する、ことを実行させる、
    仕様検証支援プログラム。
11. 情報システムの仕様検証を支援する仕様検証支援プログラムであって、
    プロセッサとメモリとを備える装置に、
    複数のモデルのそれぞれにイベントによる状態の遷移を規定するものであり前記イベントにはモデルの状態遷移により他のモデルに発生するイベントが含まれる状態遷移仕様と、イベントについて当該イベントが発生した場合に違反とすべき違反事項を規定したイベント制約とについて登録を受け付け、
    前記状態遷移仕様において前記違反事項に該当するイベントの発生がないか検証する、
    ことを実行させるためのプログラムであり、
    モデルへのイベントに対応する業務手続に複数の手続結果が存在する場合に、前記状態遷移仕様において、前記モデルへの前記イベントを前記手続結果に対応する複数のイベントに分割し、前記イベントが複数に分割されたことに伴って追加となる状態と、該追加となる状態に関連する状態の遷移とを前記状態遷移仕様に登録することを受け付ける、ことを実行させる、
    仕様検証支援プログラム。