240
M. Bozga et al.
We devote the rest of this section to describe WSκS formulae which capture the
structural properties necessary to define 1-invariants as laid down by Lemma 3 (2). As
demonstrated in Section 3 the pre- and postset of transitions, as well as general sets of
places in a PN describing the execution semantics can be defined in WSκS. Hence, we
present the definitions of the following formulae only in the full version of this article
[16] and just give the intuitions here.
As before, we fix two tuples of set variables X and X , with one variable X s for each
state s ∈
N
i=1 S
i and define the following formulae:
– unique-init S (X), which captures that the set of places induced by an interpretation
of X uniquely intersects the set of all initial states, and
– unique-intersection S (X, X ), which states that the set of places induced by an interpretation of X and X share precisely one place.
Given a transition t of the marked Petri Net N U
S
defining the execution semantics of a
component-based system S, for a universe U, we consider the following formulae:
– uniquepre C
S
(X, x 1 ,..., x ), which describes that the set of places encoded by the interpretation of X uniquely intersects • t, and
– uniquepost C
S
(X, x 1 ,..., x ), which in the same sense captures the unique intersection
with t • .
Now we define a predicate 1-pred S which consists of a conjunction of unique-init S and
the formulae:
∀x 1 ,...,∀x . (Tr(ϕ) → [¬ intersects-pre C
S
∧¬ intersects-post C
S
∨ uniquepre C
S
∧ uniquepost C
S
∨ intersects-pre C
S
∧¬ uniquepre C
S
])
(8)
one for each clause C in Γ. We show the soundness of this definition, by the following:
Lemma 4. Let S = C
1
,..., C
N
,Γ be a component-based system and let X be a tuple
of set variables, one for each state in a component of S. Then, for any structure (U,ι)
such that ι interprets the variables in X, the set P = {{s, u ∈
N
i=1 S
i
× U | u ∈ ι(X s )} is a
1-invariant of N U
S
if (U,ι) | = WSκS 1-pred S (X).
We may now define the 1-invariant analogously to the trap-invariant before:
1-invariant S (X) = ∀X . 1-pred S (X ) → unique-intersection S (X, X ).
(9)
Reasoning as before we obtain a refinement of Theorem 1 since every reachable
marking has to satisfy both invariants.
Theorem 2. Given a component-based system S and a WSκS formula ϕ(X), if the
formula:
∃X . marking S (X) ∧ 1-invariant S (X) ∧ trap-invariant S (X) ∧ ¬ϕ(X)
(10)
is unsatisfiable, then for every universe U, the property defined by the formula ϕ(X)
holds in every reachable marking of N U
S
.
5 Experiments
We have implemented a prototype (called ostrich [15]) of this verification procedure to evaluate the viability of our approach. The current version of the prototype
M. Bozga et al.
We devote the rest of this section to describe WSκS formulae which capture the
structural properties necessary to define 1-invariants as laid down by Lemma 3 (2). As
demonstrated in Section 3 the pre- and postset of transitions, as well as general sets of
places in a PN describing the execution semantics can be defined in WSκS. Hence, we
present the definitions of the following formulae only in the full version of this article
[16] and just give the intuitions here.
As before, we fix two tuples of set variables X and X , with one variable X s for each
state s ∈
N
i=1 S
i and define the following formulae:
– unique-init S (X), which captures that the set of places induced by an interpretation
of X uniquely intersects the set of all initial states, and
– unique-intersection S (X, X ), which states that the set of places induced by an interpretation of X and X share precisely one place.
Given a transition t of the marked Petri Net N U
S
defining the execution semantics of a
component-based system S, for a universe U, we consider the following formulae:
– uniquepre C
S
(X, x 1 ,..., x ), which describes that the set of places encoded by the interpretation of X uniquely intersects • t, and
– uniquepost C
S
(X, x 1 ,..., x ), which in the same sense captures the unique intersection
with t • .
Now we define a predicate 1-pred S which consists of a conjunction of unique-init S and
the formulae:
∀x 1 ,...,∀x . (Tr(ϕ) → [¬ intersects-pre C
S
∧¬ intersects-post C
S
∨ uniquepre C
S
∧ uniquepost C
S
∨ intersects-pre C
S
∧¬ uniquepre C
S
])
(8)
one for each clause C in Γ. We show the soundness of this definition, by the following:
Lemma 4. Let S = C
1
,..., C
N
,Γ be a component-based system and let X be a tuple
of set variables, one for each state in a component of S. Then, for any structure (U,ι)
such that ι interprets the variables in X, the set P = {{s, u ∈
N
i=1 S
i
× U | u ∈ ι(X s )} is a
1-invariant of N U
S
if (U,ι) | = WSκS 1-pred S (X).
We may now define the 1-invariant analogously to the trap-invariant before:
1-invariant S (X) = ∀X . 1-pred S (X ) → unique-intersection S (X, X ).
(9)
Reasoning as before we obtain a refinement of Theorem 1 since every reachable
marking has to satisfy both invariants.
Theorem 2. Given a component-based system S and a WSκS formula ϕ(X), if the
formula:
∃X . marking S (X) ∧ 1-invariant S (X) ∧ trap-invariant S (X) ∧ ¬ϕ(X)
(10)
is unsatisfiable, then for every universe U, the property defined by the formula ϕ(X)
holds in every reachable marking of N U
S
.
5 Experiments
We have implemented a prototype (called ostrich [15]) of this verification procedure to evaluate the viability of our approach. The current version of the prototype