DocumentCode
2038538
Title
Modelling a cardiac pacemaker visually and formally
Author
Leemans, Jérôme ; Amálio, Nuno
Author_Institution
Technol. & Commun., Univ. of Luxembourg, Luxembourg, Luxembourg
fYear
2012
fDate
Sept. 30 2012-Oct. 4 2012
Firstpage
257
Lastpage
258
Abstract
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.
Keywords
cardiology; diagrams; formal specification; medical computing; pacemakers; program verification; specification languages; visual languages; visual programming; VCL diagram; Visual Contract Language; Z specification; cardiac pacemaker system; formal modelling language; software verification; visual modelling; visual predicate description; Computational modeling; Contracts; Heart beat; Pacemakers; Software; Visualization; formal methods; modelling; visual languages;
fLanguage
English
Publisher
ieee
Conference_Titel
Visual Languages and Human-Centric Computing (VL/HCC), 2012 IEEE Symposium on
Conference_Location
Innsbruck
ISSN
1943-6092
Print_ISBN
978-1-4673-0852-6
Type
conf
DOI
10.1109/VLHCC.2012.6344542
Filename
6344542
Link To Document