Title :
Using CARE to construct verified software
Author :
Lindsay, Peter ; Hemer, David
Author_Institution :
Sch. of Inf. Technol., Queensland Univ., Australia
Abstract :
The CARE project investigated integration of well understood formal development principles into an industrial organisation´s software development methodology. The result was a method for construction and verification of programs from formal specifications, using libraries of pre proven, formally specified components. Tools help the user build products by selecting and instantiating components to fit the problem at hand and generating and discharging correctness of fit proof obligations. The paper illustrates the method on part of the development of a software module for logging events in a medical embedded device.
Keywords :
biomedical equipment; formal specification; medical computing; program verification; software libraries; CARE project; correctness of fit proof obligations; formal development principles; formal specifications; formally specified components; industrial organisation; medical embedded device; program development; program verification; software development methodology; verified software; Collaboration; Collaborative software; Computer industry; Formal specifications; Formal verification; Hardware; Information technology; Programming; Refining; Software libraries;
Conference_Titel :
Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on
Conference_Location :
Hiroshima, Japan
Print_ISBN :
0-8186-8002-4
DOI :
10.1109/ICFEM.1997.630417
