Component-Based Algebraic Specification and Verification in CafeOBJ
Component-Based Algebraic Specification and Verification in CafeOBJ
复制标题
CafeOBJ 中基于组件的代数规范和验证
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
S. Iida
中科院分区：
文献类型：
--
作者：
R. Diaconescu;K. Futatsugi;S. Iida
我们提出了一种基于组件的系统规范和验证的形式方法，该方法基于新的代数规范语言Cafeobj，该语言是OBJ的现代继任者，该后继者纳入了代数规范理论和实践中的几个新发展。
我们首先概述了Cafeobj的主要特征，包括其逻辑基础，然后我们专注于Cafeobj中的行为规范范式，调查了面向对象的CAFEOBJ规范和基于行为抽象的验证方法。
本文的最后一部分进一步关注基于组件的行为规范和验证方法，该方法具有规范代码和验证证明分数的高可重复性。这种方法构成了Cafeobj围绕Cafeobj的工业实力形式方法的基础。
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 main features of CafeOBJ, including its logical foundations, and then we focus on 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.