Cyber-Physical Systems

312 Cyber-Physical Systems: From Theory to Practice

x

1

x

y

(a) (b)

y = x

0≤x ≤1

x

1

y

x

1

y

(c) (d)

proj

{x,y}

(

0≤

x ≤1

)

0 ≤ x ≤1

y = x

FIGURE 13.2 The assertions W

0≤x≤1

and W

y=x

are shown in (a) and (b), respectively. The assertions



proj

{x,y}

(W

0≤x≤1

) and W

0≤x≤1



∩W

y=x

are shown in (c) and (d), respectively.

x

(a) (b) (c)

y

x

x

y

proj

{x,y}

( proj

{x}

(

))

y = x

proj

{x}

(

y=x

)

y = x

FIGURE 13.3 In a), an assertion W

y=x

is shown where W

y=x

constrains {y}. The assertions proj

{x}



W

y=x



and



proj

{x,y}



proj

{x}



W

y=x



are shown in b) and c), respectively.

Contracts for Specifying and Structuring ...