Formal Specification of Medical Systems by Proof-Based Refinement

Formal methods have emerged as an alternative approach to ensuring quality and correctness of highly critical systems, overcoming limitations of traditional validation techniques such as simulation and testing. We propose a refinement-based methodology for complex medical systems design, which possesses all the required key features. A refinement-based combined approach of formal verification, model validation using a model-checker and refinement chart is proposed in this methodology for designing a high-confidence medical device. Furthermore, we show the effectiveness of this methodology for the design of a cardiac pacemaker system.