Verification Tool and Unified Specifications for Embedded Software

In the extended abstract, our on-going research project Verification Tool and Unified Specifications for Embedded Software is explained. In the project, we are developing an upper-process support tool that helps ones formalize specifications of embedded software and verify a certain type of consistency and correctness unless formal method background is equipped. The tool is based on a proof assistant system (Agda) and a software development system (VDM tools), but is designed with the concept of lightweight formal methods. The project is being promoted as joint research with CSK systems West Japan, CSK systems and Macs co. ltd, under the program of the Ministry of Economy, Trade and Industry.