2K-2
モデル検査ツールUPPAALで検証したシステムの性質を満たしたJAVAソースコードの自動生成
○山根光裕,田辺 誠(宇部高専)
複数のプロセスが同時に動作する並行システムの安全性を保証することは難しく、コストがかかる。この問題を解決するために時間的制約を伴うモデル検査を視覚的に行うUPPAALというツールが存在する。これを用いることで、開発する対象のシステムの安全性を検証することが出来る。

しかし、検査した性質を満たしたままのソースコードを開発するのは難しく、
コストがかかる。誤解や記述ミスといったヒューマンエラーが発生する可能性があるからである。
そこで、Uppaalで作成したモデルと同じ動作を行うJavaソースコードを生成する変換システムを作成した。これにより、検査した性質を満たしたソースコードの実装が可能となり、コードの修正・追加も容易に行うことができる。