Development of Formal Specification Language for Writing Specifications as Components Based on Functions

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

In this research, we have used the specification language CafeOBJ having several machineries for writing specifications as components. CafeOBJ is the algebraic specification language that has been developed by mainly the head investigator. It can be used to spepify objects in object-orientation and abstract machines as well as abstract data types. The powerful module system that CafeOBJ has also helps write specifications as components.What we have done are as follows :Verification : Safety critical systems affecting human lives such as railroad signaling systems, air-traffic control systems, patient monitoring systems, etc. are typically distributed (real-time) systems. We have developed and proposed a method for verifying those systems with the help of the CafeOBJ system. Several case studies that we have done show its usefulness.Support Tool : We have developed a foundation for developing, reliable software by combining components. We have also designed and implemented a support tool for making software according to the foundation