Translating a VDM Model of a Medical Device into Kapture

TL;DR

This paper demonstrates that inexperienced users can effectively translate complex VDM models of medical devices into Kapture, achieving over 90% coverage and matching results, despite initial challenges and learning curve.

Contribution

It is the first known attempt to translate a VDM model into Kapture for medical devices, evaluating usability and effectiveness with minimal prior experience.

Findings

Over 90% of the VDM model was covered in Kapture

Matching traces of results were produced

Initial learning curve posed challenges

Abstract

As the complexity of safety-critical medical devices increases, so does the need for clear, verifiable, software requirements. This paper explores the use of Kapture, a formal modelling tool developed by D-RisQ, to translate an existing formal VDM model of a medical implant for treating focal epilepsy called CANDO. The work was undertaken without prior experience in formal methods. The paper assess Kapture's usability, the challenges of formal modelling, and the effectiveness of the translated model. The result is a model in Kapture which covers over 90% of the original VDM model, and produces matching traces of results. While several issues were encountered during design and implementation, mainly due to the initial learning curve, this paper demonstrates that complex systems can be effectively modelled in Kapture by inexperienced users and highlights some difficulties in translating VDM specifications to Kapture.