ECFSMモデルの通信プロトコルへの故障耐性機能の半自動生成

概要

論文の詳細を見る
通信システムにフォールトが生じた時、システム自身でフォールトから回復できるということは重要なことである。このような機能のことをself-stabilizingと呼ぶ。しかし、大規模な通信システムの構築において、最初からself-stabilizingの機能を含むプロトコルを設計することは難しい。そこで、安全性が保証されているプロトコルを、self-stabilizingの機能を含むように拡張することは有効な方法だと思われる。多くの通信プロトコルの仕様は、拡張有限状態機械(ECFSM)としてモデル化される。ECFSMの安全性を検証する方法は、文献[1]において提案されている。また、self-stabilizing については、文献[2]において記述されている。本稿では、フォールトが生じないという前提の下で安全性が保証されたECFSMの部分クラスであるカウンタ付FSM(FSM-C)でモデル化された通信プロトコルを基に、それをself-stabilizingの機能を含むプロトコルに半自動的に拡張する方法を提案する。
一般社団法人情報処理学会の論文
1995-09-20