Developing an Insulin Pump System Using the SOFL Method

Insulin pump system is a safety-critical embedded system controlling the amount of injection of insulin to diabetics based upon their blood glucose levels, and the high reliability of the software used in the pump is crucial. One way to achieve the high reliability of software is to build an accurate and complete model through effective analysis and specification, and to implement the system based upon the specification. In this paper, we describe how the SOFL formal engineering method is applied to develop a specific insulin pump system in practice. In particular, we focus on the issue of how the three-step modeling approach advocated by the SOFL method, which includes informal, semi-formal, and formal specifications, is utilized to obtain a precise and valid specification of the embedded software for the insulin pump system. We also discuss how the specification benefits the implementation of the system, and report our experience and lessons learned.