分散システム開発におけるモデル検査への視覚的支援手法(プロトコルと開発ツール)(<特集>新時代の分散処理とネットワーク(WebサービスとP2P))

概要

論文の詳細を見る
インターネットやイントラネットなどの広域開放型ネットワークが普及するにつれて, Webサービスやエージェントといった, 開放型ネットワーク環境を有効に活用するための分散システム開発技術が急速に進展している.一方, その急速な発展のため, これらの技術を用いて実際の開発を行う際に, このような大規模かつ複雑なシステムが, 機能やセキュリティなどに関し, 要求仕様を満足しているかどうかを確認することが困難になってきている.従来このような問題を解決するための最も有効な技術の1つとして, モデル検査手法などの形式的検証技術があるが, 実適用は現在でも容易ではない.本論文では, 分散システム開発において, 視覚的な支援により, モデル検査の適用を容易にする手法を提案する.本手法では, 開発ツールIPEditorで作成した視覚的モデルに対し, その形式的表現を与え, そのモデルからモデル検査ツールSPINが検証の対象とするPromelaプログラムの一部を自動的に生成する.これにより, 開発者は記述が困難なPromelaプログラムの全体を直接記述しなくても, IPEditorにより理解が容易な視覚的モデルを作成することにより, SPINツールを利用したモデル検査を用意に実施することができる.
2005-02-15

分散システム開発におけるモデル検査への視覚的支援手法(プロトコルと開発ツール)(<特集>新時代の分散処理とネットワーク(WebサービスとP2P))

スポンサーリンク

概要

著者

関連論文

スポンサーリンク