抄録
CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.
The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the OBJ language, and behavioral, rewriting, and parameterized specifications can be written in it. The CafeOBJ language system can simulate equational reasoning by executing equations as rewrite rules, and be used as an interactive verification system. This first tutorial presents an overview of the CafeOBJ formal method by using an example of "mutual exclusion protocol with a waiting queue" without getting into details of the language and the verification technique. In the following tutorials, the language and its semantics (2nd tutorial), equational reasoning and term rewriting systems (3rd tutorial) are presented, and the CafeOBJ's verification method with proof scores which only uses reductions (4th tutorial) is explained. Furthermore, CafeOBJ's verifications of an authentication protocol (5th tutorial) and a communication protocol (6th tutorial) are also presented, and several verification techniques are explained.
