[en] Embedded software in medical devices is becoming ubiquitous and increasing in content and complexity. This paper gives an outline of a visual model of a cardiac pacemaker system, a case study from the grand challenge in software verification. The model is expressed in the Visual Contract Language (VCL), a formal modelling language that describes predicates visually. From VCL diagrams it is possible to generate Z specifications. This is the first visual and formal model of one of the software verification challenges.
Disciplines :
Sciences informatiques
Identifiants :
UNILU:UL-CONFERENCE-2013-037
Auteur, co-auteur :
Leemans, Jerome
AMALIO, Nuno ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Langue du document :
Anglais
Titre :
Modelling a cardiac pacemaker visually and formally
Date de publication/diffusion :
2012
Nom de la manifestation :
Visual Languages and Human-Centric Computing (VL/HCC), 2012
