Cyber-Physical Systems

322 Cyber-Physical Systems: From Theory to Practice

lMeter

h

f

v

gnd

G΄

Esys

A΄

Esys

v

ref

v

gnd

v

branch

l

v

gnd

v

ref

v

gnd

v

branch

l

h

f

G˝

Esys

(a) (b)

A˝

Esys

Esys

lMeter

tank

bat

pot

Esys

lMeter

bat

pot

FIGURE 13.9 Two contracts C



Esys

and C



Esys

for E

Esys

where E

Esys

and are shown in (a) and (b), respectively,

where E

Esys

and its environment in the architecture A

LMsys

shown in Figure 13.5 do not meet the relations in

Equations 13.7 and 13.9.

(b) As can be seen in Figure 13.9b, the variable v

branch

is in the scope of G



Esys

, but neither in the

interface of E

Esys

nor in the scope of A



Esys

. This means that in the generic case, that is, when

G



Esys

constrains {v

branch

} and when A



Esys