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

摘要

In software developments with formal methods, there exists an unavoidable gap between a system description in formal specification languages and a system implementation in programming languages. In our previous work, we have proposed a method to generate test suites from verification results of a formal specification for the test driven development. In this work, we extend our method and apply it to concurrent systems whose implementations consist of several objects which work concurrently.%形式仕様によるシステムの記述と、プログラミング言語によるソフトウェアの実装には隔たりがあるが、これを克服するために、筆者らは形式仕様の検証を元にテストスイートを生成し、テスト駆動による開発へ持ち込む手法を提案している。本稿では、提案済みの手法を発展させ、形式仕様を元に複数のオブジェクトから成る実装や並行実行を意識した実装を得る手法と、そのコードをテストするテストスイートの生成手法を提案する。