From Informal System Requirements to Formal Software Specifications - An Experience Report

Formal methods have been enormously useful in verifying complex system requirements, especially in the safety critical domain. However, their success depends on precisely formalizing what needs to be verified and thoroughly understanding how it is verified. Unfortunately, there is a lack of awareness and guidance in using formal techniques effectively, that often makes their use difficult and the results of their application leading to overconfidence in the correctness of the fielded system in its intended environment. In this paper, we share some of the lessons learnt while using formal methods to specify and verify a complex infusion pump system. While the effort was successful and has led to hierarchically verified software for the pump, it was not without challenges that we believe are not adequately presented in the research literature. We discuss the challenges we faced with (a) precisely 'flowing down' system-level requirements to low level components, (b) thoroughly understanding the technicalities of the formal tools to avoid faulty premises and misplaced confidence on the overall system and (c) rigorously mitigating risks with using diverse formal tools in hierarchical system analysis. In the sequel, we also discuss our approach to mitigating them. We believe that the lessons we leaned in this effort serves informative for practitioners involved in similar efforts.