A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method |
| |
Authors: | Takahiro Seino Kazuhiro Ogata Kokichi Futatsugi |
| |
Affiliation: | Japan Advanced Institute of Science and Technology (JAIST);NEC Software Hokuriku, Ltd. / JAIST;Japan Advanced Institute of Science and Technology (JAIST) |
| |
Abstract: | The OTS/CafeOBJ method can be used to model, specify and verify distributed systems. Specifications are written in equations, which are regarded as rewrite rules and used to verify specifications. The usefulness of the method is demonstrated by applying the method to nontrivial problems such as electronic commerce protocols and railroad signaling systems. In this paper we describe a toolkit called Buffet, which assists verification in the method. Given predicates used to split cases and lemmas, Buffet automatically generates proofs (called proof scores) and checks the proof scores using the CafeOBJ system. Buffet also has facilities to display proof scores generated and verification results on a web browser. |
| |
Keywords: | Algebraic specification CafeOBJ observational transition system proof scores verification |
本文献已被 ScienceDirect 等数据库收录! |