モデル検査は分散システムなどの複雑なシステムの開発において，その基本設計に誤りがないことを確かめるために用いられる．
モデル検査を取り入れたシステム開発では，保証された正しさを保ちつつシステムを実装することが求められる．
しかし，モデル記述言語と実装言語間のギャップによりこれは容易ではなく，モデル記述言語から実装言語への自動変換を行うツールは有用である．
そこで本研究では，共に並行システムの記述を得意とする，モデル記述言語PROMELAからプログラミング言語Erlangへの自動変換ツールを設計した．
本発表では本ツールの設計およびプロトタイプ実装について述べ有効性を考察する．