 |
|
Application name:
Data logger for an implantable medical device
Organisation:
Telectronics Pacing Systems and SVRC (University of Queensland)
Method:
CARE
Tools:
CARE system
Domain:
Medical embedded devices
Period:
January 1995 - March 1995
Size:
1 Person-month (approximately).
Description:
CARE is a method and tool-set for the development of formally verified source code from formal specifications. CARE has been developed through a collaboration between Telectronics Pacing Systems, a large Sydney-based company that develops implantable medical devices such as pace-makers and defibrillators, and the Software Verification Research Centre (SVRC) at the University of Queensland in Australia.
The use of CARE begins after system requirements have been defined and analysed for criticality, and after software requirements have been mathematically modelled by writing a formal specification. Starting with the formal specification, software engineers use CARE to develop compilable code, with integrated checking that the code is provably correct. The process of developing software using CARE involves selecting `refinements' from a library of pre-proven `templates' and adapting them to suit the problem at hand. A substantial library of basic refinements is supplied with the CARE toolset. CARE tools then help the user build products by selecting and instantiating refinements to fit the problem at hand, and generating and discharging correctness-of-fit proof obligations.
As a case study, CARE has been applied to a software module for logging events, based on an existing Telectronics device. The module was specified in Z, then CARE was used to describe and verify the design and implementation, and executable C code was generated automatically by the tool.
Conclusions:
see publications
Publications:
"Reuse of verified design components".
David Hemer and Peter Lindsay. SVRC TR 97-3, January 1997. http://www.it.uq.edu.au/cgi-bin/svrc-tech-report?97-03
"A template-based approach to construction of verified software". Peter Lindsay
and David Hemer. SVRC TR 96-23, November 1996. http://www.it.uq.edu.au/cgi-bin/svrc-tech-report?96-23
"The CARE toolset for developing verified programs from formal specifications".
Peter Lindsay and David Hemer. In: O. Frieder and J. Wigglesworth (eds), Proceedings of
the 4th IEEE International Symposium on Assessment of Software Tools, Toronto, Canada, May
1996. http://www.it.uq.edu.au/cgi-bin/svrc-tech-report?95-52
"An industrial-strength method for the construction of formally verified
software". Peter Lindsay and David Hemer. In: Proceedings of the 9th Australian
Software Engineering Conference (ASWEC'96), Melbourne, July 1996, IEEE Computer Society
Press. http://www.it.uq.edu.au/cgi-bin/svrc-tech-report?96-13
"The Data Logger case study in CARE". Peter Lindsay. In: Proceedings of the 5th
Australasian Refinement Workshop (ARW'96), Brisbane, April 1996. SVRC TR 95-10. http://www.it.uq.edu.au/cgi-bin/svrc-tech-report?95-10
Contact:
URL:
http://www.it.uq.edu.au/svrc/CARE
|
