Formal methods software engineering for the CARA system

This paper discusses the application of formal methods software engineering (FMSE) to the development of the Computer Automated Resuscitation A (CARA) medical device at Walter Reed Army Institute of Research. Because this system is potentially life critical, a high level of quality was required. A formal engineering approach to the software development activities was chosen to satisfy this need. Specifically, a technique called sequence enumeration was applied to elicit and refine requirements while deriving a formal specification. The fundamentals of the specification process that was used on the project are described along with a brief summary of the project experience in the development and testing phases. The project employed recent advances in Cleanroom software engineering methods along with older box-structured development and usage-model-based statistical testing techniques. © 2003 Springer-Verlag.