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

点击翻译按钮获取中文摘要

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.