A Study on Verification of Software Components in Object-Based Distributed Environments

我们已经开发了基础技术，通过这些技术，我们可以正式地验证给定的组件是否符合它们的规范，以及支持这些技术的软件工具。在未来几年里，为软件行业开发这样的技术是必要的。我们使用了CafeOBJ，这是一种代数规范语言和系统，具有多种功能，可以将规范编写为组件。CafeOBJ也适用于抽象机器和抽象数据类型，并提供强大的模块功能。本研究的一些具体成果如下：1。一个定理证明器的设计与开发：将求解CafeOBJ一阶谓词公式项的解析引擎PigNose集成到CafeOBJ系统中。我们通过实例验证了它的有效性。2. 基于油品组件的开发方法：将软件组件组合在一起，为开发高保证的软件奠定了基础。3. 验证案例研究：将基于CafeOBJ的验证方法应用于铁路信号系统、安防系统等多个可靠系统，验证了其有效性。

We have developed base technologies with which we can formally verify that given components meet their specifications and the software tool supporting the technologies. It will be necessary to develop such technologies for the software industry in the coming years. We have used CafeOBJ, an algebraic specification language and system, with a variety of functionalities that make is possible to write specifications as components. CafeOBJ is also suitable for abstract machines as well as abstract data types, and provides strong module facilities. Some concrete outcomes in this study are as follows : 1. Design and development of a theorem prover : the resolution engine PigNose that resolves CafeOBJ term denoting first-order predicate formulas has been incorporated into the CafeOBJ system. We have confirmed its usefulness by applying it to some examples. 2. Development methodology based oil components : we have made foundation for developing high-assurance software by putting together software components. 3. Verification case studies : we have applied the verification method based on CafeOBJ to several reliable systems such as railroad signaling systems and security systems and confirmed its usefulness.