Figure 3. Quantitative verification of reliability requirements.

Figure 4. Formalization of S,D  R for the medical-assistance application in Figure 2.

S

{patient-requested
alarm}
{alarm service}
{failed alarm}
{change drug
service}
{result}
{request}
{patient data
analysis} {analysis ervice}
{failed
analysis}

0.2

0.8

y 1-x

z
1-y 1-z
0.12
c1

c2 c3

1 x1

1

1

0.43 0.45 1

{ok}

D
R

,

x = 0.04 y = 0.0015 z = 0.0012 c1 = 2. 5 c2 = 9. 3 c3 = 0.1

|=

R2 : P≤0.14 [ true U failed-alarm ∨ failed-analysis ∨ failed-drug-service ]

R3 : R≤ 10 [ true U ok ∨ alarm-service ∨
change-drug-service ∨ failed-analysis ]
...