Structural Invariants for Parameterized Architectures
229
correctness for at most c processes implies correctness for any number of processes
[18,27,26,7,34]. Other methods identify systems with well-structured transition relations [31,1,29]. An exhaustive chart of decidability results for verification of parameterized systems is drawn in [12]. When decidability is not of concern, over-approximation
and semi-algorithmic techniques such as regular model checking [36,2], SMT-based
bounded model checking [4,21], abstraction [10,14] and automata learning [19] can be
used to deal with more general classes of systems.
The efficiency of a verification method crucially relies on its ability to synthesize an
inductive safety invariant, i.e., an infinite set of configurations that contains the initial
configurations, is closed under the transition relation, and excludes the error configurations. In general, automatically synthesizing invariants requires computationally expensive fixpoint iterations [22]. In the particular case of parameterized systems, invariants
can be either global, relating the local states of all processes [23], or modular, relating
the local states of a few processes whose identity is irrelevant [38,20].
Our Contributions. The novelty of the approach described in this paper is three-fold:
1. The architecture of the system is not fixed a priori, but given as a parameter of
the verification problem. In fact, we describe parameterized systems using the
Behavior-Interaction-Priorities (BIP) framework [9], in which processes are instances of finite-state component types, whose interfaces are sets of ports, labeling
transitions between local states, and interactions are sets of strongly synchronizing
ports, described by formulae of an interaction logic. An interaction formula captures the architecture of the interactions (pipeline, ring, clique, tree) and the communication scheme (rendez-vous, broadcast), which are not hardcoded, but rather
specified by the designer of the system.
2. We synthesize parameterized invariants directly from the interaction formula of a
system, without iterating its transition relation. Such invariants depend only on the
structure (and not on the operational semantics) of an infinite family of Petri Nets,
one for each instance of the system, and are thus structural invariants. Essentially,
the invariants we infer use the traps 4 of the system, which are sets W of local states
with the property that, if a process is initially in a state from W, then always some
process will be in a state from W. Following [11,17], we call them (parameterized) trap invariants. Computing trap invariants only requires a simple syntactic
transformation of the interaction formula and the result is expressed using WSκS,
the weak monadic second order logic of κ ≥ 1 successor functions. Thus invariant
computation is very cheap, and the verification problem (proving the emptiness of
the intersection between the invariant and the set of error states) is reduced to the
unsatisfiability of a WSκS formula with a single quantifier alternation. In practice,
this check can be carried out quite efficiently by existing tools, such as Mona [33].
3. We refine the approach by considering so called 1-invariants, that can also be derived cheaply from the interaction formula of the system. We show that 1-invariants
in conjunction with trap invariants successfully verify additional examples.
Comparison to related work. Trap invariants have been very successfully used in the
verification of non-parameterized systems [11,28,13]. The technique was lifted to parameterized systems in [17], but the work there is only applicable to clique architec4 Called in this way by analogy with the notion of traps for Petri Nets [39].
229
correctness for at most c processes implies correctness for any number of processes
[18,27,26,7,34]. Other methods identify systems with well-structured transition relations [31,1,29]. An exhaustive chart of decidability results for verification of parameterized systems is drawn in [12]. When decidability is not of concern, over-approximation
and semi-algorithmic techniques such as regular model checking [36,2], SMT-based
bounded model checking [4,21], abstraction [10,14] and automata learning [19] can be
used to deal with more general classes of systems.
The efficiency of a verification method crucially relies on its ability to synthesize an
inductive safety invariant, i.e., an infinite set of configurations that contains the initial
configurations, is closed under the transition relation, and excludes the error configurations. In general, automatically synthesizing invariants requires computationally expensive fixpoint iterations [22]. In the particular case of parameterized systems, invariants
can be either global, relating the local states of all processes [23], or modular, relating
the local states of a few processes whose identity is irrelevant [38,20].
Our Contributions. The novelty of the approach described in this paper is three-fold:
1. The architecture of the system is not fixed a priori, but given as a parameter of
the verification problem. In fact, we describe parameterized systems using the
Behavior-Interaction-Priorities (BIP) framework [9], in which processes are instances of finite-state component types, whose interfaces are sets of ports, labeling
transitions between local states, and interactions are sets of strongly synchronizing
ports, described by formulae of an interaction logic. An interaction formula captures the architecture of the interactions (pipeline, ring, clique, tree) and the communication scheme (rendez-vous, broadcast), which are not hardcoded, but rather
specified by the designer of the system.
2. We synthesize parameterized invariants directly from the interaction formula of a
system, without iterating its transition relation. Such invariants depend only on the
structure (and not on the operational semantics) of an infinite family of Petri Nets,
one for each instance of the system, and are thus structural invariants. Essentially,
the invariants we infer use the traps 4 of the system, which are sets W of local states
with the property that, if a process is initially in a state from W, then always some
process will be in a state from W. Following [11,17], we call them (parameterized) trap invariants. Computing trap invariants only requires a simple syntactic
transformation of the interaction formula and the result is expressed using WSκS,
the weak monadic second order logic of κ ≥ 1 successor functions. Thus invariant
computation is very cheap, and the verification problem (proving the emptiness of
the intersection between the invariant and the set of error states) is reduced to the
unsatisfiability of a WSκS formula with a single quantifier alternation. In practice,
this check can be carried out quite efficiently by existing tools, such as Mona [33].
3. We refine the approach by considering so called 1-invariants, that can also be derived cheaply from the interaction formula of the system. We show that 1-invariants
in conjunction with trap invariants successfully verify additional examples.
Comparison to related work. Trap invariants have been very successfully used in the
verification of non-parameterized systems [11,28,13]. The technique was lifted to parameterized systems in [17], but the work there is only applicable to clique architec4 Called in this way by analogy with the notion of traps for Petri Nets [39].