Component-based Algebraic Specification and Verification in
back to Selected Publications
- We present a formal method for component-based system
specification and verification which is based on the new algebraic
specification language CafeOBJ, which is a modern successor of OBJ
incorporating several new developments in algebraic specification
theory and practice.
- We first give an overview of the origins and of the main
features of CafeOBJ, including its logical foundations, and then we
- the behavioural specification paradigm in CafeOBJ, surveying the
object-oriented CafeOBJ specification and verification methodology
based on behavioural abstraction.
- The last part of this paper further focuses on a component-based
behavioural specification and verification methodology which
features high reusability of both specification code and
verification proof scores. This methodology constitutes the basis
for an industrial strength formal method around CafeOBJ.