Medicine-by-wire: Practical considerations on formal techniques for dependable medical systems

Abstract We see the future of medicine as highly automated. Improvement in care-provision will be achieved by both increased clinician efficiency, as well as new computing assisted treatments and diagnoses. In other safety-critical industries, such as avionics and automotive, certification is dependability-driven. In contrast, medical certification is clinical-trial driven, which we argue will become increasingly problematic with increasing medical device and software complexity. By dependability, we mean the dictionary notion: reliable and trustworthy. Thus, failures are either avoided by design, or are accountable to a measured extent. This touches upon the verification (intent) versus validation (outcome) problem. Even though correctness does not imply safety, we do believe from our experiences that, the process of striving for correctness (verification) done right does shed light on safety; on whether the requirements/assumptions were addressed as intended (validation). Medical device trials can lead to adequate assurances of safety, as defined by the local regulatory burden. Nevertheless, the nature of such complex systems means that certain errors may not be detected by trials and so additional efforts to reduce errors is needed. Our intent is, at least for software, to explore the contrast between approaches: correctness-by-construction versus correct-by-trial. Additionally, these levels of safety and effectiveness of systems vary across regulatory domains in different countries. A key challenge is how to achieve a successful interaction between verification tasks using formal methods and system development tasks within engineering teams without prior knowledge of formal techniques. This paper describes a pragmatic process for the application of formal techniques, which is illustrated for three medical devices during pre-clinical development prior to certification. That means, the techniques are not only applied to realistic systems, but are also taken up by development teams themselves (i.e. cannot be entirely formal expert driven). We demonstrate differences in applying formalisms at the start, midpoint and final development stages. In particular, we describe the underlying socio-technical challenges and how we developed mitigation methods for each exemplar case. This paper is not about a general technique for medical automation, as we do not believe this is practical/possible given the varied/dynamic nature of medical problems.