Title :
Engineering CASE tools to support formal methods for real-time software development
Author :
Heitmeyer, C.L. ; Labaw, B.G. ; Clements, P.C. ; Mok, A.K.
Author_Institution :
US Naval Res. Lab., Washington, DC, USA
Abstract :
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
Keywords :
formal specification; formal verification; real-time systems; software prototyping; software tools; user interfaces; completeness checking; computer-aided software engineering; consistency; engineering CASE tools; formal verification; graphical Modechart language; prototype toolset; prototyping; simulation; specifications; user interface design; verifiably correct real-time systems; Computer aided software engineering; Delay effects; Design engineering; Laboratories; Programming; Prototypes; Real time systems; Software prototyping; Timing; User interfaces;
Conference_Titel :
Computer-Aided Software Engineering, 1992. Proceedings., Fifth International Workshop on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-8186-2960-6
DOI :
10.1109/CASE.1992.200138
