◎坂本　統・和崎克己（信州大）

メッセージ交換プロトコルのモデル検査を行うため，上流設計としてUMLを 用いてモデル化を行い，モデル検査器SPIN向けコードの自動生成を行った．具体的には，UMLコ ミュニケーション図を用いて，ノード間の接続状態を有向グラフで表現し，図要素に紐付けたUMLステートマシン図の情報と結合することで，プロトコルとネットワーク全体の設計レビュー，並びに網羅的な検査 を行う．特に通信路のタイムアウト機構を導入することで，時間経過による処理の振る舞い記述に対応させた．接続チャンネル数を変数Nで抽象化した上，タグ付け値を利用して要素拡張を行い，自動変換時にスケーラブルな状態値決定が出来るように 工夫した．