
Contracts for Specifying and Structuring Requirements on Cyber-Physical Systems 317
h
f
v
gnd
G
lMeter
A
lMeter
v
ref
v
gnd
l
v
branch
Esys
lMeter
tank
bat
pot
FIGURE 13.7 A contract C
lMeter
= ({A
lMeter
}, G
lMeter
).
means that the conditions hold for any type of architecture that is considered and further for the cases
where the contract is not limited to the interface of the element.
As a start, a general definition of a contract is presented.
Definition 13.5 (Contract) A contract C is a pair (A, G), where
(i) G is an assertion, called guarantee
(ii) A is a set of assertions
{
A
i
}
N
i=1
, where each A
i
is called an assumption
In the context of an architecture, a guarantee