158
A. Cimatti et al.
A
Off
On
[3, 6]
B
Off
On
[2, 4]
(a) Example of system with two local requirements and one state dependency.
E
Off
Normal
[1, 2]
C
Off
Normal
High
[2, 3]
[2, 3]
D
Off
Normal
[4, 6]
(b) Example of system with two local requirements and two signal dependencies.
Definition 1 (Local Requirements) A specification S is given by a set of
local (or component) requirements, where each local requirement C ∈ S is given
by an (ordered) sequence P
C
1 , . . . , P
C
n of phases. In turn, each phase P i of C
is associated when i > 1 with a closed real interval β Pi with non-negative lower
limit l Pi and (finite or infinite) upper limit u Pi , with a formula φ Pi (called signal
dependency) and, when i > 0 with a formula ψ Pi (called state dependency). Both
φ Pi and ψ Pi are Boolean formulae over the atoms in {{D, Q} D∈S\{C},Q∈D (i.e.,
the phases of other components).
If a dependency ψ P is just a conjunction of atoms, then we say that ψ P is
convex. With the notation |C|, we will refer to the number of phases of C.
Figs. 1a and 1b show two examples of sets of local requirements. In Fig. 1a,
we have two local requirements A and B (i.e., S = {A, B}); each local requirement has two phases Off and On (i.e., P
A
1 = Off and P
A
2 = On and similarly for B); the bounds are depicted in square brackets (thus, for example
β
A
On = [3, 6]); all dependencies are trivially true apart from the state dependency ψ
B
On = A, On of the local requirement B, which is plotted as an arrow
from the phase On of B to phase On of A. In Fig. 1b, we have another example
with three components and some signal dependencies; for example, signal dependency φ
C
Normal = E, Normal is plotted as an arrow from the transition to
phase Normal of C to phase Normal of E.
Definition 2 (Stronger local requirements) We say that a local requirement
C
= P
C
1 , . . . , P
C
n is stronger than C = P
C
1 , . . . , P
C
n (written C
C), iff
phase P
C
i
is identical to P
C
i except that l P C
i
≤ l P C
i
and u P C
i
≤ u P C
i
, for all
1 ≤ i ≤ n. Given two specifications S = {C 1 , . . . , C n } and S
= {C
1 , . . . , C
n },
we say that S
is stronger than S (written S
S) iff for all i, 1 ≤ i ≤ n,
|C i | = |C
i | and C
i C i .
In defining the semantics of a composition of local requirements C 1 . . . C n ,
every local requirement C i is associated with a local clock, which is reset each
time it enters a new phase. Given a local requirements specification {C 1 , . . . , C n },
A. Cimatti et al.
A
Off
On
[3, 6]
B
Off
On
[2, 4]
(a) Example of system with two local requirements and one state dependency.
E
Off
Normal
[1, 2]
C
Off
Normal
High
[2, 3]
[2, 3]
D
Off
Normal
[4, 6]
(b) Example of system with two local requirements and two signal dependencies.
Definition 1 (Local Requirements) A specification S is given by a set of
local (or component) requirements, where each local requirement C ∈ S is given
by an (ordered) sequence P
C
1 , . . . , P
C
n of phases. In turn, each phase P i of C
is associated when i > 1 with a closed real interval β Pi with non-negative lower
limit l Pi and (finite or infinite) upper limit u Pi , with a formula φ Pi (called signal
dependency) and, when i > 0 with a formula ψ Pi (called state dependency). Both
φ Pi and ψ Pi are Boolean formulae over the atoms in {{D, Q} D∈S\{C},Q∈D (i.e.,
the phases of other components).
If a dependency ψ P is just a conjunction of atoms, then we say that ψ P is
convex. With the notation |C|, we will refer to the number of phases of C.
Figs. 1a and 1b show two examples of sets of local requirements. In Fig. 1a,
we have two local requirements A and B (i.e., S = {A, B}); each local requirement has two phases Off and On (i.e., P
A
1 = Off and P
A
2 = On and similarly for B); the bounds are depicted in square brackets (thus, for example
β
A
On = [3, 6]); all dependencies are trivially true apart from the state dependency ψ
B
On = A, On of the local requirement B, which is plotted as an arrow
from the phase On of B to phase On of A. In Fig. 1b, we have another example
with three components and some signal dependencies; for example, signal dependency φ
C
Normal = E, Normal is plotted as an arrow from the transition to
phase Normal of C to phase Normal of E.
Definition 2 (Stronger local requirements) We say that a local requirement
C
= P
C
1 , . . . , P
C
n is stronger than C = P
C
1 , . . . , P
C
n (written C
C), iff
phase P
C
i
is identical to P
C
i except that l P C
i
≤ l P C
i
and u P C
i
≤ u P C
i
, for all
1 ≤ i ≤ n. Given two specifications S = {C 1 , . . . , C n } and S
= {C
1 , . . . , C
n },
we say that S
is stronger than S (written S
S) iff for all i, 1 ≤ i ≤ n,
|C i | = |C
i | and C
i C i .
In defining the semantics of a composition of local requirements C 1 . . . C n ,
every local requirement C i is associated with a local clock, which is reset each
time it enters a new phase. Given a local requirements specification {C 1 , . . . , C n },