Vol.3 No.3 2010

25/84

研究論文:複雑システムの信頼性を向上させる開発手法(加藤ほか)−201−Synthesiology Vol.3 No.3(2010)用するモデル検査ツールの表現形式に従い、検査対象となるシステムの仕様などを基に、検査対象の状態遷移をモデル化する。次に、検査対象が満たすべき性質を検討する。適用するモデル検査ツールの表現形式に従い、性質を表す検査式を作成する。そして、計算機上のモデル検査ツールに対して、モデルと検査式を入力し、モデル検査を実施する。モデル検査では、モデルが実現しうるすべての状態遷移において、検査式で表現する性質をモデルが満足するか否かを網羅的に検証する。最後に、モデル検査の出力結果を基に、検査式で表現する性質とモデルとの適合結果を分析する。モデルに対して検査式が適合する場合、それはモデルの基になった仕様が性質を満足することを意味する。モデルに対して検査式が適合しない場合、反例として性質が成り立たない条件に至るまでのモデルの状態遷移が出力される。反例を分析し、モデルに誤りがない場合、モデルの基になった検査対象の仕様に誤りがあることを意味する。モデル検査を適用することにより、次に示す二つの効果が期待できる。一つ目は、反例を用いることで、仕様の誤りを検出する際の工数を削減できる可能性がある。テスト手法やシミュレーション手法を適用し、確認内容が不適合となった場合、不適合に結びつく原因を複数仮定し、原因を分析する必要がある。その際に原因特定までに大きな労力を要することがある。モデル検査を適用する場合、自動で出力される反例を用いて不適合の発生過程を遡ることができる。それにより、不適合を引き起こす原因を効率よく特定することが可能である。二つ目は、モデル検査を実施する場合、モデル化という仕様の形式化を通して、検査対象である仕様の誤りを検出できる可能性がある。4 技術の融合アーキテクチャ設計手法とモデル検査について、それぞれの技術の特徴を活かしながら融合し、この研究における開発手法を構築する。本章では、この研究の開発手法における作業フローを詳述することで、アーキテクチャ設計手法とモデル検査を融合するプロセスを示す。4.1 提案する開発手法図6に、アーキテクチャ設計手法とモデル検査を融合したこの研究で提案する開発手法を示す。本開発手法は、アーキテクチャ設計、モデル検査、それら二つを繋ぐブリッジ技術用語23で構成される。まず、本開発手法のインプットとして、システム仕様を入力する。システム仕様を基に、IEEE 1220に従い、機能設計および物理設計を含むアーキテクチャ設計を実施する。アーキテクチャ設計を実施することで、システム仕様を構成要素の仕様および構成要素間のインタフェース仕様に分解する(図6の左上における破線の仕様)。また、アーキテクチャ設計の過程において、IEEE 1220で規定されるトレーサビリティマトリクス用語24を作成する。図7にトレーサビリティマトリクスを示す。システムの仕様および構成要素の仕様には、仕様の一つ一つに項番が付与される。トレーサビリティマトリクスには、システム仕様とそれをブレークダウンした構成要素仕様との対応関係がまとめられる。次に、構成要素の仕様、構成要素間のインタフェース仕様、トレーサビリティマトリクス、システム仕様に対し、こ入力開発手法協調動作の不整合トレーサビリティマトリクス構成要素B仕様ブリッジ技術構成要素間インタフェース仕様構成要素A仕様アーキテクチャ設計システム仕様構成要素A協調動作仕様構成要素B協調動作仕様構成要素間インタフェース協調動作仕様満たすべき性質性質を満足しない場合性質を満足する場合協調動作の整合性確認済構成要素A仕様構成要素B仕様構成要素間インタフェース仕様作業フロー出力モデル検査モデル検査ツールリリース5.3 ZB機能5.2 YB機能5.1 XB機能5.1 XA機能5.2 YA1機能5.3 YA2機能4.3 Z機能4.2 Y機能4.1 X機能4.3 Z機能4.2 Y機能4.1 X機能システム仕様-構成要素B仕様トレーサビリティマトリクスシステム仕様-構成要素A仕様トレーサビリティマトリクス5.1 XB機能5.2 YB機能5.3 ZB機能4.1 X機能4.2 Y機能4.3 Z機能構成要素B仕様システム仕様N/A5.3 YA2機能5.2 YA1機能5.1 XA機能構成要素A仕様システム仕様構成要素B仕様構成要素A仕様システム仕様6図 6 この研究における開発手法図 7 トレーサビリティマトリクス

※このページを正しく表示するにはFlashPlayer9以上が必要です