OTS/CafeOBJ法に基づく並行システムの実装とテスト生成

摘要

形式仕様によるシステムの記述と、プログラミング言語によるソフトウェアの実装には隔たりがあるが、これを克服するために、筆者らは形式仕様の検証を元にテストスイートを生成し、テスト駆動による開発へ持ち込む手法を提案している。本稿では、提案済みの手法を発展させ、形式仕様を元に複数のオブジェクトから成る実装や並行実行を意識した実装を得る手法と、そのコードをテストするテストスイートの生成手法を提案する。