@article{oai:uec.repo.nii.ac.jp:00009105,
 author = {田原, 康之 and Tahara, Yasuyuki and 吉岡, 信和 and Yoshioka, Nobukazu and 大須賀, 昭彦 and Ohsuga, Akihiko and 本位田, 真一 and Honiden, Shinichi},
 issue = {2},
 journal = {情報処理学会論文誌},
 month = {Feb},
 note = {インターネットやイントラネットなどの広域開放型ネットワークが普及するにつれて，Webサービスやエージェントといった，開放型ネットワーク環境を有効に活用するための分散システム開発技術が急速に進展している．一方，その急速な発展のため，これらの技術を用いて実際の開発を行う際に，このような大規模かつ複雑なシステムが，機能やセキュリティなどに関し，要求仕様を満足しているかどうかを確認することが困難になってきている．従来このような問題を解決するための最も有効な技術の1 つとして，モデル検査手法などの形式的検証技術があるが，実適用は現在でも容易ではない．本論文では，分散システム開発において，視覚的な支援により，モデル検査の適用を容易にする手法を提案する．本手法では，開発ツールIPEditorで作成した視覚的モデルに対し，その形式的表現を与え，そのモデルからモデル検査ツールSPINが検証の対象とするPromelaプログラムの一部を自動的に生成する．これにより，開発者は記述が困難なPromelaプログラムの全体を直接記述しなくても，IPEditorにより理解が容易な視覚的モデルを作成することにより，SPINツールを利用したモデル検査を用意に実施することができる．, As wide-area open networks like the Internet and intranets grow larger, various technology of distributed system development is rapidly emerging such as the Web service technology and the agent technology. On the other hand, the growth is so rapid that people are reporting a number of difficulties in actually operating practical systems such as management of complexity, poor flexibility to cope with frequent changes of requirements and environments, and security issues. Although the vendors are considering such difficulties, one of the most effective techniques is still in an early stage of research, that is, formal verification including model checking. Application of formal verification techniques is thought of as difficult because it is not easy to create models to verify. In this paper, we propose a method that visually supports model checking and development of distributed systems. Our technique realizes integration of visual modeling and model checking by providing formal representations of the visual models and a procedure of generation of a part of Promela programs that are formal models for the model checking tool SPIN. We can create the visual models using IPEditor, a development support tool for multi-agent applications originally and also applicable to other technologies including Web services. Thus the developer do not have to describe the entire Promela programs directly and therefore easily use SPIN in system development. We demonstrate the advantage of our method with an example of mutual exclusion.},
 pages = {459--469},
 title = {分散システム開発におけるモデル検査への視覚的支援手法},
 volume = {46},
 year = {2005},
 yomi = {タハラ, ヤスユキ and ヨシオカ, ノブカズ and オオスガ, アキヒコ and ホンイデン, シンイチ}
}