モデル検査は検査の対象となる仕様の振る舞いにおいて，モデルが初期状態から取りうる状態を自動的に網羅し，調べる技術である．そこで，モデル検査ツールSPINを使用して検査する対象のモデルをUML図で記述する．UMLはソフトウェア開発において，データの構造や処理の流れなどを図示するための記法を定めたものである．本研究では提案手法として，分散システムの一つであるリーダー選挙問題を対象とし，SPINの記述言語であるPROMELAの通信チャネル記述方法に変更を加え，合成構造図とステートマシン図を使用して記述した．さらに，UMLモデリングツールastah*とSPINを連携させるプラグインの実装を行った．