(57)【要約】【課題】設計対象の分野特有の要求仕様に応じた設計モデルを容易に生成する。【解決手段】監視対象の状態遷移を表現した原始モデルを入力する原始モデル入力手段１１１と、原始モデルの変換規則を要求仕様と対応付けて格納するモデル変換規則格納手段１１３と、要求仕様を入力する要求仕様入力手段１１２と、入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する設計モデル生成手段１１４を備える。【選択図】図１
2007241435.tif 000002
【特許請求の範囲】
【請求項１】
監視対象の状態遷移を表現した原始モデルを入力する原始モデル入力手段と、
原始モデルの変換規則を要求仕様と対応付けて格納するモデル変換規則格納手段と、
要求仕様を入力する要求仕様入力手段と、
該要求仕様入力手段により入力された要求仕様に対応する原始モデルの変換規則を上記モデル変換規則格納手段より取得し、上記原始モデル入力手段により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する設計モデル生成手段を備えたモデル生成装置。
【請求項２】
モデル変換規則格納手段は可変情報を含む要求仕様を格納し、
上記モデル変換規則格納手段に格納されている要求仕様に含まれる可変情報を入力する可変情報入力手段を備え、
設計モデル生成手段は、要求仕様入力手段により入力された要求仕様と上記可変情報入力手段により入力された可変情報に対応する原始モデルの変換規則を上記モデル変換規則格納手段より取得し、原始モデル入力手段により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することを特徴とする請求項１記載のモデル生成装置。
【請求項３】
モデル変換規則格納手段は検証目的の可変情報を含む要求仕様を格納することを特徴とする請求項２記載のモデル生成装置。
【請求項４】
モデル変換規則格納手段は可変情報を含む原始モデルの変換規則を格納し、
上記モデル変換規則格納手段に格納されている原始モデルの変換規則に含まれる可変情報に設定するための所定値を入力する可変情報入力手段を備え、
設計モデル生成手段は、要求仕様入力手段により入力された要求仕様に対応する原始モデルの変換規則を上記モデル変換規則格納手段より取得し、取得した原始モデルの変換規則に含まれる可変情報に上記可変情報入力手段により入力された所定値を設定し、原始モデル入力手段により入力された原始モデルを、取得した原始モデルの所定値が設定された可変情報を含む変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することを特徴とする請求項１記載のモデル生成装置。
【請求項５】
モデル変換規則格納手段は検証目的の可変情報を含む原始モデルの変換規則を格納することを特徴とする請求項４記載のモデル生成装置。
【請求項６】
モデル変換規則格納手段は原始モデルの変換規則を原始モデルに付加されている付加情報に対応付けて格納し、
設計モデル生成手段は、原始モデル入力手段により入力された監視対象の原始モデルに付加されている所定の付加情報を検出した場合に、上記モデル変換規則格納手段から所定の付加情報及び要求仕様に対応する原始モデルの変換規則を取得し、原始モデル入力手段により入力された原始モデルを、取得した所定の付加情報及び要求仕様に対応する原始モデルの変換規則に基づき変換して、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することを特徴とする請求項１記載のモデル生成装置。
【請求項７】
モデル変換規則格納手段に格納される要求仕様と原始モデルの変換規則を入力するモデル変換規則入力手段を備えたことを特徴とする請求項１記載のモデル生成装置。
【請求項８】
コンピュータを
監視対象の状態遷移を表現した原始モデルを入力する原始モデル入力手段、
原始モデルの変換規則を要求仕様と対応付けて格納するモデル変換規則格納手段、
要求仕様を入力する要求仕様入力手段、
該要求仕様入力手段により入力された要求仕様に対応する原始モデルの変換規則を上記モデル変換規則格納手段より取得し、上記原始モデル入力手段により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する設計モデル生成手段として機能させるためのモデル生成用プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成するモデル生成装置及びモデル生成用プログラムに関するものである。
【背景技術】
【０００２】
従来のモデル生成装置では、性能評価モデル作成にかかる時間及びコストを削減するために、例えば特許文献１に示すように、ＵＭＬ（Unified Modeling Language）モデルを解析した結果に応じて変換規則を適用することで性能評価モデルを自動的に生成できるようにしている。
【０００３】
【特許文献１】特開２００１−３１８８１２号公報（段落０００８）
【発明の開示】
【発明が解決しようとする課題】
【０００４】
従来のモデル生成装置は以上のように構成され、ＵＭＬモデル解析部の解析結果に応じて変換規則を選択するため、その結果、入力したＵＭＬモデルに対して単一の性能評価モデルしか生成できず、設計対象の分野特有の要求仕様に応じた設計モデルを容易に生成することができないという課題があった。
【０００５】
この発明は、上記のような課題を解決するためになされたもので、設計対象の分野特有の要求仕様に応じた設計モデルを容易に生成することができるモデル生成装置及びモデル生成用プログラムを得ることを目的とする。
【課題を解決するための手段】
【０００６】
この発明に係るモデル生成装置は、監視対象の状態遷移を表現した原始モデルを入力する原始モデル入力手段と、原始モデルの変換規則を要求仕様と対応付けて格納するモデル変換規則格納手段と、要求仕様を入力する要求仕様入力手段と、該要求仕様入力手段により入力された要求仕様に対応する原始モデルの変換規則を上記モデル変換規則格納手段より取得し、上記原始モデル入力手段により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する設計モデル生成手段を備えたものである。
【発明の効果】
【０００７】
この発明により、設計対象の分野特有の要求仕様に応じた設計モデルを容易に生成することができるという効果が得られる。
【発明を実施するための最良の形態】
【０００８】
実施の形態１．
図１はこの実施の形態１におけるモデル生成装置の構成を示すブロック図である。このモデル生成装置は、原始モデル入力手段１１１、要求仕様入力手段１１２、モデル変換規則格納手段１１３及び設計モデル生成手段１１４を備えている。
【０００９】
図１において、原始モデル入力手段１１１は設計者から監視対象の状態遷移を表現した原始モデルを入力する。この原始モデルはモデル生成装置によって生成される設計モデルの元となるものである。モデル変換規則格納手段１１３は原始モデルの変換規則を要求仕様と対応付けて格納すると共に後述の伝送路モデルを格納する。
【００１０】
要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００１１】
図２は図１に示すモデル生成装置を実現するコンピュータの構成を示すブロック図である。コンピュータ１は、ディスプレイ２、キーボード３、ポインティングデバイス４、ＣＰＵ５、メモリ６及びハードディスク７を備えている。なお、表示（出力）装置はディスプレイ２に、入力装置はキーボード３やポインティングデバイス４に、記憶装置はメモリ６やハードディスク７に限定されるものではない。
【００１２】
この実施の形態１においては、列車におけるブレーキ監視装置に搭載するソフトウェアの設計を行う場合の処理の流れを説明する。一般に、列車には電気ブレーキが採用されていることが多い。電気ブレーキは電気回路の故障によりブレーキ力を失うことがある。ブレーキ監視装置は電気回路の故障によるブレーキの故障及び故障からの復帰を監視することを目的とした装置である。
【００１３】
図３は要求仕様入力手段１１２により要求仕様として入力される監視システムの構成を示す図である。この監視システムの構成は監視装置１２１と監視対象（原始モデル）１２３が伝送路１２２によって一対一で接続されている。
【００１４】
図４は図３に示す監視システムにおける伝送路１２２の伝送路モデルを示す図であり、伝送路１２２が取り得る状態と状態間の遷移を示している。この伝送路モデルは、伝送路１２２が正常な正常状態（ＯＫ状態）及び伝送路１２２が故障した異常状態（ＮＧ状態）の２状態を有し、伝送路１２２が故障すると正常状態から異常状態に遷移し、伝送路１２２が復帰すると異常状態から正常状態に遷移する。
【００１５】
図５は原始モデル入力手段１１１により入力される監視対象の原始モデルとしてのブレーキモデルを示す図であり、監視対象のブレーキが取り得る状態と状態間の遷移を示している。このブレーキモデルは、ブレーキが正常な正常状態（ＯＫ状態）及びブレーキが故障した異常状態（ＮＧ状態）の２状態を有し、ブレーキが故障すると正常状態から異常状態に遷移し、ブレーキが復帰すると異常状態から正常状態に遷移する。
【００１６】
図６はモデル変換規則格納手段１１３に格納され対応付けられている要求仕様と原始モデルの変換規則の例を示す図であり、要求仕様が図３に示す監視システムの場合の原始モデルの変換規則を示している。
【００１７】
図６において、要求仕様が図３に示す監視システムの場合の原始モデルの変換規則は以下のようになっている。
変換規則１：監視対象の原始モデルと伝送路モデルを合成する
変換規則２：伝送路モデルは監視対象の原始モデルに対して監視性依存関係を持つ
変換規則３：監視性依存関係を持つ依存先モデルの異常状態を併合する
【００１８】
ここで、モデルＡがモデルＢに対して監視性依存関係を持つとは、モデルＡが異常状態の場合、監視装置１２１はモデルＢの状態を監視できないという依存関係があることを表す。このとき、モデルＡをモデルＢの監視性依存先モデル又は単に依存先モデルと呼ぶ。
例えば、図３に示す監視システムの場合、伝送路１２２が異常状態の場合には、監視装置１２１は監視対象１２３からの伝送データを受信できず、監視装置１２１は監視対象１２３を監視できない。このため、図６の変換規則２に挙げたように、伝送路モデルは監視対象の原始モデルに対して監視性依存関係を持ち、伝送路モデルが依存先モデルとなる。
【００１９】
図７はこの実施の形態１におけるモデル生成装置の概略処理を示すフローチャートである。
ステップＳＴ１において、要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。ここでは、要求仕様として図３に示す監視システムを入力する。
【００２０】
ステップＳＴ２において、原始モデル入力手段１１１は設計者から監視対象１２３であるブレーキが取り得る状態と状態間の遷移を示すブレーキモデル（図５）を監視対象の原始モデルとして入力し設計モデル生成手段１１４に出力する。
【００２１】
ステップＳＴ３において、設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様（監視システム）に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された監視対象の原始モデル（ブレーキモデル）を、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００２２】
図８は設計モデル生成手段１１４により設計モデルとして生成された監視装置モデルを示す図であり、伝送路及びブレーキが取り得る状態と状態間の遷移を示している。すなわち、この監視装置モデルはブレーキ及び伝送路が正常状態、ブレーキが異常状態で伝送路が正常状態並びに伝送路が異常状態の３状態と、状態間の遷移を示している。
図８に示す監視装置モデルの詳細な生成方法については後述する。
【００２３】
図９はこの実施の形態１におけるモデル生成装置の詳細処理を示すフローチャートである。ここでは、図２に示すコンピュータの構成と関連させて説明する。
ステップＳＴ１１において、要求仕様入力手段１１２はハードディスク７上のモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得してディスプレイ２に出力する。ステップＳＴ１２において、要求仕様入力手段１１２はディスプレイ２に表示された要求仕様の一覧から設計者によりキーボード３又はポインティングデバイス４を用いて選択された要求仕様を入力してメモリ６に保持する。
【００２４】
ステップＳＴ１３において、設計モデル生成手段１１４はメモリ６に保持されている要求仕様に対応した原始モデルの変換規則をハードディスク７上のモデル変換規則格納手段１１３から取得してメモリ６に保持する。ステップＳＴ１４において、原始モデル入力手段１１１は設計者よりキーボード３又はポインティングデバイス４を用いて指示された監視対象の原始モデルを入力してメモリ６に保持する。
【００２５】
ステップＳＴ１５において、設計モデル生成手段１１４は変換規則により監視対象の原始モデルの変換が終了したか否かを判定し、変換が終了していない場合には、ステップＳＴ１６において、設計モデル生成手段１１４はメモリ６に保持されている原始モデルの変換規則に基づき、メモリ６に保持されている監視対象の原始モデルを変換する。変換した監視対象の原始モデルは一時的にメモリ６に保持される。設計モデル生成手段１１４は、メモリ６に保持されている全ての変換規則による監視対象の原始モデルの変換が終了するまで、ステップＳＴ１５，ＳＴ１６の処理を繰り返す。
【００２６】
ステップＳＴ１７において、設計モデル生成手段１１４は、全ての変換規則により変換が完了した時点でメモリ６に保持されている変換された監視対象の原始モデルを設計モデルとしてメモリ６に保持し、生成した設計モデルをディスプレイ２に出力する。
以上の全ての処理はＣＰＵ５の命令に従って実行される。
【００２７】
図９に示す処理では、要求仕様を入力後に原始モデルを入力しているが、その順番は限定されるものではなく、原始モデルを入力後に要求仕様を入力しても良い。
【００２８】
次に図８に示す設計モデルとしての監視装置モデルの生成方法について説明する。
まず、設計モデル生成手段１１４は、図６に示す変換規則１により、原始モデル入力手段１１１により入力された図５に示す監視対象の原始モデル（ブレーキモデル）と図４に示す伝送路モデルを合成し、４状態のモデルを生成する。ここでの合成は、文献“Systems and Software Verification:Model-Checking Techniques and Tools”(2001 Berard)の14ページ“1.5 Synchronized Product”に記述されている手法を用いて複数のモデルを一つのモデルにまとめることを意味する。
【００２９】
図１０は図６に示す変換規則１により変換された４状態のモデルを示す図である。ここでは、ブレーキ及び伝送路が正常状態、ブレーキが正常状態で伝送路が異常状態、ブレーキが異常状態で伝送路が正常状態並びにブレーキ及び伝送路が異常状態の４状態と、状態間の遷移を示している。
【００３０】
次に、設計モデル生成手段１１４は、図６に示す変換規則２及び変換規則３により、依存先モデルである伝送路が異常状態、すなわち、「ブレーキが正常状態で伝送路が異常状態」と「ブレーキ及び伝送路が異常状態」とを併合する
【００３１】
ここで、一般的に状態Ａと状態Ｂの併合とは以下の処理を示している。
１．状態Ａ及び状態Ｂ間の遷移を削除し、状態Ａ及び状態Ｂを１つの状態Ｃとする。
２．遷移先が状態Ａ又は状態Ｂである全ての遷移を遷移元の状態毎にグループ分けする。
３．各グループについて、そのグループの遷移元の状態をＰとし以下の処理を実施する。
３−１．状態Ｐから状態Ｃへの遷移を追加する。
３−２．状態Ｐから状態Ａ及び状態Ｐから状態Ｂへのそれぞれの遷移条件の論理和を状態Ｐから状態Ｃへの遷移条件とする。
３−３．状態Ｐから状態Ａ、状態Ｐから状態Ｂへの遷移を削除する。
４．状態Ａからの遷移（遷移先をＱとする）全てについて以下の処理を実施する。
４−１．状態Ｃから状態Ｑへの遷移を追加する。
４−２．状態Ａから状態Ｑへの遷移条件のガード条件に「状態Ａであること」を追加した遷移条件を、状態Ｃから状態Ｑへの遷移条件とする。
４−３．状態Ａから状態Ｑへの遷移を削除する。
５．状態Ｂからの遷移（遷移先をＲとする）全てについて以下の処理を実施する。
５−１．状態Ｃから状態Ｒへの遷移を追加する。
５−２．状態Ｂから状態Ｒへの遷移条件のガード条件に「状態Ｂであること」を追加した遷移条件を、状態Ｃから状態Ｒへの遷移条件とする。
５−３．状態Ｂから状態Ｒへの遷移を削除する。
６．上記４、５の結果、状態Ｃから同じ状態Ｓへの遷移が複数ある場合、これらの状態を状態Ｃから状態Ｓへの１つの遷移にまとめ、遷移条件を、まとめる前の遷移条件の論理和とする。
【００３２】
併合には結合法則が成立するため、３状態以上の併合は、任意の２状態に対して上記を繰り返し適用することにより実現できる。
以上により、図８に示す設計モデルが生成される。
【００３３】
図１１は監視対象の原始モデルとしての他のブレーキモデルを示す図であり、監視対象のブレーキが取り得る３状態と状態間の遷移を示している。すなわち、このブレーキモデルは、ブレーキが正常な正常状態（ＯＫ状態）、ブレーキの故障の可能性を警告する警告状態（ＷＡＲＮＩＮＧ状態）及びブレーキが故障した異常状態（ＮＧ状態）の３状態と、状態間の遷移を示している。
【００３４】
図１２は図１１に示すブレーキモデルの場合に設計モデル生成手段１１４により設計モデルとして生成された監視装置モデルを示す図であり、伝送路及びブレーキが取り得る状態と状態間の遷移を示している。すなわち、この監視装置モデルはブレーキ及び伝送路が正常状態、ブレーキが警告状態で伝送路が正常状態、ブレーキが異常状態で伝送路が正常状態並びに伝送路が異常状態の４状態と、状態間の遷移を示している。
【００３５】
生成されたこの設計モデルを用いて設計検証を行うことが可能である。また、開発の次段階に対する成果物として活用することも可能である。
【００３６】
以上のように、この実施の形態１によれば、モデル変換規則格納手段１１３が原始モデルの変換規則を要求仕様と対応付けて格納し、設計モデル生成手段１１４が、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することにより、設計対象の分野特有の要求仕様に応じた設計モデルを容易に生成することができるという効果が得られる。
【００３７】
実施の形態２．
図１３はこの実施の形態２におけるモデル生成装置の構成を示すブロック図である。このモデル生成装置は、原始モデル入力手段１１１、要求仕様入力手段１１２、モデル変換規則格納手段１１３、可変情報入力手段１１５及び設計モデル生成手段１１４を備えている。
【００３８】
図１３において、モデル変換規則格納手段１１３は原始モデルの変換規則を可変情報を含む要求仕様と対応付けて格納する。可変情報入力手段１１５はモデル変換規則格納手段１１３に格納されている要求仕様に含まれる可変情報を入力する。設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様と可変情報入力手段１１５により入力された可変情報に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。その他の原始モデル入力手段１１１及び要求仕様入力手段１１２の処理は上記実施の形態１の処理と同じである。
【００３９】
この実施の形態２においても、列車におけるブレーキ監視装置に搭載するソフトウェアの設計を行う場合の処理の流れを説明する。
図１４は伝送データが正常か異常かを示すデータ整合性モデルを示す図であり、データ整合性が取り得る状態と状態間の遷移を示している。このデータ整合性モデルは、データが正常な正常状態（ＯＫ状態）及びデータが異常な異常状態（ＮＧ状態）の２状態を有し、データが異常データであれば正常状態から異常状態に遷移し、データが正常データであれば異常状態から正常状態に遷移する。
【００４０】
図１５はモデル変換規則格納手段１１３に格納され対応付けられている可変情報を含む要求仕様と原始モデルの変換規則の例を示す図であり、要求仕様が図３に示す監視システムの場合で、要求仕様に含まれる可変情報として伝送データの整合性確認を行う場合と整合性確認を行わない場合が設定され、整合性確認を行う場合と整合性確認を行わない場合の原始モデルの変換規則を示している。
【００４１】
図１５において、要求仕様が図３に示す監視システムの場合の原始モデルの変換規則は以下のようになっている。
伝送データの整合性確認を行う場合
変換規則１：監視対象の原始モデルと伝送路モデルを合成する
変換規則２：監視対象の原始モデルとデータ整合性モデルを合成する
変換規則３：伝送路モデルはデータ整合性モデルに対して監視性依存関係を持つ
変換規則４：データ整合性モデルは監視対象の原始モデルに対して監視性依存関係を持つ
変換規則５：監視性依存関係を持つ依存先モデルの異常状態を併合する
伝送データの整合性確認を行わない場合
変換規則１：監視対象の原始モデルと伝送路モデルを合成する
変換規則２：伝送路モデルは監視対象の原始モデルに対して監視性依存関係を持つ
変換規則３：監視性依存関係を持つ依存先モデルの異常状態を併合する
【００４２】
図１６はこの実施の形態２におけるモデル生成装置の概略処理を示すフローチャートである。
ステップＳＴ２１において、要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。ここでは、要求仕様として、上記実施の形態１の図３に示す監視システムを入力する。
【００４３】
ステップＳＴ２２において、可変情報入力手段１１５は設計者からこの監視システムの要求仕様に含まれる可変情報を入力する。この監視システムは可変情報として伝送データの整合性確認を行うか否かを指定することができ、ここでは、可変情報として「整合性確認を行う」を入力する。
【００４４】
ステップＳＴ２３において、原始モデル入力手段１１１は設計者から監視対象１２３であるブレーキが取り得る状態と状態間の遷移を示すブレーキモデルを監視対象の原始モデルとして入力し設計モデル生成部１１４に出力する。このブレーキモデルは上記実施の形態１の図５に示すものと同じである。
【００４５】
ステップＳＴ２４において、設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様（監視システム）及び可変情報入力手段１１５により入力された可変情報（整合性確認を行う）に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された監視対象の原始モデル（ブレーキモデル）を、取得した整合性確認を行う場合の原始モデルの変換規則に基づき上記実施の形態１と同様にして変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００４６】
図１７は設計モデル生成手段１１４により設計モデルとして生成された監視装置モデルを示す図であり、ブレーキ、データ整合性及び伝送路が取り得る状態と状態間の遷移を示している。すなわち、この監視装置モデルは、ブレーキ、データ整合性及び伝送路が正常状態、ブレーキが異常状態でデータ整合性及び伝送路が正常状態、データ整合性が異常状態で伝送路が正常状態並びに伝送路が異常状態の４状態と、状態間の遷移を示している。
この生成された設計モデルを用いて設計検証を行うことが可能である。また、開発の次段階に対する成果物として生成された設計モデルを活用することも可能である。
【００４７】
以上のように、この実施の形態２によれば、モデル変換規則格納手段１１３が原始モデルの変換規則を可変情報を含む要求仕様と対応付けて格納し、可変情報入力手段１１５がモデル変換規則格納手段１１３に格納されている要求仕様に含まれる可変情報を入力し、設計モデル生成手段１１４が、要求仕様入力手段１１２により入力された要求仕様と可変情報入力手段１１５により入力された可変情報に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することにより、設計対象の分野特有の多様な要求仕様に応じた設計モデルを容易に生成することができるという効果が得られる。
【００４８】
実施の形態３．
上記実施の形態２では要求仕様に可変情報を含む場合について説明したが、この実施の形態３では原始モデルの変換規則に可変情報を含む場合について説明する。
【００４９】
この実施の形態３におけるモデル生成装置の構成を示すブロック図は上記実施の形態２の図１３と同じである。ただし、図１３において、モデル変換規則格納手段１１３は可変情報を含む原始モデルの変換規則を要求仕様と対応付けて格納する。可変情報入力手段１１５はモデル変換規則格納手段１１３に格納されている原始モデルの変換規則に含まれる可変情報に設定するための所定値を入力する。設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、取得した原始モデルの変換規則に含まれる可変情報に可変情報入力手段１１５により入力された所定値を設定し、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した原始モデルの所定値が設定された可変情報を含む変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。その他の原始モデル入力手段１１１及び要求仕様入力手段１１２の処理は上記実施の形態２の処理と同じである。
【００５０】
この実施の形態３においても、列車におけるブレーキ監視装置に搭載するソフトウェアの設計を行う場合の処理の流れを説明する。
要求仕様入力手段１１２により要求仕様として入力される監視システムの構成は上記実施の形態１の図３と同じである。
【００５１】
図１８はこの実施の形態３における伝送路モデルを示す図であり、伝送路１２２が取り得る状態と状態間の遷移を示している。この伝送路モデルは、伝送路１２２が正常な正常状態（ＯＫ状態）及び伝送路１２２が輻輳した異常状態（ＮＧ状態）の２状態を有し、伝送路１２２が伝送タイムアウトになると正常状態から異常状態に遷移し、伝送路１２２が伝送タイムアウトから復帰すると異常状態から正常状態に遷移する。
【００５２】
図１９はモデル変換規則格納手段１１３に格納され対応付けられている要求仕様と原始モデルの変換規則の例を示す図であり、要求仕様が図３に示す監視システムの場合で、変換規則に含まれる可変情報として、変換規則４に伝送タイムアウトを設定可能な原始モデルの変換規則を示している。
【００５３】
図１９において、要求仕様が図３に示す監視システムの場合の原始モデルの変換規則は以下のようになっている。
変換規則１：監視対象の原始モデルと伝送路モデルを合成する
変換規則２：伝送路モデルは監視対象の原始モデルに対して監視性依存関係を持つ
変換規則３：監視性依存関係を持つ依存先モデルの異常状態を併合する
変換規則４：＜可変情報＞“伝送タイムアウト＝Ｘｍｓｅｃ”として合成する
【００５４】
図２０はこの実施の形態３におけるモデル生成装置の概略処理を示すフローチャートである。
ステップＳＴ３１において、要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。ここでは、要求仕様として、上記実施の形態１の図３に示す監視システムを入力する。
【００５５】
ステップＳＴ３２において、可変情報入力手段１１５は設計者からモデル変換規則格納手段１１３に格納されている原始モデルの変換規則に含まれる可変情報に設定するための所定値を入力する。この監視システムでは、図１９に示す変換規則１で示されている伝送路モデルが可変情報を持っており、伝送タイムアウトの時間を設定することができる。この内容は図１９に示す変換規則４として管理されている。ここでは、可変情報入力手段１１５は設計者からの指示により伝送タイムアウトの時間２００ｍｓｅｃを入力する。
【００５６】
ステップＳＴ３３において、原始モデル入力手段１１１は設計者から監視対象１２３であるブレーキが取り得る状態と状態間の遷移を示すブレーキモデルを監視対象の原始モデルとして入力し設計モデル生成手段１１４に出力する。このブレーキモデルは上記実施の形態１の図５に示すものと同じである。
【００５７】
ステップＳＴ３４において、設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、取得した原始モデルの変換規則に含まれる可変情報に可変情報入力手段１１５により入力された所定値を設定する。すなわち、設計モデル生成手段１１４は、可変情報としての変換規則４の変数Ｘに２００を代入して、次の変換規則４を設定する。
変換規則４：“伝送タイムアウト＝２００ｍｓｅｃ”として合成する
そして、設計モデル生成手段１１４は、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した原始モデルの所定値が設定された可変情報を含む変換規則に基づき上記実施の形態１と同様にして変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００５８】
図２１は設計モデル生成手段１１４により設計モデルとして生成された監視装置モデルを示す図であり、ブレーキ及び伝送路が取り得る状態と状態間の遷移を示している。すなわち、この監視装置モデルは、ブレーキ及び伝送路が正常状態、ブレーキが異常状態で伝送路が正常状態並びに伝送路が異常状態の３状態と、状態間の遷移を示している。
この生成された設計モデルを用いて設計検証を行うことが可能である。また、開発の次段階に対する成果物として生成された設計モデルを活用することも可能である。
【００５９】
以上のように、この実施の形態３によれば、モデル変換規則格納手段１１３が可変情報を含む原始モデルの変換規則を要求仕様と対応付けて格納し、可変情報入力手段１１５がモデル変換規則格納手段１１３に格納されている原始モデルの変換規則に含まれる可変情報に設定するための所定値を入力し、設計モデル生成手段１１４が、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、取得した原始モデルの変換規則に含まれる可変情報に可変情報入力手段１１５により入力された所定値を設定し、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した原始モデルの所定値が設定された可変情報を含む変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することにより、設計対象の分野特有の多様な要求仕様に応じた設計モデルを容易に生成することができるという効果が得られる。
【００６０】
実施の形態４．
この実施の形態４では、列車用のブレーキ監視装置が故障することを想定して二重化する場合の主系監視装置と待機系監視装置のソフトウェア設計方法について説明する。ここでは、ブレーキ監視装置が主系、待機系ともに故障しない限り、ブレーキ監視が正常に行われることを検証することを目的としている。
【００６１】
この実施の形態４におけるモデル生成装置の構成を示すブロック図は上記実施の形態２の図１３と同じである。ただし、モデル変換規則格納手段１１３は原始モデルの変換規則を検証目的の可変情報を含む要求仕様と対応付けて格納する。その他の原始モデル入力手段１１１、要求仕様入力手段１１２、可変情報入力手段１１５及び設計モデル生成手段１１４の処理は、上記実施の形態２の処理と同じである。
【００６２】
図２２は要求仕様入力手段１１２により要求仕様として入力される監視システムの構成を示す図である。この監視システムの構成では、監視装置である主系監視装置４１１及び待機系監視装置４１２と監視対象（原始モデル）４１４が伝送路４１３によって二対一で接続されている。
【００６３】
図２３は主系監視装置４１１の主系監視装置モデルを示す図であり、監視を行う主系監視装置４１１が取り得る状態と状態間の遷移を示している。この主系監視装置モデルは、正常に稼動している稼動状態（ＲＵＮ状態）及び主系監視装置４１１が故障した異常状態（ＮＧ状態）の２状態を有し、主系監視装置４１１が故障すると稼動状態から異常状態に遷移し、主系監視装置４１１が復帰すると異常状態から稼動状態に遷移する。
【００６４】
図２４は待機系監視装置４１２の待機系監視装置モデルを示す図であり、監視を行う待機系監視装置４１２が取り得る状態と状態間の遷移を示している。この待機系監視装置モデルは、主系監視装置４１１が故障した場合に正常に稼動している稼動状態（ＲＵＮ状態）、主系監視装置４１１が復帰した場合に待機している待機状態（ＷＡＩＴ状態）及び待機系監視装置４１２が故障した異常状態（ＮＧ状態）の３状態を有し、主系監視装置４１１が故障すると待機状態から稼動状態に遷移し、主系監視装置４１１が復帰すると稼動状態から待機状態に遷移し、待機系監視装置４１２が故障した場合に稼動状態又は待機状態から異常状態に遷移し、待機系監視装置４１２が復帰した場合に異常状態から稼動状態又は待機状態に遷移する。
【００６５】
図２５はモデル変換規則格納手段１１３に格納され対応付けられている要求仕様と原始モデルの変換規則の例を示す図であり、要求仕様が図２２に示す監視システムの場合で、要求仕様が検証目的の可変情報として二重故障は起こり得る場合と二重故障は起こらない場合が設定され、二重故障は起こり得る場合と二重故障は起こらない場合の原始モデルの変換規則を示している。
【００６６】
図２５において、要求仕様が図２２に示す監視システムの場合の原始モデルの変換規則は以下のようになっている。
二重故障は起こり得る場合
変換規則１：監視対象の原始モデルと主系監視装置モデルを合成する
変換規則２：監視対象の原始モデルと待機系監視装置モデルを合成する
二重故障は起こらない場合
変換規則１：監視対象の原始モデルと主系監視装置モデルを合成する
変換規則２：監視対象の原始モデルと待機系監視装置モデルを合成する
変換規則３：主系監視装置モデルと待機系監視装置モデルが同時に異常状態になることはない
【００６７】
また、この実施の形態４におけるモデル生成装置の概略処理を示すフローチャートは上記実施の形態２の図１６と同じである。
図１６のステップＳＴ２１において、要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。ここでは、要求仕様として図２２に示す監視システムを入力する。
【００６８】
図１６のステップＳＴ２２において、可変情報入力手段１１５は設計者からこの監視システムに対応する検証目的の可変情報を入力する。ここでは、検証目的の可変情報として「主系監視装置と待機系監視装置の二重故障は起こらない」を入力する。
【００６９】
図１６のステップＳＴ２３において、原始モデル入力手段１１１は設計者から監視対象４１４であるブレーキが取り得る状態と状態間の遷移を示すブレーキモデルを監視対象の原始モデルとして入力し設計モデル生成手段１１４に出力する。このブレーキモデルは上記実施の形態１の図５に示すものと同じである。
【００７０】
図１６のステップＳＴ２４において、設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様及び可変情報入力手段１１５により入力された検証目的の可変情報（二重故障は起こらない）に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した二重故障は起こらない場合の原始モデルの変換規則に基づき上記実施の形態１と同様にして変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００７１】
図２６は検証目的の可変情報として「主系監視装置と待機系監視装置の二重故障は起こらない」を入力した場合に設計モデル生成手段１１４により設計モデルとして生成された二重化監視装置モデルを示す図であり、ブレーキ、主系監視装置及び待機系監視装置が取り得る状態と状態間の遷移を示している。すなわち、この二重化監視装置モデルは、ブレーキが正常状態で主系監視装置が稼動状態で待機系監視装置が異常状態、ブレーキが正常状態で主系監視装置が稼動状態で待機系監視装置が待機状態、ブレーキが正常状態で主系監視装置が異常状態で待機系監視装置が稼動状態、ブレーキが異常状態で主系監視装置が稼動状態で待機系監視装置が異常状態、ブレーキが異常状態で主系監視装置が稼動状態で待機系監視装置が待機状態及びブレーキが異常状態で主系監視装置が異常状態で待機系監視装置が稼動状態の６状態と、状態間の遷移を示している。
図２６に示す二重化監視装置モデルではブレーキの状態を常に監視することができる。
【００７２】
上記図１６のステップＳＴ２２では、可変情報入力手段１１５が検証目的の可変情報として「主系監視装置と待機系監視装置の二重故障は起こらない」を入力しているが、検証目的の可変情報として「主系監視装置と待機系監視装置の二重故障は起こり得る」を入力した場合には、二重化監視装置モデルはブレーキの状態を監視することができない状態を有することとなる。
【００７３】
図２７は検証目的の可変情報として「主系監視装置と待機系監視装置の二重故障は起こり得る」を入力した場合に設計モデル生成手段１１４により設計モデルとして生成された二重化監視装置モデルを示す図であり、ブレーキ、主系監視装置及び待機系監視装置が取り得る状態と状態間の遷移を示している。すなわち、この二重化監視装置モデルは、ブレーキが正常状態で主系監視装置が稼動状態で待機系監視装置が異常状態、ブレーキが正常状態で主系監視装置が稼動状態で待機系監視装置が待機状態、ブレーキが正常状態で主系監視装置が異常状態で待機系監視装置が稼動状態、ブレーキが異常状態で主系監視装置が稼動状態で待機系監視装置が異常状態、ブレーキが異常状態で主系監視装置が稼動状態で待機系監視装置が待機状態、ブレーキが異常状態で主系監視装置が異常状態で待機系監視装置が稼動状態並びにブレーキが監視不能状態で主系監視装置及び待機系監視装置が異常状態の７状態と、状態間の遷移を示している。
【００７４】
以上のように、この実施の形態４によれば、モデル変換規則格納手段１１３が原始モデルの変換規則を可変情報を含む要求仕様と対応付けて格納し、可変情報入力手段１１５がモデル変換規則格納手段１１３に格納されている要求仕様に含まれる検証目的の可変情報を入力し、設計モデル生成手段１１４が、要求仕様入力手段１１２により入力された要求仕様と可変情報入力手段１１５により入力された検証目的の可変情報に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することにより、設計対象の分野特有の多様な要求仕様に応じた設計モデルを容易に生成することができると共に、検証目的の可変情報を指定するので、設計モデルの状態数及び遷移数を抑制することができ、設計検証をより短時間で行うことができるという効果が得られる。
【００７５】
実施の形態５．
この実施の形態５では、上記実施の形態４と同様に、列車用のブレーキ監視装置が故障することを想定して二重化する場合の主系監視装置と待機系監視装置のソフトウェア設計方法について説明する。ここでは、待機系監視装置が故障しないと仮定して検証することを目的としている。
【００７６】
この実施の形態５におけるモデル生成装置の構成を示すブロック図は上記実施の形態２の図１３と同じである。ただし、図１３において、モデル変換規則格納手段１１３は検証目的の可変情報を含む原始モデルの変換規則を要求仕様と対応付けて格納する。可変情報入力手段１１５はモデル変換規則格納手段１１３に格納されている原始モデルの変換規則に含まれる検証目的の可変情報に設定するための所定値を入力する。設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、取得した原始モデルの変換規則に含まれる検証目的の可変情報に可変情報入力手段１１５により入力された所定値を設定し、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した原始モデルの所定値が設定された検証目的の可変情報を含む変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。その他の原始モデル入力手段１１１及び要求仕様入力手段１１２の処理は上記実施の形態２の処理と同じである。
【００７７】
要求仕様入力手段１１２により要求仕様として入力される監視システムの構成は上記実施の形態４の図２２と同じであり、主系監視装置４１１の主系監視装置モデルは上記実施の形態４の図２３と同じである。
【００７８】
図２８は待機系監視装置４１２の待機系監視装置モデルを示す図であり、監視を行う待機系監視装置４１２が取り得る状態と状態間の遷移を示している。この待機系監視装置モデルは、主系監視装置４１１が故障した場合に正常に稼動している稼動状態（ＲＵＮ状態）、主系監視装置４１１が復帰した場合に待機している待機状態（ＷＡＩＴ状態）及び待機系監視装置４１２が故障した異常状態（ＮＧ状態）の３状態を有し、主系監視装置４１１が故障すると待機状態から稼動状態に遷移し、主系監視装置４１１が復帰すると稼動状態から待機状態に遷移し、待機系監視装置４１２が故障した場合に稼動状態又は待機状態から異常状態に遷移し、待機系監視装置４１２が復帰した場合に異常状態から稼動状態又は待機状態に遷移するが、待機系監視装置４１２の異常状態を可変情報により有効又は無効に設定できるようになっている。
【００７９】
図２９はモデル変換規則格納手段１１３に格納され対応付けられている要求仕様と原始モデルの変換規則の例を示す図であり、要求仕様が図２２に示す監視システムの場合で、変換規則の検証目的の可変情報として変換規則３を持ち、待機系監視装置４１２の異常状態を有効又は無効に設定可能な原始モデルの変換規則を示している。
【００８０】
図２９において、要求仕様が図２２に示す監視システムの場合の原始モデルの変換規則は以下のようになっている。
変換規則１：監視対象の原始モデルと主系監視装置モデルを合成する
変換規則２：監視対象の原始モデルと待機系監視装置モデルを合成する
変換規則３：＜可変情報＞待機系監視装置の異常状態を｛有効  無効｝とする
【００８１】
また、この実施の形態５におけるモデル生成装置の概略処理を示すフローチャートは上記実施の形態３の図２０と同じである。
図２０のステップＳＴ３１において、要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。要求仕様として入力された監視システムの構成は上記実施の形態４の図２２と同じである。
【００８２】
図２０のステップＳＴ３２において、可変情報入力手段１１５は設計者からモデル変換規則格納手段１１３に格納されている原始モデルの変換規則に含まれる検証目的の可変情報に設定するための所定値を入力する。この監視システムでは、図２９に示す変換規則２で示されている待機系監視装置モデルが検証目的の可変情報を持っており、待機系監視装置の異常状態を有効又は無効と設定することができる。この内容は図２９に示す変換規則３として管理されている。ここでは、可変情報入力手段１１５は設計者からの指示により待機系監視装置の異常状態の無効を入力する。
【００８３】
図２０のステップＳＴ３３において、原始モデル入力手段１１１は設計者から監視対象４１４であるブレーキが取り得る状態と状態間の遷移を示すブレーキモデルを監視対象の原始モデルとして入力し設計モデル生成手段１１４に出力する。このブレーキモデルは上記実施の形態１の図５に示すものと同じである。
【００８４】
図２０のステップＳＴ３４において、設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、取得した原始モデルの変換規則に含まれる可変情報に可変情報入力手段１１５により入力された所定値を設定する。すなわち、設計モデル生成手段１１４は、可変情報としての変換規則３に無効を入力し、次の変換規則３を設定する。
変換規則３：待機系監視装置の異常状態を無効とする
そして、設計モデル生成手段１１４は、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した原始モデルの所定値が設定された可変情報を含む変換規則に基づき上記実施の形態１と同様にして変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００８５】
図３０は「待機系監視装置の異常状態を無効とする」を入力した場合に設計モデル生成手段１１４により設計モデルとして生成された二重化監視装置モデルを示す図であり、ブレーキ、主系監視装置及び待機系監視装置が取り得る状態と状態間の遷移を示している。すなわち、この二重化監視装置モデルは、ブレーキが正常状態で主系監視装置が稼動状態で待機系監視装置が待機状態、ブレーキが正常状態で主系監視装置が異常状態で待機系監視装置が稼動状態、ブレーキが異常状態で主系監視装置が稼動状態で待機系監視装置が待機状態及びブレーキが異常状態で主系監視装置が異常状態で待機系監視装置が稼動状態の４状態と、状態間の遷移を示している。
図３０に示す二重化監視装置モデルではブレーキの状態を常に監視することができる。
【００８６】
なお、この二重化監視装置モデルにおいて、待機系監視装置の異常状態を有効と設定する場合は、上記実施の形態４の図２７に示すようなモデルとなり、検証に時間がかかることになる。
【００８７】
以上のように、この実施の形態５によれば、モデル変換規則格納手段１１３が検証目的の可変情報を含む原始モデルの変換規則を要求仕様と対応付けて格納し、可変情報入力手段１１５がモデル変換規則格納手段１１３に格納されている原始モデルの変換規則に含まれる検証目的の可変情報に設定するための所定値を入力し、設計モデル生成手段１１４が、要求仕様入力手段１１２により入力された要求仕様に対応する原始モデルの変換規則をモデル変換規則格納手段１１３より取得し、取得した原始モデルの変換規則に含まれる検証目的の可変情報に可変情報入力手段１１５により入力された所定値を設定し、原始モデル入力手段１１１により入力された監視対象の原始モデルを、取得した原始モデルの所定値が設定された検証目的の可変情報を含む変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することにより、設計対象の分野特有の多様な要求仕様に応じた設計モデルを容易に生成することができると共に、検証目的に応じて変換規則の可変情報を指定するので、設計モデルの状態数及び遷移数を抑制することができ、設計検証をより短時間で行うことができるという効果が得られる。
【００８８】
実施の形態６．
この実施の形態６では、ＣＰＵ監視装置に搭載するソフトウェアの設計時にモデル生成装置に入力する原始モデルに対して、設計者が付加情報を利用してモデル生成のヒントを付加する方法について説明する。
【００８９】
この実施の形態６におけるモデル生成装置の構成を示すブロック図は上記実施の形態１の図１と同様である。ただし、モデル変換規則格納手段１１３は、原始モデルの変換規則を要求仕様と対応付けて格納すると共に、原始モデルの変換規則を原始モデルに付加されている付加情報に対応付けて格納する。
図３１はモデル変換規則格納手段１１３に格納され対応付けられている付加情報と原始モデルの変換規則の例を示す図である。図３１において、原始モデルに付加されている付加情報と原始モデルの変換規則は以下のようになっている。
付加情報：＜＜Ｐｒｏｃｅｓｓｏｒ＞＞
変換規則：原始モデルを二重化する
【００９０】
また、設計モデル生成手段１１４は、原始モデル入力手段１１１により入力された監視対象の原始モデルに付加されている所定の付加情報を検出した場合に、モデル変換規則格納手段１１３から所定の付加情報及び要求仕様に対応する原始モデル変換規則を取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した所定の付加情報及び要求仕様に対応する原始モデルの変換規則に基づき変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
その他の原始モデル入力手段１１１及び要求仕様入力手段１１２の処理は上記実施の形態１と同様である。
【００９１】
要求仕様入力手段１１２により要求仕様として入力される監視システムの構成は上記実施の形態１の図３と同じであり、伝送路モデルを示す図は上記実施の形態１の図４と同じである。また、変換規則格納手段１１３に格納されている原始モデルの変換規則は上記実施の形態１の図６に示す要求仕様に対応する変換規則と、図３１に示す付加情報に対応する変換規則から構成されている。
【００９２】
図３２は原始モデル入力手段１１１により入力される監視対象の原始モデルとしてのＣＰＵモデルを示す図であり、監視対象のＣＰＵが取り得る状態と状態間の遷移を示している。このＣＰＵモデルは、ＣＰＵが正常に稼動している稼動状態（ＲＵＮ状態）及びＣＰＵが故障した異常状態（ＮＧ状態）の２状態を有し、ＣＰＵが故障すると稼動状態から異常状態に遷移し、ＣＰＵが復帰すると異常状態から稼動状態に遷移する。また、このＣＰＵモデルには、監視対象がプロセッサであることを示す付加情報＜＜Ｐｒｏｃｅｓｓｏｒ＞＞が付加されている。
【００９３】
この実施の形態６では、ＣＰＵ監視装置に搭載するソフトウェアの設計を行う場合の処理の流れを説明する。
この実施の形態６におけるモデル生成装置の概略処理を示すフローチャートは、上記実施の形態１の図７と同様である。
ステップＳＴ１において、要求仕様入力手段１１２はモデル変換規則格納手段１１３に格納されている要求仕様の一覧を取得し設計者により選択された要求仕様を入力する。ここでは、要求仕様として上記実施の形態１の図３に示す監視システムを入力する。
【００９４】
ステップＳＴ２において、原始モデル入力手段１１１は設計者から監視対象であるＣＰＵが取り得る状態と状態間の遷移を示すＣＰＵモデル（図３２）を監視対象の原始モデルとして入力し設計モデル生成手段１１４に出力する。なお、このＣＰＵモデルには、付加情報＜＜Ｐｒｏｃｅｓｓｏｒ＞＞が付加されている。
【００９５】
ステップＳＴ３において、設計モデル生成手段１１４は、原始モデル入力手段１１１により入力された監視対象の原始モデル（ＣＰＵモデル）に付加されている所定の付加情報を検出した場合に、モデル変換規則格納手段１１３から所定の付加情報に対応する原始モデルの変換規則を取得する。ここでは付加情報として＜＜Ｐｒｏｃｅｓｓｏｒ＞＞を検出した場合に、原始モデルを二重化するという変換規則を取得することができ、図３２に示す原始モデル（ＣＰＵモデル）を二重化し、要求仕様入力手段１１２により入力された要求仕様である監視システムを、監視対象を二重化した監視システムに変換する。
【００９６】
図３３は設計モデル生成手段１１４により変換された監視対象を二重化した監視システムを示す図であり、監視装置６２１と監視対象（ＣＰＵ１  ６２３、ＣＰＵ２  ６２４）が伝送路６２２により一対二で接続されている。
【００９７】
そして、設計モデル生成手段１１４は、要求仕様入力手段１１２により入力された要求仕様（監視システム）に対応する原始モデルの変換規則（上記実施の形態１の図６）をモデル変換規則格納手段１１３より取得し、取得した要求仕様に対応する原始モデルの変換規則に基づき、二重化した原始モデル（ＣＰＵモデル）を上記実施の形態１と同様にして変換し、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成する。
【００９８】
図３４は設計モデル生成手段１１４により設計モデルとして生成されたＣＰＵ監視装置モデルを示す図であり、ＣＰＵ１、ＣＰＵ２及び伝送路が取り得る状態と状態間の遷移を示している。すなわち、このＣＰＵ監視装置モデルはＣＰＵ１及びＣＰＵ２が稼動状態で伝送路が正常状態、ＣＰＵ１が稼動状態でＣＰＵ２が異常状態で伝送路が正常状態、ＣＰＵ１が異常状態でＣＰＵ２が稼動状態で伝送路が正常状態、ＣＰＵ１及びＣＰＵ２が異常状態で伝送路が正常状態並びに伝送路が異常状態の５状態と、状態間の遷移を示している。
生成されたこの設計モデルを用いて設計検証を行うことが可能であり、また、開発の次段階に対する成果物として活用することも可能である。
【００９９】
以上のように、この実施の形態６によれば、設計モデル生成手段１１４が、原始モデル入力手段１１１により入力された監視対象の原始モデルに付加されている所定の付加情報を検出した場合に、モデル変換規則格納手段１１３から所定の付加情報及び要求仕様に対応する原始モデルの変換規則を取得し、原始モデル入力手段１１１により入力された原始モデルを、取得した所定の付加情報及び要求仕様に対応する原始モデルの変換規則に基づき変換して、状態遷移モデル形式で表現されたソフトウェアの設計モデルを生成することにより、設計対象の分野特有の要求仕様に応じた設計モデルを容易に生成することができると共に、原始モデルの付加情報に応じた設計モデルを生成することができ、設計モデルの精度を向上することができるという効果が得られる。
【０１００】
実施の形態７
図３５はこの実施の形態７におけるモデル生成装置の構成を示すブロック図である。このモデル生成装置は、原始モデル入力手段１１１、要求仕様入力手段１１２、モデル変換規則格納手段１１３、設計モデル生成手段１１４及びモデル変換規則入力手段１１６を備えている。
【０１０１】
図３５において、モデル変換規則入力手段１１６は、対象とする要求仕様と原始モデルの変換規則を入力し、要求仕様で伝送路を使用する場合には伝送路モデルを入力し、モデル変換規則格納手段１１３は、モデル変換規則入力手段１１７により入力された要求仕様と原始モデルの変換規則を対応付けて格納すると共に伝送路モデルを格納する。その他の原始モデル入力手段１１１、要求仕様入力手段１１２及び設計モデル生成部１１４の処理は、上記実施の形態１の処理と同じである。このように、モデル変換規則入力手段１１６を備えることにより、モデル生成装置に対して新たなモデル変換規則を追加することが可能となる。
【０１０２】
例えば、上記実施の形態１の場合には、モデル変換規則入力手段１１６は、図３に示す要求仕様（監視システム）、図４に示す伝送路モデルと、次の原始モデルの変換規則を入力する。
変換規則１：監視対象の原始モデルと伝送路モデルを合成する
変換規則２：伝送路モデルは監視対象の原始モデルに対して監視性依存関係を持つ
変換規則３：監視性依存関係を持つ依存先モデルの異常状態を併合する
【０１０３】
モデル変換規則格納手段１１３は、モデル変換規則入力手段１１６により入力された伝送路モデルを格納すると共に、モデル変換規則入力手段１１６により入力された図３に示す要求仕様（監視システム）と変換規則１から変換規則３を対応付けて上記実施の形態１の図６に示すように格納する。
【０１０４】
以上のように、この実施の形態７によれば、上記実施の形態１と同様の効果が得られると共に、モデル変換規則入力手段１１６が要求仕様と原始モデルの変換規則を入力することにより、モデル変換の対象を拡げることができるという効果が得られる。
【図面の簡単な説明】
【０１０５】
【図１】実施の形態１におけるモデル生成装置の構成を示すブロック図である。
【図２】実施の形態１におけるモデル生成装置を実現するコンピュータの構成を示すブロック図である。
【図３】実施の形態１において要求仕様として入力される監視システムの構成を示す図である。
【図４】実施の形態１における伝送路の伝送路モデルを示す図である。
【図５】実施の形態１における監視対象の原始モデルとしてのブレーキモデルを示す図である。
【図６】実施の形態１における要求仕様と原始モデルの変換規則の例を示す図である。
【図７】実施の形態１におけるモデル生成装置の概略処理を示すフローチャートである。
【図８】実施の形態１において設計モデルとして生成された監視装置モデルを示す図である。
【図９】実施の形態１におけるモデル生成装置の詳細処理を示すフローチャートである。
【図１０】実施の形態１において図６に示す変換規則１により変換された４状態のモデルを示す図である。
【図１１】実施の形態１における監視対象の原始モデルとしての他のブレーキモデルを示す図である。
【図１２】実施の形態１において図１１に示すブレーキモデルの場合に設計モデルとして生成された監視装置モデルを示す図である。
【図１３】実施の形態２におけるモデル生成装置の構成を示すブロック図である。
【図１４】実施の形態２におけるデータ整合性モデルを示す図である。
【図１５】実施の形態２における要求仕様と原始モデルの変換規則の例を示す図である。
【図１６】実施の形態２におけるモデル生成装置の概略処理を示すフローチャートである。
【図１７】実施の形態２において設計モデルとして生成された監視装置モデルを示す図である。
【図１８】実施の形態３における伝送路モデルを示す図である。
【図１９】実施の形態３における要求仕様と原始モデルの変換規則の例を示す図である。
【図２０】この実施の形態３におけるモデル生成装置の概略処理を示すフローチャートである。
【図２１】実施の形態３において設計モデルとして生成された監視装置モデルを示す図である。
【図２２】実施の形態４における要求仕様として入力される監視システムの構成を示す図である。
【図２３】実施の形態４における主系監視装置の主系監視装置モデルを示す図である。
【図２４】実施の形態４における待機系監視装置の待機系監視装置モデルを示す図である。
【図２５】実施の形態４における要求仕様と原始モデルの変換規則の例を示す図である。
【図２６】実施の形態４において設計モデルとして生成された二重化監視装置モデルを示す図である。
【図２７】実施の形態４において設計モデルとして生成された二重化監視装置モデルを示す図である。
【図２８】実施の形態５における待機系監視装置の待機系監視装置モデルを示す図である。
【図２９】実施の形態５における要求仕様と原始モデルの変換規則の例を示す図である。
【図３０】実施の形態５において設計モデルとして生成された二重化監視装置モデルを示す図である。
【図３１】実施の形態６における付加情報と原始モデルの変換規則の例を示す図である。
【図３２】実施の形態６における監視対象の原始モデルとしてのＣＰＵモデルを示す図である。
【図３３】実施の形態６における監視対象を二重化した監視システムを示す図である。
【図３４】実施の形態６において設計モデルとして生成されたＣＰＵ監視装置モデルを示す図である。
【図３５】実施の形態７におけるモデル生成装置の構成を示すブロック図である。
【符号の説明】
【０１０６】
１  コンピュータ、２  ディスプレイ、３  キーボード、４  ポインティングデバイス、５  ＣＰＵ、６  メモリ、７  ハードディスク、１１１  原始モデル入力手段、１１２  要求仕様入力手段、１１３  モデル変換規則格納手段、１１４設計モデル生成手段、１１５  可変情報入力手段、１１６  モデル変換規則入力手段、１２１  監視装置、１２２  伝送路、１２３  監視対象、４１１  主系監視装置、４１２  待機系監視装置、４１３  伝送路、４１４  監視対象、６２１  監視装置、６２２  伝送路、６２３  監視対象ＣＰＵ１、６２４  監視対象ＣＰＵ２。
【図１】
2007241435.tif 000003
【図２】
2007241435.tif 000004
【図３】
2007241435.tif 000005
【図４】
2007241435.tif 000006
【図５】
2007241435.tif 000007
【図６】
2007241435.tif 000008
【図７】
2007241435.tif 000009
【図８】
2007241435.tif 000010
【図９】
2007241435.tif 000011
【図１０】
2007241435.tif 000012
【図１１】
2007241435.tif 000013
【図１２】
2007241435.tif 000014
【図１３】
2007241435.tif 000015
【図１４】
2007241435.tif 000016
【図１５】
2007241435.tif 000017
【図１６】
2007241435.tif 000018
【図１７】
2007241435.tif 000019
【図１８】
2007241435.tif 000020
【図１９】
2007241435.tif 000021
【図２０】
2007241435.tif 000022
【図２１】
2007241435.tif 000023
【図２２】
2007241435.tif 000024
【図２３】
2007241435.tif 000025
【図２４】
2007241435.tif 000026
【図２５】
2007241435.tif 000027
【図２６】
2007241435.tif 000028
【図２７】
2007241435.tif 000029
【図２８】
2007241435.tif 000030
【図２９】
2007241435.tif 000031
【図３０】
2007241435.tif 000032
【図３１】
2007241435.tif 000033
【図３２】
2007241435.tif 000034
【図３３】
2007241435.tif 000035
【図３４】
2007241435.tif 000036
【図３５】
2007241435.tif 000037