A VCL Model of a Cardiac Pacemaker - Visual Contract Language

Embedded software in medical devices is becoming ubiquitous and increasing in content and ... During the development of the VCL model, we encoun-.
5MB Sizes 0 Downloads 110 Views
A VCL Model of a Cardiac Pacemaker

J´erˆ ome Leemans and Nuno Am´alio Laboratory for Advanced Software Systems University of Luxembourg 6, rue R. Coudenhove-Kalergi L-1359 Luxembourg

TR-LASSY-12-04

Contents Contents

2

1 Introduction 1.1 Heart and Pacemakers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 The Visual Contract Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5 5 6 6

2 The CommonPM package

8

3 The Battery package 3.1 State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Overall behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10 10 10

4 The 4.1 4.2 4.3

RateSmoothing package State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Overall Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Global Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

12 12 12 13

5 The 5.1 5.2 5.3

AVDelay package State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Overall Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Global Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17 17 18 19

6 The 6.1 6.2 6.3

RateModulation Package State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Overall Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Global Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28 28 30 31

7 The 7.1 7.2 7.3 7.4

Pacing package State . . . . . . . . Overall Behaviour Local operations of Global Operations

. . . .

43 43 44 47 53

8 The 8.1 8.2 8.3

Sensing Package State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Overall Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

63 63 64 65

. . . . . . . . . . . . . . . . . . . . . . . . blob ChamberPacing . . . . . . . . . . . .

2

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

9 The ResponseCommon Package

75

10 The 10.1 10.2 10.3

AtrialResponse Package State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Overall Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Global Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

76 76 78 79

11 The 11.1 11.2 11.3

VentricularResponse State . . . . . . . . . . Overall Behaviour . . Global Operations . .

Package . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

94 94 95 95

12 The 12.1 12.2 12.3

Response package 101 State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 Overall Behaviour . . . . . . . . . . .