Engineering CASE tools to support formal methods for real-time software development

摘要

A prototype toolset that provides comprehensive support for constructing verifiably correct real-time systems is described. The toolset supports the development of specifications in the graphical Modechart language and several methods for improving the correctness of the specifications, including formal verification, simulation, and consistency and completeness checking. An engineering approach for developing the toolset is presented that integrates software engineering principles, prototyping, and early and continued focus on user interface design. Contributions that the toolset effort makes to computer-aided software engineering (CASE) support for formal methods are summarized.