システム開発支援装置及びプログラム並びに方法
【課題】検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行手段に実装された状態遷移とが同等であることを保障する。
【解決手段】本発明の一態様に係るシステム開発支援装置１は、テスト対象の状態遷移実行手段７に対して、アーキテクチャ・モデル８１〜８ｎに対する形式検証技術４による検証結果データ１０１〜１０ｎに基づいて生成されたテストパターン１２にそった状態遷移を引き起こす事象を発生させ、状態遷移実行手段７が遷移した結果と、テストパターン１２の遷移結果とをマッピングし、このマッピング結果が同等か否かを示すテスト実行結果データ１３を生成するテスト実行手段６を具備する。
【解決手段】本発明の一態様に係るシステム開発支援装置１は、テスト対象の状態遷移実行手段７に対して、アーキテクチャ・モデル８１〜８ｎに対する形式検証技術４による検証結果データ１０１〜１０ｎに基づいて生成されたテストパターン１２にそった状態遷移を引き起こす事象を発生させ、状態遷移実行手段７が遷移した結果と、テストパターン１２の遷移結果とをマッピングし、このマッピング結果が同等か否かを示すテスト実行結果データ１３を生成するテスト実行手段６を具備する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、形式検証されたソフトウェア・アーキテクチャに基づいてシステムを設計／実装する場合の信頼性確保を実現するシステム開発支援装置及びプログラム並びに方法に関する。
【背景技術】
【０００２】
システムの検証に用いられる従来の形式検証技術について以下に説明する。
【０００３】
開発者Ａは、実装非依存（プラットフォーム非依存）のアーキテクチャ・モデル（例えば状態遷移図）を生成し、このアーキテクチャ・モデルを形式検証モデル生成部に入力する。
【０００４】
形式検証モデル生成部は、入力されたアーキテクチャ・モデルに基づいて、形式検証モデル（例えばＳＰＩＮにおけるＰｒｏｍｅｌａ）を生成する。なお、形式検証モデルの生成は、開発者Ａが行うとしてもよい。
【０００５】
いわゆる検証エンジンである形式検証モデル実行部（例えばＳＰＩＮ）は、形式検証モデルを入力し、この形式検証モデルについて、システムとして満たすべき制約条件を満たしているか否かを含む検証結果を出力する。
【０００６】
開発者Ａは、この検証結果を確認し、問題があればアーキテクチャ・モデルを修正し、上記の処理を繰り返す。これにより、最終的に、形式検証されたアーキテクチャ・モデルが得られる。
【０００７】
次に、開発者Ｂは、検証されたアーキテクチャ・モデルを参照しながら、開発対象となっているシステム実行環境で実行可能な状態遷移実行部（例えば状態遷移がハードコーティングされた実装）を生成し、その状態遷移実行部の出力である実行結果を確認する。開発者Ｂは、状態遷移実行部が、検証されたアーキテクチャ・モデルと等価な動作をすると認められるまで、独自に生成されたテストパターンを用いて、状態遷移実行部の修正を繰り返す。このような工程を経て、状態遷移実行部が開発される。
【０００８】
特許文献１（特開２００５−１８２８０６号公報）には、プログラムの所望の振る舞いを定義した形式仕様および進化的アルゴリズムを用いてプログラムを進化させ、正当性証明可能なプログラムを生成することが記載されている。
【０００９】
特許文献２（特開２００１−２０２３９７号公報）には、対象となるシステムの仕様からシステム・オン・チップのシステム・アーキテクチャの設計を支援するシステムが記載されている。この特許文献２のシステムは、ハードウェアモジュール及びソフトウェアモジュールの再利用可能なライブラリと、前記仕様記述に対応する複数のタスクの夫々に関して選択され、その実現に適したハードウェアモジュールとソフトウェアモジュールの組み合わせから、前記仕様記述に対応するシステムを実装するためのハードウェア及びソフトウェアのシステム・アーキテクチャを生成する。
【００１０】
特許文献３（特開２００５−４９９４７号公報）には、組込み系システムの制御ソフトウェアのシミュレーション装置であって、組込み系システムでの制御対象の等価入力情報を読取る読取り部と、制御ソフトウェアが処理した内容を書込む書込み部と、制御ソフトウェアの制御結果を判断する判断部と、を有する実機レスシミュレーション装置が記載されている。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２００５−１８２８０６号公報
【特許文献２】特開２００１−２０２３９７号公報
【特許文献３】特開２００５−４９９４７号公報
【発明の概要】
【発明が解決しようとする課題】
【００１２】
上記従来の形式検証技術においては、検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行部に実装された状態遷移とが同等であることを保障することが困難な場合がある。
【００１３】
本発明は、以上のような実情に鑑みてなされたもので、検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行部に実装された状態遷移とが同等であることを保障するためのシステム開発支援装置及びプログラム並びに方法を提供することを目的とする。
【課題を解決するための手段】
【００１４】
上記課題は、アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを記憶する第１の記憶手段と、前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識する実装認識手段と、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成する第１のマッピング手段と、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成する第２のマッピング手段と、前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶する第３マッピング手段と、前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶するテスト結果生成手段とを具備するシステム開発支援装置、により解決される。
【００１５】
なお、ここでは装置により課題が解決されているが、コンピュータシステム、方法、プログラム、コンピュータ読み取り可能な記録媒体などにより課題が解決されるとしてもよい。
【発明の効果】
【００１６】
本発明により、検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行部に実装された状態遷移とが同等であることを保障することができる。
【図面の簡単な説明】
【００１７】
【図１】本発明の実施の形態に係るシステム開発支援装置の構成の一例を示すブロック図。
【図２】アーキテクチャ・モデル生成からテストパターン生成までの処理の一例を示すフローチャート。
【図３】アーキテクチャ・モデルの一例を示す図。
【図４】検証結果データの一例を示す図。
【図５】本実施の形態に係るテストパターン生成部とテスト実行部の一例を示すブロック図。
【図６】テスト実行部の具体的構成の一例を示すブロック図。
【図７】本実施の形態に係るシステム開発支援装置をコンピュータで実現する場合の一例を示すブロック図。
【発明を実施するための形態】
【００１８】
以下、図面を参照しながら本発明の実施の形態について説明する。なお、以下の各図において略同一の部分については同一の符号を付して説明を省略する。
【００１９】
本実施の形態に係るシステム開発支援装置は、上流工程で開発されたソフトウェア・アーキテクチャに基づいてシステムの設計／実装を詳細化する開発工程において、ソフトウェア・アーキテクチャの内容に適合して設計／実装が開発されていることを、高い信頼性で確認可能にする。
【００２０】
本実施の形態において、開発者Ａ（例えばアーキテクト）は、形式検証技術を用いて、開発対象のシステムの仕様記述を、開発者Ａが開発したアーキテクチャ・モデルが満たしていることを確認する。この形式検証技術の結果として、状態遷移の履歴を含む検証結果が生成される。
【００２１】
次に、本実施の形態では、開発者Ｂ（例えば詳細設計者又は実装者）は、この開発者Ｂによって生成された詳細設計／実装が正しいか否かを確認するために、開発者Ｂによって生成された詳細設計／実装に対して、状態遷移履歴を含む検証結果にそった状態遷移を起こさせることが可能なテストフレームワークを利用し、開発者Ａによって開発されたアーキテクチャ・モデルと開発者Ｂによって生成された詳細設計／実装の動作とが同等であるか否か確認可能とする。
【００２２】
図１は、本実施の形態に係るシステム開発支援装置の構成の一例を示すブロック図である。
【００２３】
システム開発支援装置１は、記憶装置２ａ〜２ｈ、形式検証モデル生成部３、形式検証モデル実行部４、テストパターン生成部５、テスト実行部６、状態遷移実行部７、入力装置１４、出力装置１５を具備する。
【００２４】
本実施の形態において、形式検証モデル生成部３、形式検証モデル実行部４、テストパターン生成部５、テスト実行部６、状態遷移実行部７は、コンピュータが記録媒体１９に記録されているプログラム２０を実行することにより当該コンピュータによって実現されるとしてもよい。
【００２５】
システム開発支援装置１には、入力装置１４を用いて各種データ又は指示が入力される。入力された指示にしたがって、システム開発支援装置１は動作し、入力された各種データが例えば記憶装置２ａ〜２ｈのいずれかに記憶される。
【００２６】
また、システム開発支援装置１は、各種のデータのうち出力するように指示されたデータを、出力装置１５を用いて出力する。出力装置１５としては、例えばディスプレイ又はプリンタなどが用いられる。
【００２７】
本実施の形態において、開発者Ａ〜Ｃは、少なくとも２つが同一人物であってもよく、いずれもが別の人物であってもよい。例えば、開発者Ａと開発者Ｃは、同一人物であってもよい。また、開発者Ａ〜Ｃは、二人以上からなるグループであってもよい。
【００２８】
開発者Ａは、開発対象のシステムが満たすべき要件定義を実現するソフトウェア・アーキテクチャを検討し、このアーキテクチャの振舞いの表現であるアーキテクチャ・モデル（例えば状態遷移図）８１を生成する。
【００２９】
記憶装置２ａは、開発者Ａによって生成されたアーキテクチャ・モデル８１を記憶する。
【００３０】
形式検証モデル生成部３は、記憶装置２ａに記憶されているアーキテクチャ・モデル８１を読み出し、このアーキテクチャ・モデル８１に基づいて形式検証モデル９１を生成し、この形式検証モデル９１を記憶装置２ｂに記憶する。なお、形式検証モデル９１の生成手法については、既存の技術を利用可能である。形式検証モデル９１の一例としては、形式検証モデル実行部４がＳＰＩＮの場合のＰｒｏｍｅｌａがある。
【００３１】
形式検証モデル実行部（検証エンジン）４は、記憶装置２ｂに記憶されている形式検証モデル９１を読み出し、この形式検証モデル９１がシステムとして満たすべき制約条件、または、開発対象のソフトウェア・アーキテクチャが満たすべき制約条件を満たすか否かを検証した検証結果データ１０１を生成し、検証結果データ１０１を記憶装置２ｃに記憶する。この形式検証モデル実行部４は、形式検証モデル９１に対するシミュレーションを実行する。例えば、形式検証モデル実行部４は、形式検証モデル９１で示される状態遷移にデッドロック及び未到達状態などが存在しないことを網羅的に検証し、検証結果を出力する。この形式検証モデル実行部４としては、例えばＳＰＩＮ又はＮｕＳＭＶなどのような既存の検証エンジンを利用可能である。本実施の形態において、検証結果データ１０１には、状態遷移の履歴が含まれている。状態遷移の履歴としては、例えば、初期状態と遷移系列との組合せが少なくとも一つ含まれる。
【００３２】
開発者Ａは、記憶装置２ｃに記憶されている検証結果データ１０１を確認し、問題がある場合に、アーキテクチャ・モデル８１を修正したアーキテクチャ・モデル８２を生成し、アーキテクチャ・モデル８２を記憶装置２ａに記憶する。すると、形式検証モデル生成部３が、アーキテクチャ・モデル８１に基づいて形式検証モデル９２を生成し、記憶装置２ｂに記憶する。さらに、形式検証モデル実行部４が、形式検証モデル９２に基づいて検証結果データ１０２を生成し、記憶装置２ｃに記憶する。以下、同様の処理が繰り返される。この結果、記憶装置２ａには、アーキテクチャ・モデル８１〜８ｎが記憶され、記憶装置２ｂには、形式検証モデル９１〜９ｎが記憶され、記憶装置２ｃには、検証結果データ１０１〜１０ｎが記憶される。また、このように、アーキテクチャ・モデルの生成が正常なアーキテクチャ・モデルが得られるまで繰り返されることにより、最終的に、異常なアーキテクチャ・モデル８１〜８ｎ−１、形式検証モデル９１〜９ｎ−１、検証結果データ１０１〜１０ｎ−１と、形式検証された正常なアーキテクチャ・モデル８ｎ、形式検証モデル９ｎ、検証結果データ１０ｎが得られる。
【００３３】
本実施の形態においては、記憶装置２ｃに記憶された検証結果データ１０１〜１０ｎは、シミュレーション実行結果である。
【００３４】
テストパターン生成部５は、記憶装置２ｃに記憶されている検証結果データ１０１〜１０ｎのうちの少なくとも一つに基づいて、状態遷移実行部７に対して状態遷移を起こさせることを可能とするためのテストパターン１２を生成し、テストパターン１２を記憶装置２ｄに記憶する。すなわち、テストパターン生成部５は、検証結果データ１０１〜１０ｎのうちの少なくとも一つに含まれている状態遷移の履歴を用いて、状態遷移実行部７をテストするために使用されるテストパターン１２を生成する。なお、本実施の形態において、テストパターン生成部５は、検証結果データの内容を出力装置１５によって出力し、入力装置１４によって開発者Ｃの指示及び入力内容を受け、この開発者Ｃの指示及び入力内容に応じてテストパターン１２を生成するとしている。
【００３５】
本実施の形態において、テストパターン１２には、少なくとも一つの状態遷移（初期状態とこの初期状態からの遷移系列）とその結果（正常（ＯＫ）又は異常（ＮＧ））が含まれているとする。
【００３６】
状態遷移実行部７は、最終的に形式検証されたアーキテクチャ・モデル８ｎにしたがって生成されたハードコーティング実装である。開発者Ｂは、アーキテクチャ・モデル８ｎを参照しながら、より詳細なソフトウェアの設計及び実行を行い、開発対象となっているシステム実行環境で実行可能でありシステムが振舞うべき状態が実装された状態遷移実行部７を生成し、システム開発支援装置１に搭載する。なお、この状態遷移実行部７は、上述したように、記憶媒体１９に記憶されたプログラム２０がプロセッサなどによって実行されることで実現されるとしてもよい。
【００３７】
テスト実行部６は、記憶装置２ｄに記憶されているテストパターン１２を読み出し、テスト対象の状態遷移実行部７に対して、テストパターン１２に含まれている初期状態からの状態遷移（遷移系列）を促すイベント等を発生させ、状態遷移実行部７をテスト動作させる。
【００３８】
また、テスト実行部６は、例えば、テストパターン１２に含まれている状態遷移を状態遷移実行部７に実行させた場合の実行結果（ＯＫ又はＮＧ）と、テストパターン１２で規定されている状態遷移の結果（ＯＫ又はＮＧ）とを比較し、この比較の結果が同等であるか否かを示すテスト実行結果データ１３を生成する。
【００３９】
そして、テスト実行部６は、生成されたテスト実行結果データ１３を記憶装置２ｅに記憶する。
【００４０】
開発者Ｂ又は別の開発者は、このテスト実行結果データ１３を参照し、状態遷移実行部７のテスト結果が、予めテストパターン１２で規定されている結果と等しいか否か判断し、これにより状態遷移実行部７がアーキテクチャ・モデル８ｎと同等であるか判断する。
【００４１】
また、例えば、テスト実行部６は、自動で、テストパターン１２で規定されている状態遷移が状態遷移実行部７によって同等に実行されたか否か判断し、すべての状態遷移が同等であるか、及び、同等でない場合にはどの状態遷移において整合していないかを示すテスト実行結果データ１３を生成する。これにより、開発者Ｂ又は別の開発者は、このテスト実行結果データ１３を参照し、生成された状態遷移実行部７が正しいか否か容易に確認できる。
【００４２】
図２は、アーキテクチャ・モデル生成からテストパターン生成までの処理の一例を示すフローチャートである。
【００４３】
開発者Ａは、開発しているシステムが満たすべき要件定義にしたがって、アーキテクチャの検討を行う。ここで生成される成果物がアーキテクチャ・モデル８１（いわゆる状態遷移モデル）である。
【００４４】
ステップＳ１において、記憶装置２ａは、生成されたアーキテクチャ・モデル８１を記憶する。
【００４５】
ステップＳ２において、形式検証モデル生成部３は、記憶装置２ａに記憶されているアーキテクチャ・モデル８１に基づいて、形式検証モデル９１を生成し、この形式検証モデル９１を記憶装置２ｂに記憶する。
【００４６】
ステップＳ３において、形式検証モデル実行部４は、記憶装置２ｂに記憶されている形式検証モデル９１に基づいて、モデル検証を行い、その結果得られる検証結果データ１０１を記憶装置２ｃに記憶する。
【００４７】
モデル検証は、いわゆる形式検証とも言われ、形式検証モデル９１においてデッドロックが発生しないこと、到達し得ない状態を持たないことなどを網羅的に検証する。
【００４８】
ステップＳ４において、テストパターン生成部５は、開発者Ｃ（開発者Ａでもよい）の操作及び指定に応じて、検証結果データ１０１に含まれている初期状態とその遷移系列（イベント系列）に対して、この遷移系列が正常であるか異常であるかを示す情報を付して、テストパターン１２の一要素として記憶装置２ｄに記憶する。
【００４９】
ステップＳ５において上記処理を繰り返すか否か判断され、繰り返される場合には処理はステップＳ１に戻る。繰り返されない場合は処理を終了する。
【００５０】
例えば、アーキテクチャ・モデル８１の開発において不備がある場合には、次のアーキテクチャ・モデル８２、形式検証モデル９２、検証結果データ１０２が生成され、検証結果データ１０２に含まれている初期状態とその遷移系列に対して正常又は異常を示す情報を付したデータが、テストパターン１２の一要素として記憶装置２ｄに記憶される。そして、最終的に、形式検証された正常なアーキテクチャ・モデル８ｎ、形式検証モデル９ｎ、検証結果データ１０ｎが生成され、正常な検証結果データ１０ｎに含まれる初期状態とその遷移系列に対して正常を示す情報を付したデータが、テストパターン１２の一要素として記憶装置２ｄに記憶されるまで、ステップＳ１〜Ｓ４の処理は繰り返される。
【００５１】
このように、一般的に、アーキテクチャの開発途中で不備がある段階では、不備を反映した検証結果データ（ＮＧの検証結果）１０１〜１０ｎ-1が複数得られる。そして、アーキテクチャの開発の最後の段階では、正常な検証結果データ（ＯＫの検証結果）１０ｎが一種類得られる。
【００５２】
上記の検証結果データ１０１〜１０ｎは、上述したように、それぞれの場合の状態遷移の履歴、すなわち初期状態及び遷移系列の集合を含む。
【００５３】
なお、テストパターン生成部５は、開発者Ｃの操作及び指定に応じて、生成された複数の検証結果データ１０１〜１０ｎのうちどのデータをテストパターン１２として採用するかの指定を受け、採用する旨の指定を受けたデータをテストパターン１２の一要素として登録するとしてもよい。
【００５４】
図３は、アーキテクチャ・モデル８１（状態遷移モデル）の一例を示す図である。
【００５５】
丸で囲まれたアルファベットは、それぞれ状態を表す。状態から状態へ向かう矢印は、状態の遷移を表す。矢印に付されている数字は状態遷移を引き起こした事象（イベント）を表す。
【００５６】
図４は、検証結果データ１０１の一例を示す図である。
【００５７】
検証結果データ１０１における状態遷移履歴の記述例としては、｛Ａ，{２，３}｝などで記述できる。｛Ａ，{２，３}｝において、Ａは初期状態であり、{２，３}は状態の遷移を引き起こす事象を発生順に並べた遷移系列である。
【００５８】
図５は、本実施の形態に係るテストパターン生成部５とテスト実行部６の一例を示すブロック図である。すなわち、この図５においては、検証結果データ１０１〜１０ｎに基づいてテストパターン１２が生成されてから、テスト実行結果データ１３が生成されるまでの工程を表している。
【００５９】
また、図６は、本実施の形態に係るテスト実行部６の具体的構成の一例を示すブロック図である。
【００６０】
テストパターン生成部５は、複数のＮＧの検証結果データ１０１〜１０ｎ−１と一つのＯＫの検証結果データ１０ｎを読み出す。
【００６１】
開発者Ｃは、テストパターン生成部５を用いて、検証結果データ１０１〜１０ｎに含まれている初期状態と遷移系列について、テストパターンとしての実行時間が適切になるように、遷移系列を分割又は統合し、この初期状態と遷移系列の適用結果が正常（ＯＫ）か異常（ＮＧ）かを対応付ける（マッピングする）。
【００６２】
テストパターン生成部５は、正常で終了する初期状態と遷移系列を正常系のテストパターンの要素、異常（テストパターンで規定された遷移の系列と実際の処理系が遷移する系列とが異なる状態）で終了する初期状態と遷移系列を異常系のテストパターンの要素として体系化したテストパターン１２を生成し、記憶する。
【００６３】
テスト実行部６は、読み出し部６１、実装認識部６２、第１マッピング部６３、第２マッピング部６４、第３マッピング部６５、テスト結果生成部６６を具備する。
【００６４】
読み出し部６１は、記憶装置２ｄからテストパターン１２を読み出す。
【００６５】
実装認識部６２は、テスト対象の状態遷移実行部７（オブジェクト指向言語によって開発されたプログラムであればそのオブジェクトの状態又はメモリ上での値）が取る状態と、その状態から他の状態へ遷移する事象（割り込み、メッセージ送信、ソフトウェア・イベントなど）とを認識する。
【００６６】
第１マッピング部６３は、読み出されたテストパターン１２と実装認識部６２の認識結果とに基づいて、テストパターン１２に記述されている状態と、テスト対象の状態遷移実行部７が取る状態との対応関係を表す第１のマッピングデータ１６を生成し、この第１のマッピングデータ１６を記憶装置２ｆに記憶する。すなわち、テスト実行部６の第１マッピング部６３は、テスト対象の状態遷移実行部７の初期状態の設定を行い、テストパターン１２における状態と実装オブジェクトとのマッピングを行う。
【００６７】
第２マッピング部６４は、読み出されたテストパターン１２と実装認識部６２の認識結果とに基づいて、テストパターン１２における状態遷移を引き起こす事象がテスト対象の状態遷移実行部７のどの事象に対応するかのマッピングを行い、第２のマッピングデータ１７を記憶装置２ｇに記憶する。
【００６８】
第３マッピング部６５は、第１のマッピングデータ１６及び第２のマッピングデータ１７の設定に基づいて、テスト対象の状態遷移実行部７に対して、テストパターン１２にそった状態遷移を引き起こす事象を発生させ、テスト対象の状態遷移実行部７が遷移（移行）した状態を取得し、この遷移後の状態とテストパターン１２の最終の遷移状態とを比較するために対応付けるマッピングを行い、この結果得られる第３のマッピングデータ１８を記憶装置２ｈに記憶する。すなわち、テスト実行部６の第３マッピング部６５は、テスト対象の状態遷移実行部７がテストパターン１２を実行して最後に遷移した状態（オブジェクトの状態、メモリの状態など）を取得し、この取得した状態をテストパターン１２で期待された状態と比較するためのマッピングを行う。
【００６９】
なお、本実施の形態において、これらのマッピングは、テスト実行部６によって自動的に行われるが、開発者Ｂなどによってマッピングが行われ、テスト実行部６は、開発者Ｂによって与えられたマッピングデータを利用するとしてもよい。
【００７０】
そして、テスト結果生成部６６は、第３のマッピングデータ１８に基づいて、テスト対象の状態遷移実行部７の実装が遷移（移行）した状態と、テストパターン１２の遷移状態とを比較し、状態遷移実行部７でアーキテクチャ・モデル８１と同等の遷移が行われたか否かを判断した結果を示すテスト実行結果データ１３を記憶装置２ｅに記憶する。なお、テスト実行結果データ１３には、第３のマッピングデータ１８が含まれており、開発者Ｂは、テスト実行結果データ１３を出力装置１５から出力し、第３のマッピングデータ１８の内容を検討することができるとしてもよい。
【００７１】
以上説明した本実施の形態は、形式検証技術を用いてシステムのソフトウェア・アーキテクチャの開発を行う場合の、アーキテクチャが満たすべき制約条件を満たしているか検証を行うための形式検証モデルの検証、及び、シミュレーション実行可能な形式検証モデル実行部４（例えばＳＰＩＮ）を備えたシステム開発支援環境に適用される。
【００７２】
本実施の形態に係るシステム開発支援装置１は、シミュレーション実行結果（検証がＮＧであった場合とＯＫの場合とを含む）に基づいてテストパターン１２を生成するテストパターン生成部５と、システムの振舞いが実装された状態遷移実行部７に対してテストパターン１２にしたがったテストを実行するテスト実行部６とを具備する。
【００７３】
本実施の形態に係るシステム開発支援装置１を用いて確認を行うことにより、検証によって正常とされたアーキテクチャ・モデル８ｎで規定された状態遷移が、開発された状態遷移実行部７によって実行可能であることを保障することができる。
【００７４】
本実施の形態において、開発者は、検証されたアーキテクチャ・モデル８ｎで規定された状態遷移が、開発対象のシステムの実行環境で実現されているか容易に判断可能である。
【００７５】
本実施の形態においては、形式検証されたソフトウェア・アーキテクチャに基づいてシステムを設計／実装する場合の信頼性を確保することができる。すなわち、本実施の形態においては、上流工程で開発されたソフトウェア・アーキテクチャに基づいてシステムの設計／実装を詳細化していく場合に、設計／実装がソフトウェア・アーキテクチャに基づいて開発されていることを、高い信頼性で確認することができる。
【００７６】
なお、本実施の形態において、各種の構成要素は自由に組み合わせ又は分離することができる。例えば、各記憶装置２ａ〜２ｈは、自由に組み合わせることができ、また分割することもできる。
【００７７】
本実施の形態において、状態遷移実行部７は、例えば、システムとして振舞うべき状態遷移記述が定義されており、この状態遷移記述にしたがってシステムの状態を遷移させる状態遷移記述解釈実行部であるとしてもよい。
【００７８】
本実施の形態に係るシステム開発支援装置１は、図７に示すように、コンピュータ２１によって実現されるとしてもよい。例えば、コンピュータ２１は、プロセッサ２２、記憶装置２、入力装置１４、出力装置１５を具備する。プロセッサ２２は、記録媒体１９のプログラム２０を読み出して実行する。記憶装置２は、上記記憶装置２ａ〜２ｈとして利用される。
【符号の説明】
【００７９】
１…システム開発支援装置、２，２ａ〜２ｈ…記憶装置、３…形式検証モデル生成部、４…形式検証モデル実行部、５…テストパターン生成部、６…テスト実行部、７…状態遷移実行部、８１〜８ｎ…アーキテクチャ・モデル、９１〜９ｎ…形式検証モデル、１０１〜１０ｎ…検証結果データ、１２…テストパターン、１３…テスト実行結果データ、１４…入力装置、１５…出力装置、１６…第１のマッピングデータ、１７…第２のマッピングデータ、１８…第３のマッピングデータ、１９…記録媒体、２０…プログラム、２１…コンピュータ、２２…プロセッサ
【技術分野】
【０００１】
本発明は、形式検証されたソフトウェア・アーキテクチャに基づいてシステムを設計／実装する場合の信頼性確保を実現するシステム開発支援装置及びプログラム並びに方法に関する。
【背景技術】
【０００２】
システムの検証に用いられる従来の形式検証技術について以下に説明する。
【０００３】
開発者Ａは、実装非依存（プラットフォーム非依存）のアーキテクチャ・モデル（例えば状態遷移図）を生成し、このアーキテクチャ・モデルを形式検証モデル生成部に入力する。
【０００４】
形式検証モデル生成部は、入力されたアーキテクチャ・モデルに基づいて、形式検証モデル（例えばＳＰＩＮにおけるＰｒｏｍｅｌａ）を生成する。なお、形式検証モデルの生成は、開発者Ａが行うとしてもよい。
【０００５】
いわゆる検証エンジンである形式検証モデル実行部（例えばＳＰＩＮ）は、形式検証モデルを入力し、この形式検証モデルについて、システムとして満たすべき制約条件を満たしているか否かを含む検証結果を出力する。
【０００６】
開発者Ａは、この検証結果を確認し、問題があればアーキテクチャ・モデルを修正し、上記の処理を繰り返す。これにより、最終的に、形式検証されたアーキテクチャ・モデルが得られる。
【０００７】
次に、開発者Ｂは、検証されたアーキテクチャ・モデルを参照しながら、開発対象となっているシステム実行環境で実行可能な状態遷移実行部（例えば状態遷移がハードコーティングされた実装）を生成し、その状態遷移実行部の出力である実行結果を確認する。開発者Ｂは、状態遷移実行部が、検証されたアーキテクチャ・モデルと等価な動作をすると認められるまで、独自に生成されたテストパターンを用いて、状態遷移実行部の修正を繰り返す。このような工程を経て、状態遷移実行部が開発される。
【０００８】
特許文献１（特開２００５−１８２８０６号公報）には、プログラムの所望の振る舞いを定義した形式仕様および進化的アルゴリズムを用いてプログラムを進化させ、正当性証明可能なプログラムを生成することが記載されている。
【０００９】
特許文献２（特開２００１−２０２３９７号公報）には、対象となるシステムの仕様からシステム・オン・チップのシステム・アーキテクチャの設計を支援するシステムが記載されている。この特許文献２のシステムは、ハードウェアモジュール及びソフトウェアモジュールの再利用可能なライブラリと、前記仕様記述に対応する複数のタスクの夫々に関して選択され、その実現に適したハードウェアモジュールとソフトウェアモジュールの組み合わせから、前記仕様記述に対応するシステムを実装するためのハードウェア及びソフトウェアのシステム・アーキテクチャを生成する。
【００１０】
特許文献３（特開２００５−４９９４７号公報）には、組込み系システムの制御ソフトウェアのシミュレーション装置であって、組込み系システムでの制御対象の等価入力情報を読取る読取り部と、制御ソフトウェアが処理した内容を書込む書込み部と、制御ソフトウェアの制御結果を判断する判断部と、を有する実機レスシミュレーション装置が記載されている。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２００５−１８２８０６号公報
【特許文献２】特開２００１−２０２３９７号公報
【特許文献３】特開２００５−４９９４７号公報
【発明の概要】
【発明が解決しようとする課題】
【００１２】
上記従来の形式検証技術においては、検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行部に実装された状態遷移とが同等であることを保障することが困難な場合がある。
【００１３】
本発明は、以上のような実情に鑑みてなされたもので、検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行部に実装された状態遷移とが同等であることを保障するためのシステム開発支援装置及びプログラム並びに方法を提供することを目的とする。
【課題を解決するための手段】
【００１４】
上記課題は、アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを記憶する第１の記憶手段と、前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識する実装認識手段と、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成する第１のマッピング手段と、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成する第２のマッピング手段と、前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶する第３マッピング手段と、前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶するテスト結果生成手段とを具備するシステム開発支援装置、により解決される。
【００１５】
なお、ここでは装置により課題が解決されているが、コンピュータシステム、方法、プログラム、コンピュータ読み取り可能な記録媒体などにより課題が解決されるとしてもよい。
【発明の効果】
【００１６】
本発明により、検証されたアーキテクチャ・モデルで規定された状態遷移と、状態遷移実行部に実装された状態遷移とが同等であることを保障することができる。
【図面の簡単な説明】
【００１７】
【図１】本発明の実施の形態に係るシステム開発支援装置の構成の一例を示すブロック図。
【図２】アーキテクチャ・モデル生成からテストパターン生成までの処理の一例を示すフローチャート。
【図３】アーキテクチャ・モデルの一例を示す図。
【図４】検証結果データの一例を示す図。
【図５】本実施の形態に係るテストパターン生成部とテスト実行部の一例を示すブロック図。
【図６】テスト実行部の具体的構成の一例を示すブロック図。
【図７】本実施の形態に係るシステム開発支援装置をコンピュータで実現する場合の一例を示すブロック図。
【発明を実施するための形態】
【００１８】
以下、図面を参照しながら本発明の実施の形態について説明する。なお、以下の各図において略同一の部分については同一の符号を付して説明を省略する。
【００１９】
本実施の形態に係るシステム開発支援装置は、上流工程で開発されたソフトウェア・アーキテクチャに基づいてシステムの設計／実装を詳細化する開発工程において、ソフトウェア・アーキテクチャの内容に適合して設計／実装が開発されていることを、高い信頼性で確認可能にする。
【００２０】
本実施の形態において、開発者Ａ（例えばアーキテクト）は、形式検証技術を用いて、開発対象のシステムの仕様記述を、開発者Ａが開発したアーキテクチャ・モデルが満たしていることを確認する。この形式検証技術の結果として、状態遷移の履歴を含む検証結果が生成される。
【００２１】
次に、本実施の形態では、開発者Ｂ（例えば詳細設計者又は実装者）は、この開発者Ｂによって生成された詳細設計／実装が正しいか否かを確認するために、開発者Ｂによって生成された詳細設計／実装に対して、状態遷移履歴を含む検証結果にそった状態遷移を起こさせることが可能なテストフレームワークを利用し、開発者Ａによって開発されたアーキテクチャ・モデルと開発者Ｂによって生成された詳細設計／実装の動作とが同等であるか否か確認可能とする。
【００２２】
図１は、本実施の形態に係るシステム開発支援装置の構成の一例を示すブロック図である。
【００２３】
システム開発支援装置１は、記憶装置２ａ〜２ｈ、形式検証モデル生成部３、形式検証モデル実行部４、テストパターン生成部５、テスト実行部６、状態遷移実行部７、入力装置１４、出力装置１５を具備する。
【００２４】
本実施の形態において、形式検証モデル生成部３、形式検証モデル実行部４、テストパターン生成部５、テスト実行部６、状態遷移実行部７は、コンピュータが記録媒体１９に記録されているプログラム２０を実行することにより当該コンピュータによって実現されるとしてもよい。
【００２５】
システム開発支援装置１には、入力装置１４を用いて各種データ又は指示が入力される。入力された指示にしたがって、システム開発支援装置１は動作し、入力された各種データが例えば記憶装置２ａ〜２ｈのいずれかに記憶される。
【００２６】
また、システム開発支援装置１は、各種のデータのうち出力するように指示されたデータを、出力装置１５を用いて出力する。出力装置１５としては、例えばディスプレイ又はプリンタなどが用いられる。
【００２７】
本実施の形態において、開発者Ａ〜Ｃは、少なくとも２つが同一人物であってもよく、いずれもが別の人物であってもよい。例えば、開発者Ａと開発者Ｃは、同一人物であってもよい。また、開発者Ａ〜Ｃは、二人以上からなるグループであってもよい。
【００２８】
開発者Ａは、開発対象のシステムが満たすべき要件定義を実現するソフトウェア・アーキテクチャを検討し、このアーキテクチャの振舞いの表現であるアーキテクチャ・モデル（例えば状態遷移図）８１を生成する。
【００２９】
記憶装置２ａは、開発者Ａによって生成されたアーキテクチャ・モデル８１を記憶する。
【００３０】
形式検証モデル生成部３は、記憶装置２ａに記憶されているアーキテクチャ・モデル８１を読み出し、このアーキテクチャ・モデル８１に基づいて形式検証モデル９１を生成し、この形式検証モデル９１を記憶装置２ｂに記憶する。なお、形式検証モデル９１の生成手法については、既存の技術を利用可能である。形式検証モデル９１の一例としては、形式検証モデル実行部４がＳＰＩＮの場合のＰｒｏｍｅｌａがある。
【００３１】
形式検証モデル実行部（検証エンジン）４は、記憶装置２ｂに記憶されている形式検証モデル９１を読み出し、この形式検証モデル９１がシステムとして満たすべき制約条件、または、開発対象のソフトウェア・アーキテクチャが満たすべき制約条件を満たすか否かを検証した検証結果データ１０１を生成し、検証結果データ１０１を記憶装置２ｃに記憶する。この形式検証モデル実行部４は、形式検証モデル９１に対するシミュレーションを実行する。例えば、形式検証モデル実行部４は、形式検証モデル９１で示される状態遷移にデッドロック及び未到達状態などが存在しないことを網羅的に検証し、検証結果を出力する。この形式検証モデル実行部４としては、例えばＳＰＩＮ又はＮｕＳＭＶなどのような既存の検証エンジンを利用可能である。本実施の形態において、検証結果データ１０１には、状態遷移の履歴が含まれている。状態遷移の履歴としては、例えば、初期状態と遷移系列との組合せが少なくとも一つ含まれる。
【００３２】
開発者Ａは、記憶装置２ｃに記憶されている検証結果データ１０１を確認し、問題がある場合に、アーキテクチャ・モデル８１を修正したアーキテクチャ・モデル８２を生成し、アーキテクチャ・モデル８２を記憶装置２ａに記憶する。すると、形式検証モデル生成部３が、アーキテクチャ・モデル８１に基づいて形式検証モデル９２を生成し、記憶装置２ｂに記憶する。さらに、形式検証モデル実行部４が、形式検証モデル９２に基づいて検証結果データ１０２を生成し、記憶装置２ｃに記憶する。以下、同様の処理が繰り返される。この結果、記憶装置２ａには、アーキテクチャ・モデル８１〜８ｎが記憶され、記憶装置２ｂには、形式検証モデル９１〜９ｎが記憶され、記憶装置２ｃには、検証結果データ１０１〜１０ｎが記憶される。また、このように、アーキテクチャ・モデルの生成が正常なアーキテクチャ・モデルが得られるまで繰り返されることにより、最終的に、異常なアーキテクチャ・モデル８１〜８ｎ−１、形式検証モデル９１〜９ｎ−１、検証結果データ１０１〜１０ｎ−１と、形式検証された正常なアーキテクチャ・モデル８ｎ、形式検証モデル９ｎ、検証結果データ１０ｎが得られる。
【００３３】
本実施の形態においては、記憶装置２ｃに記憶された検証結果データ１０１〜１０ｎは、シミュレーション実行結果である。
【００３４】
テストパターン生成部５は、記憶装置２ｃに記憶されている検証結果データ１０１〜１０ｎのうちの少なくとも一つに基づいて、状態遷移実行部７に対して状態遷移を起こさせることを可能とするためのテストパターン１２を生成し、テストパターン１２を記憶装置２ｄに記憶する。すなわち、テストパターン生成部５は、検証結果データ１０１〜１０ｎのうちの少なくとも一つに含まれている状態遷移の履歴を用いて、状態遷移実行部７をテストするために使用されるテストパターン１２を生成する。なお、本実施の形態において、テストパターン生成部５は、検証結果データの内容を出力装置１５によって出力し、入力装置１４によって開発者Ｃの指示及び入力内容を受け、この開発者Ｃの指示及び入力内容に応じてテストパターン１２を生成するとしている。
【００３５】
本実施の形態において、テストパターン１２には、少なくとも一つの状態遷移（初期状態とこの初期状態からの遷移系列）とその結果（正常（ＯＫ）又は異常（ＮＧ））が含まれているとする。
【００３６】
状態遷移実行部７は、最終的に形式検証されたアーキテクチャ・モデル８ｎにしたがって生成されたハードコーティング実装である。開発者Ｂは、アーキテクチャ・モデル８ｎを参照しながら、より詳細なソフトウェアの設計及び実行を行い、開発対象となっているシステム実行環境で実行可能でありシステムが振舞うべき状態が実装された状態遷移実行部７を生成し、システム開発支援装置１に搭載する。なお、この状態遷移実行部７は、上述したように、記憶媒体１９に記憶されたプログラム２０がプロセッサなどによって実行されることで実現されるとしてもよい。
【００３７】
テスト実行部６は、記憶装置２ｄに記憶されているテストパターン１２を読み出し、テスト対象の状態遷移実行部７に対して、テストパターン１２に含まれている初期状態からの状態遷移（遷移系列）を促すイベント等を発生させ、状態遷移実行部７をテスト動作させる。
【００３８】
また、テスト実行部６は、例えば、テストパターン１２に含まれている状態遷移を状態遷移実行部７に実行させた場合の実行結果（ＯＫ又はＮＧ）と、テストパターン１２で規定されている状態遷移の結果（ＯＫ又はＮＧ）とを比較し、この比較の結果が同等であるか否かを示すテスト実行結果データ１３を生成する。
【００３９】
そして、テスト実行部６は、生成されたテスト実行結果データ１３を記憶装置２ｅに記憶する。
【００４０】
開発者Ｂ又は別の開発者は、このテスト実行結果データ１３を参照し、状態遷移実行部７のテスト結果が、予めテストパターン１２で規定されている結果と等しいか否か判断し、これにより状態遷移実行部７がアーキテクチャ・モデル８ｎと同等であるか判断する。
【００４１】
また、例えば、テスト実行部６は、自動で、テストパターン１２で規定されている状態遷移が状態遷移実行部７によって同等に実行されたか否か判断し、すべての状態遷移が同等であるか、及び、同等でない場合にはどの状態遷移において整合していないかを示すテスト実行結果データ１３を生成する。これにより、開発者Ｂ又は別の開発者は、このテスト実行結果データ１３を参照し、生成された状態遷移実行部７が正しいか否か容易に確認できる。
【００４２】
図２は、アーキテクチャ・モデル生成からテストパターン生成までの処理の一例を示すフローチャートである。
【００４３】
開発者Ａは、開発しているシステムが満たすべき要件定義にしたがって、アーキテクチャの検討を行う。ここで生成される成果物がアーキテクチャ・モデル８１（いわゆる状態遷移モデル）である。
【００４４】
ステップＳ１において、記憶装置２ａは、生成されたアーキテクチャ・モデル８１を記憶する。
【００４５】
ステップＳ２において、形式検証モデル生成部３は、記憶装置２ａに記憶されているアーキテクチャ・モデル８１に基づいて、形式検証モデル９１を生成し、この形式検証モデル９１を記憶装置２ｂに記憶する。
【００４６】
ステップＳ３において、形式検証モデル実行部４は、記憶装置２ｂに記憶されている形式検証モデル９１に基づいて、モデル検証を行い、その結果得られる検証結果データ１０１を記憶装置２ｃに記憶する。
【００４７】
モデル検証は、いわゆる形式検証とも言われ、形式検証モデル９１においてデッドロックが発生しないこと、到達し得ない状態を持たないことなどを網羅的に検証する。
【００４８】
ステップＳ４において、テストパターン生成部５は、開発者Ｃ（開発者Ａでもよい）の操作及び指定に応じて、検証結果データ１０１に含まれている初期状態とその遷移系列（イベント系列）に対して、この遷移系列が正常であるか異常であるかを示す情報を付して、テストパターン１２の一要素として記憶装置２ｄに記憶する。
【００４９】
ステップＳ５において上記処理を繰り返すか否か判断され、繰り返される場合には処理はステップＳ１に戻る。繰り返されない場合は処理を終了する。
【００５０】
例えば、アーキテクチャ・モデル８１の開発において不備がある場合には、次のアーキテクチャ・モデル８２、形式検証モデル９２、検証結果データ１０２が生成され、検証結果データ１０２に含まれている初期状態とその遷移系列に対して正常又は異常を示す情報を付したデータが、テストパターン１２の一要素として記憶装置２ｄに記憶される。そして、最終的に、形式検証された正常なアーキテクチャ・モデル８ｎ、形式検証モデル９ｎ、検証結果データ１０ｎが生成され、正常な検証結果データ１０ｎに含まれる初期状態とその遷移系列に対して正常を示す情報を付したデータが、テストパターン１２の一要素として記憶装置２ｄに記憶されるまで、ステップＳ１〜Ｓ４の処理は繰り返される。
【００５１】
このように、一般的に、アーキテクチャの開発途中で不備がある段階では、不備を反映した検証結果データ（ＮＧの検証結果）１０１〜１０ｎ-1が複数得られる。そして、アーキテクチャの開発の最後の段階では、正常な検証結果データ（ＯＫの検証結果）１０ｎが一種類得られる。
【００５２】
上記の検証結果データ１０１〜１０ｎは、上述したように、それぞれの場合の状態遷移の履歴、すなわち初期状態及び遷移系列の集合を含む。
【００５３】
なお、テストパターン生成部５は、開発者Ｃの操作及び指定に応じて、生成された複数の検証結果データ１０１〜１０ｎのうちどのデータをテストパターン１２として採用するかの指定を受け、採用する旨の指定を受けたデータをテストパターン１２の一要素として登録するとしてもよい。
【００５４】
図３は、アーキテクチャ・モデル８１（状態遷移モデル）の一例を示す図である。
【００５５】
丸で囲まれたアルファベットは、それぞれ状態を表す。状態から状態へ向かう矢印は、状態の遷移を表す。矢印に付されている数字は状態遷移を引き起こした事象（イベント）を表す。
【００５６】
図４は、検証結果データ１０１の一例を示す図である。
【００５７】
検証結果データ１０１における状態遷移履歴の記述例としては、｛Ａ，{２，３}｝などで記述できる。｛Ａ，{２，３}｝において、Ａは初期状態であり、{２，３}は状態の遷移を引き起こす事象を発生順に並べた遷移系列である。
【００５８】
図５は、本実施の形態に係るテストパターン生成部５とテスト実行部６の一例を示すブロック図である。すなわち、この図５においては、検証結果データ１０１〜１０ｎに基づいてテストパターン１２が生成されてから、テスト実行結果データ１３が生成されるまでの工程を表している。
【００５９】
また、図６は、本実施の形態に係るテスト実行部６の具体的構成の一例を示すブロック図である。
【００６０】
テストパターン生成部５は、複数のＮＧの検証結果データ１０１〜１０ｎ−１と一つのＯＫの検証結果データ１０ｎを読み出す。
【００６１】
開発者Ｃは、テストパターン生成部５を用いて、検証結果データ１０１〜１０ｎに含まれている初期状態と遷移系列について、テストパターンとしての実行時間が適切になるように、遷移系列を分割又は統合し、この初期状態と遷移系列の適用結果が正常（ＯＫ）か異常（ＮＧ）かを対応付ける（マッピングする）。
【００６２】
テストパターン生成部５は、正常で終了する初期状態と遷移系列を正常系のテストパターンの要素、異常（テストパターンで規定された遷移の系列と実際の処理系が遷移する系列とが異なる状態）で終了する初期状態と遷移系列を異常系のテストパターンの要素として体系化したテストパターン１２を生成し、記憶する。
【００６３】
テスト実行部６は、読み出し部６１、実装認識部６２、第１マッピング部６３、第２マッピング部６４、第３マッピング部６５、テスト結果生成部６６を具備する。
【００６４】
読み出し部６１は、記憶装置２ｄからテストパターン１２を読み出す。
【００６５】
実装認識部６２は、テスト対象の状態遷移実行部７（オブジェクト指向言語によって開発されたプログラムであればそのオブジェクトの状態又はメモリ上での値）が取る状態と、その状態から他の状態へ遷移する事象（割り込み、メッセージ送信、ソフトウェア・イベントなど）とを認識する。
【００６６】
第１マッピング部６３は、読み出されたテストパターン１２と実装認識部６２の認識結果とに基づいて、テストパターン１２に記述されている状態と、テスト対象の状態遷移実行部７が取る状態との対応関係を表す第１のマッピングデータ１６を生成し、この第１のマッピングデータ１６を記憶装置２ｆに記憶する。すなわち、テスト実行部６の第１マッピング部６３は、テスト対象の状態遷移実行部７の初期状態の設定を行い、テストパターン１２における状態と実装オブジェクトとのマッピングを行う。
【００６７】
第２マッピング部６４は、読み出されたテストパターン１２と実装認識部６２の認識結果とに基づいて、テストパターン１２における状態遷移を引き起こす事象がテスト対象の状態遷移実行部７のどの事象に対応するかのマッピングを行い、第２のマッピングデータ１７を記憶装置２ｇに記憶する。
【００６８】
第３マッピング部６５は、第１のマッピングデータ１６及び第２のマッピングデータ１７の設定に基づいて、テスト対象の状態遷移実行部７に対して、テストパターン１２にそった状態遷移を引き起こす事象を発生させ、テスト対象の状態遷移実行部７が遷移（移行）した状態を取得し、この遷移後の状態とテストパターン１２の最終の遷移状態とを比較するために対応付けるマッピングを行い、この結果得られる第３のマッピングデータ１８を記憶装置２ｈに記憶する。すなわち、テスト実行部６の第３マッピング部６５は、テスト対象の状態遷移実行部７がテストパターン１２を実行して最後に遷移した状態（オブジェクトの状態、メモリの状態など）を取得し、この取得した状態をテストパターン１２で期待された状態と比較するためのマッピングを行う。
【００６９】
なお、本実施の形態において、これらのマッピングは、テスト実行部６によって自動的に行われるが、開発者Ｂなどによってマッピングが行われ、テスト実行部６は、開発者Ｂによって与えられたマッピングデータを利用するとしてもよい。
【００７０】
そして、テスト結果生成部６６は、第３のマッピングデータ１８に基づいて、テスト対象の状態遷移実行部７の実装が遷移（移行）した状態と、テストパターン１２の遷移状態とを比較し、状態遷移実行部７でアーキテクチャ・モデル８１と同等の遷移が行われたか否かを判断した結果を示すテスト実行結果データ１３を記憶装置２ｅに記憶する。なお、テスト実行結果データ１３には、第３のマッピングデータ１８が含まれており、開発者Ｂは、テスト実行結果データ１３を出力装置１５から出力し、第３のマッピングデータ１８の内容を検討することができるとしてもよい。
【００７１】
以上説明した本実施の形態は、形式検証技術を用いてシステムのソフトウェア・アーキテクチャの開発を行う場合の、アーキテクチャが満たすべき制約条件を満たしているか検証を行うための形式検証モデルの検証、及び、シミュレーション実行可能な形式検証モデル実行部４（例えばＳＰＩＮ）を備えたシステム開発支援環境に適用される。
【００７２】
本実施の形態に係るシステム開発支援装置１は、シミュレーション実行結果（検証がＮＧであった場合とＯＫの場合とを含む）に基づいてテストパターン１２を生成するテストパターン生成部５と、システムの振舞いが実装された状態遷移実行部７に対してテストパターン１２にしたがったテストを実行するテスト実行部６とを具備する。
【００７３】
本実施の形態に係るシステム開発支援装置１を用いて確認を行うことにより、検証によって正常とされたアーキテクチャ・モデル８ｎで規定された状態遷移が、開発された状態遷移実行部７によって実行可能であることを保障することができる。
【００７４】
本実施の形態において、開発者は、検証されたアーキテクチャ・モデル８ｎで規定された状態遷移が、開発対象のシステムの実行環境で実現されているか容易に判断可能である。
【００７５】
本実施の形態においては、形式検証されたソフトウェア・アーキテクチャに基づいてシステムを設計／実装する場合の信頼性を確保することができる。すなわち、本実施の形態においては、上流工程で開発されたソフトウェア・アーキテクチャに基づいてシステムの設計／実装を詳細化していく場合に、設計／実装がソフトウェア・アーキテクチャに基づいて開発されていることを、高い信頼性で確認することができる。
【００７６】
なお、本実施の形態において、各種の構成要素は自由に組み合わせ又は分離することができる。例えば、各記憶装置２ａ〜２ｈは、自由に組み合わせることができ、また分割することもできる。
【００７７】
本実施の形態において、状態遷移実行部７は、例えば、システムとして振舞うべき状態遷移記述が定義されており、この状態遷移記述にしたがってシステムの状態を遷移させる状態遷移記述解釈実行部であるとしてもよい。
【００７８】
本実施の形態に係るシステム開発支援装置１は、図７に示すように、コンピュータ２１によって実現されるとしてもよい。例えば、コンピュータ２１は、プロセッサ２２、記憶装置２、入力装置１４、出力装置１５を具備する。プロセッサ２２は、記録媒体１９のプログラム２０を読み出して実行する。記憶装置２は、上記記憶装置２ａ〜２ｈとして利用される。
【符号の説明】
【００７９】
１…システム開発支援装置、２，２ａ〜２ｈ…記憶装置、３…形式検証モデル生成部、４…形式検証モデル実行部、５…テストパターン生成部、６…テスト実行部、７…状態遷移実行部、８１〜８ｎ…アーキテクチャ・モデル、９１〜９ｎ…形式検証モデル、１０１〜１０ｎ…検証結果データ、１２…テストパターン、１３…テスト実行結果データ、１４…入力装置、１５…出力装置、１６…第１のマッピングデータ、１７…第２のマッピングデータ、１８…第３のマッピングデータ、１９…記録媒体、２０…プログラム、２１…コンピュータ、２２…プロセッサ
【特許請求の範囲】
【請求項１】
アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを記憶する第１の記憶手段と、
前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識する実装認識手段と、
前記第１の記憶手段に記憶されているテストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成する第１のマッピング手段と、
前記第１の記憶手段に記憶されているテストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成する第２のマッピング手段と、
前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶する第３マッピング手段と、
前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶するテスト結果生成手段と
を具備するシステム開発支援装置。
【請求項２】
請求項１記載のシステム開発支援装置において、
前記状態遷移実行手段は、開発されるシステムとして振舞うべき状態遷移記述が定義されており、当該記述にしたがって前記システムの状態を遷移させる状態遷移記述解釈実行手段であることを特徴とするシステム開発支援装置。
【請求項３】
請求項１又は請求項２記載のシステム開発支援装置において、
前記テスト結果生成手段は、前記第３のマッピングデータに基づいて、テストパターン１２にそった状態遷移が、前記状態遷移実行手段によって正当に実行されたか否かの判断結果を含み、正当に実行されていないと判断された場合に、正当に実行されていない部分を指定する異常部分情報を含む前記テスト実行結果データを生成することを特徴とするシステム開発支援装置。
【請求項４】
請求項１乃至請求項３のいずれか１項に記載のシステム開発支援装置において、
形式検証技術を用いて前記アーキテクチャ・モデルが制約条件を満たしているか検証を行い、形式検証モデルの検証及びシミュレーションを実行した結果を示す検証結果データを生成し、当該検証結果データを第４の記憶手段に記憶する形式検証モデル実行手段と、
前記第４の記憶手段に記憶されている検証結果データをユーザに対して出力し、この検証結果データに含まれている前記第１の状態と前記第１の遷移系列とに対する正常又は異常を示す情報を前記ユーザから入力し、当該入力された情報を前記第１の状態と前記第１の遷移系列とに付した前記テストパターンを生成し、前記テストパターンを前記第１の記憶手段に記憶するテストパターン生成手段と
をさらに具備することを特徴とするシステム開発支援装置。
【請求項５】
コンピュータを、
第１の記憶手段から、アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを読み出す手段、
前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識する実装認識手段、
前記テストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成する第１のマッピング手段、
前記テストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成する第２のマッピング手段、
前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶する第３マッピング手段、
前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶するテスト結果生成手段
として機能させるためのプログラム。
【請求項６】
コンピュータによって実現されるシステム開発支援方法において、
前記コンピュータは、アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを第１の記憶手段に記憶し、
前記コンピュータは、前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識し、
前記コンピュータは、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成し、
前記コンピュータは、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成し、
前記コンピュータは、前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶し、
前記コンピュータは、前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶する
ことを特徴とするシステム開発支援方法。
【請求項１】
アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを記憶する第１の記憶手段と、
前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識する実装認識手段と、
前記第１の記憶手段に記憶されているテストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成する第１のマッピング手段と、
前記第１の記憶手段に記憶されているテストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成する第２のマッピング手段と、
前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶する第３マッピング手段と、
前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶するテスト結果生成手段と
を具備するシステム開発支援装置。
【請求項２】
請求項１記載のシステム開発支援装置において、
前記状態遷移実行手段は、開発されるシステムとして振舞うべき状態遷移記述が定義されており、当該記述にしたがって前記システムの状態を遷移させる状態遷移記述解釈実行手段であることを特徴とするシステム開発支援装置。
【請求項３】
請求項１又は請求項２記載のシステム開発支援装置において、
前記テスト結果生成手段は、前記第３のマッピングデータに基づいて、テストパターン１２にそった状態遷移が、前記状態遷移実行手段によって正当に実行されたか否かの判断結果を含み、正当に実行されていないと判断された場合に、正当に実行されていない部分を指定する異常部分情報を含む前記テスト実行結果データを生成することを特徴とするシステム開発支援装置。
【請求項４】
請求項１乃至請求項３のいずれか１項に記載のシステム開発支援装置において、
形式検証技術を用いて前記アーキテクチャ・モデルが制約条件を満たしているか検証を行い、形式検証モデルの検証及びシミュレーションを実行した結果を示す検証結果データを生成し、当該検証結果データを第４の記憶手段に記憶する形式検証モデル実行手段と、
前記第４の記憶手段に記憶されている検証結果データをユーザに対して出力し、この検証結果データに含まれている前記第１の状態と前記第１の遷移系列とに対する正常又は異常を示す情報を前記ユーザから入力し、当該入力された情報を前記第１の状態と前記第１の遷移系列とに付した前記テストパターンを生成し、前記テストパターンを前記第１の記憶手段に記憶するテストパターン生成手段と
をさらに具備することを特徴とするシステム開発支援装置。
【請求項５】
コンピュータを、
第１の記憶手段から、アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを読み出す手段、
前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識する実装認識手段、
前記テストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成する第１のマッピング手段、
前記テストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成する第２のマッピング手段、
前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶する第３マッピング手段、
前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶するテスト結果生成手段
として機能させるためのプログラム。
【請求項６】
コンピュータによって実現されるシステム開発支援方法において、
前記コンピュータは、アーキテクチャ・モデルに対する形式検証結果に含まれている「第１の状態とこの第１の状態からの状態遷移を示す第１の遷移系列」とに対して、正常又は異常を示す情報を付したテストパターンを第１の記憶手段に記憶し、
前記コンピュータは、前記アーキテクチャ・モデルにそって生成されたテスト対象の状態遷移実行手段における「第２の状態とこの第２の状態からの状態遷移を示す第２の遷移系列」とを認識し、
前記コンピュータは、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の状態と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の状態とを対応付けた第１のマッピングデータを生成し、
前記コンピュータは、前記第１の記憶手段に記憶されているテストパターンに含まれている第１の遷移系列の事象と、前記実装認識手段よって認識された前記状態遷移実行手段における第２の遷移系列の事象とを対応付けた第２のマッピングデータを生成し、
前記コンピュータは、前記第１のマッピングデータ及び前記第２のマッピングデータに基づいて、前記状態遷移実行手段に対して、前記テストパターン１２にそった状態遷移を引き起こす事象を発生させ、前記状態遷移実行手段が遷移した結果と、前記テストパターン１２の遷移結果とを対応付けた第３のマッピングデータを生成し、前記第３のマッピングデータを第２の記憶手段に記憶し、
前記コンピュータは、前記第２の記憶手段に記憶されている第３のマッピングデータに基づいて、テスト実行結果を示すテスト実行結果データを生成し、前記テスト実行結果データを第３の記憶手段に記憶する
ことを特徴とするシステム開発支援方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【公開番号】特開２０１１−２４２８８８（Ｐ２０１１−２４２８８８Ａ）
【公開日】平成２３年１２月１日（２０１１．１２．１）
【国際特許分類】
【出願番号】特願２０１０−１１２４８６（Ｐ２０１０−１１２４８６）
【出願日】平成２２年５月１４日（２０１０．５．１４）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【出願人】（３０１０６３４９６）東芝ソリューション株式会社 (1,478)
【Ｆターム（参考）】
【公開日】平成２３年１２月１日（２０１１．１２．１）
【国際特許分類】
【出願日】平成２２年５月１４日（２０１０．５．１４）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【出願人】（３０１０６３４９６）東芝ソリューション株式会社 (1,478)
【Ｆターム（参考）】
[ Back to top ]