Translating a VDM Model of a Medical Device into Kapture
Journal:
arXiv
Published Date:
Jun 11, 2025
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.
