1 Introduction and Motivation
1.1 Small Experiments
2 New High-Level Translation of B to Z3
2.1 Normalizing B / Event-B
B | Normalized B |
---|---|
\(E \ne S\)
|
\(\lnot (E = S)\)
|
\(E \not \in S\)
|
\(\lnot (E \in S)\)
|
\(E \not \subset S\)
|
\(\lnot (E \subset S)\)
|
\(E \not \subseteq S\)
|
\(\lnot (E \subseteq S)\)
|
\(E \subset S\)
|
\(\lnot (E=S) \wedge (E \subseteq S)\)
|
NAT, NAT1, INT
. We thus rewrite constraints featuring membership in one of these to a conjunction of disequalities, e.g.,-
\(\forall m . m \in S \Rightarrow t \le m\), i.e., the temporary variable is less or equal to all members of the set.
-
\(\exists m . m \in S \wedge t = s\), i.e., t is equal to one of the members of S.
-
The general union, general intersection, general sum and general product. For instance, the general union of \(U \in \mathbb {P}(\mathbb {P}(S))\) could be rewritten as \(union(U) = \{x | x \in S \wedge (\exists s . s \in U \wedge x \in s) \}\). However, the existential quantification inside the set comprehension leads to highly involved constraints later on.
-
The construction of (non-empty) powersets. Again we could translate\(\mathbb {P}(X) = \{ s | s \subseteq {} X \}\).
-
The iteration and closure operators of classical B.
2.2 Translation Rules
-
Some common operators have different semantics in B and SMT-LIB.
-
SMT-LIB as well as Z3 do not support set comprehensions natively. We will translate those by using a universal quantification constraining all members of a set variable.
-
User-given sets have to be mapped to SMT-LIB sorts.
INTEGER
, the B method features user defined types represented as deferred or enumerated sets. We translate those to custom SMT-LIB sorts. For enumerated sets we additionally introduce the identifiers and enforce their disequality using an additional constraint. Z3 natively supports sorts with given cardinality. Hence, if the cardinality of a user-given type can be computed statically by ProB we can submit said cardinality to Z3.3 Integration of Solvers
-
Use Z3 solely for falsification of B predicates. If we only rely on the SMT solvers for the detection of unsatisfiability, we can safely skip untranslatable parts of the predicate without risking unsound results (as those parts will be checked by ProB’s solver). However, many predicates cannot be disproven once important parts are missing.
-
We could employ a cooperative approach where parts of a predicate are given to one or both of the SMT solvers, while other parts are handled by the ProB kernel. In this case, we would translate partial assignments back and forth between the two solvers in order to communicate intermediate results.
-
Lastly, we could use a fully integrated approach where the whole predicate is given to the ProB kernel and as much as is translatable is given to the SMT solvers. In addition to partial assignments we could transport information about inferred or learned clauses or unsatisfiable cores back and forth.
4 Limitations
Model | # POs | SMT | HL-SMT |
ProB
|
ProB/SMT | |||
---|---|---|---|---|---|---|---|---|
prove | disprove | prove | disprove | prove | disprove | |||
Landing Gear System 1, Su, et al. | 2328 | 1478 | 2196 | 0 | 2311 | 0 | 2303 | 0 |
Landing Gear System 2, Su, et al. | 1188 | 548 | 741 | 0 | 1176 | 0 | 1152 | 0 |
Landing Gear System 3, Su, et al. | 341 | 171 | 77 | 0 | 290 | 0 | 262 | 0 |
CAN Bus, Colley | 534 | 296 | 316 | 0 | 276 | 0 | 340 | 1 |
Graph Coloring, Andriamiarina, et al. | 254 | 119 | 51 | 0 | 0 | 0 | 51 | 0 |
Landing Gear System, Hansen, et al. | 74 | 59 | 55 | 0 | 74 | 0 | 74 | 0 |
Landing Gear System, Mammar, et al. | 433 | 265 | 212 | 0 | 400 | 0 | 413 | 0 |
Landing Gear System, André, et al. | 619 | 263 | 77 | 0 | 567 | 5 | 533 | 4 |
Pacemaker, Neeraj Kumar Singh | 370 | 198 | 369 | 0 | 354 | 0 | 370 | 0 |
Stuttgart 21 interlocking, Wiegard | 202 | 46 | 18 | 0 | 125 | 2 | 123 | 0 |
5 Empirical Results
-
HL-SMT, our high-level translation from Event-B to SMT featuring Z3’s set theory, alone without ProB’s solver,
-
ProB, a plain version of ProB’s constraint solving kernel, and
-
ProB/SMT, ProB’s constraint solving kernel integrated with Z3.
-
A model of the Stuttgart 21 Railway station interlocking by Wiegard, derived from Chap. 17 of [2] with added timing and performance modeling.
-
A model of a controller area network (CAN) bus developed by Colley.
-
A formal development of a graph coloring algorithm by Andriamiarina and Méry. The graphs to be colored are finite, but unbounded and not fixed in the model.
-
A model of a pacemaker by Méry and Singh [22].
-
Figure 2 shows a Venn diagram comparing the number of discharged proof obligations by each of the configurations mentioned above.
-
Table 2 shows how the individual configurations perform on the different models. In particular it distinguishes between proof and disprove.
-
Table 3 shows how the individual configurations perform on different kinds of proof obligations.
Kind of PO | # POs | SMT | HL-SMT |
ProB
|
ProB/SMT |
---|---|---|---|---|---|
Feasibility of non-det. action | 59 | 40 (67.8 %) | 52 (88.1 %) | 44 (74.6 %) | 57 (96.6 %) |
Guard strengthening | 300 | 13 (4.3 %) | 139 (46.3 %) | 258 (86.0 %) | 254 (84.7 %) |
Invariant preservation | 4938 | 3106 (62.9 %) | 3741 (75.8 %) | 4488 (90.9 %) | 4552 (92.2 %) |
Natural number for a numeric variant | 6 | 5 (83.3 %) | 6 (100.0 %) | 4 (66.7 %) | 6 (100.0 %) |
Action simulation | 153 | 104 (68.0 %) | 86 (56.2 %) | 134 (87.6 %) | 142 (92.8 %) |
Theorem | 97 | 29 (29.9 %) | 26 (26.8 %) | 66 (68.0 %) | 62 (63.9 %) |
Decreasing of variant | 6 | 6 (100.0 %) | 6 (100.0 %) | 6 (100.0 %) | 6 (100.0 %) |
Well definedness | 779 | 140 (18.0 %) | 56 (7.2 %) | 570 (73.2 %) | 539 (69.2 %) |
Feasibility of a witness | 1 | 0 (0.0 %) | 0 (0.0 %) | 1 (100.0 %) | 1 (100.0 %) |
Well definedness of a witness | 4 | 0 (0.0 %) | 0 (0.0 %) | 2 (50.0 %) | 2 (50.0 %) |
6343 | 3443 (54.3 %) | 4112 (64.8 %) | 5573 (87.9 %) | 5621 (88.6 %) |