Using CARE to construct verified software

Author

Lindsay, Peter ; Hemer, David

Author_Institution

Sch. of Inf. Technol., Queensland Univ., Australia

fYear

1997

fDate

12-14 Nov. 1997

Firstpage

122

Lastpage

131

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on

Conference_Location

Hiroshima, Japan

Print_ISBN

0-8186-8002-4

Type

conf

DOI

10.1109/ICFEM.1997.630417

Filename

630417