Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
Peter Lindsay , The University of Queensland
David Hemer , The University of Queensland
The CARE project investigated integration of well-understood formal development principles into an industrial organization'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. This paper illustrates the method on part of the development of a software module for logging events in a medical embedded device.
formal methods, program development, software verification, refinement
D. Hemer and P. Lindsay, "Using CARE to Construct Verified Software," Formal Engineering Methods, International Conference on(ICFEM), Hiroshima, JAPAN, 1997, pp. 122.