Current Research

Software Development with Formal Specification

OUTLINE

We are engaged in the research of software development using formal specification description. In particular, we have been researching a method of efficiently developing software with high reliability using algebraic specification, which is one kind of formal specification. Strict specification can be described by using algebraic specification, but description and comprehension take time, and acquisition is difficult. Therefore, it is necessary to improve the facility of description and the comprehension of algebraic specification.

TOPICS

We are currently researching the support of software porting using algebraic specification. Computer systems have started to be used in various platforms, and much work to port one set of software to various platforms is being done. To use the software operated in a certain environment in a different environment, modification is required based on the environment. To shorten the computer system's development period and to decrease development cost, cost reduction of software porting is needed. Our research aims to achieve an efficient porting support environment. Using algebraic specification, this method can be expected to reduce software porting cost and improve the development speed of software systems. When the platform changes, software specifications should change the part that depends on the platform. In this technique, porting is supported by using platform and software specifications. Both specifications are described algebraically. The API specification, the parameter limitations of the differences between hardware, etc. are described in platform specifications. Porting that holds the correspondence becomes possible because it uses an algebraic specification description method for both the software and platform specifications. It only has to prepare a platform specification for each platform once. The procedure follows for porting software specifications developed by using this technique's porting support environment on a certain platform and the program to another platform. The procedure of porting by this technique is as follows.

• Extraction of platform specification differences
• Automatic change in software specifications based on platform specification differences
• Generation of program templates from software specifications and program differences

FUTURE WORK

Contradiction might be caused when porting software to another platform even if intended to be platform-independent. Establishing a method for detecting contradiction on specifications is necessary.