State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin

Abstract

In previous work, we presented symbolic reachability analysis by linking ProB, an animator and model checker for B and Event-B, and LTSmin, a language-independent model checker offering state-of-the-art model checking algorithms. Although the results seemed very promising, it was a very basic integration of these tools and much potential of LTSmin was not covered by the implementation.

In this paper, we present a much more mature version of this tool integration. In particular, explicit-state model checking, efficient verification of state invariants, model checking of LTL properties, as well as partial order reduction and proper multi-core model checking are now available. The (improved) performance of this advanced tool link is benchmarked on a series of models with various sizes and compared to ProB.

J. Meijer—Supported by STW SUMBAT grant: 13859.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Formal methods, e.g., the B-Method [3], are vital to ensure correctness in software where failure means loss of money or even risking human lives. Yet, for industrial application, tooling often remains unsatisfactory [6, 34]. One such tool is ProB, an animator and model checker for B and Event-B. While ProB is fairly mature after hundreds of man-years of engineering effort, it may still struggle with industrial-sized models containing several millions of states. LTSmin, however, is a language-independent model checker that offers symbolic algorithms and many optimizations in order to deal with the state space explosion problem.

In [4], we linked LTSmin with ProB in order to obtain a symbolic reachability analysis for B and Event-B. ProB was computing the B operational semantics and providing static information about possible state transitions while LTSmin was performing the symbolic reachability algorithm.

LTSmin offers further model checking algorithms and optimizations, both for its symbolic and for its sequential backend. In this paper, we describe how we extended the link between LTSmin and ProB using ZeroMQ [18] in order to obtain a model checking tool for B and Event-B and evaluate the performance on a set of real life, industrial-sized models. LTSmin’s language frontend that interacts with ProB can directly be used with any model checker that speaks the same protocol via ZeroMQ. The extension is based on [20] and includes:

• invariant checking (for both the symbolic and sequential backend),

• guard splitting for symbolic analysis of B models,¹

• partial order reduction (with the sequential backend),

• (parallel) LTL model checking (with the sequential/multi-core backend),

• effective caching of transitions and state labels,

• short states, to transmit only relevant variables for each transition.

1.1 LTSmin

LTSmin [8] is an open-source, language-independent, state-of-the-art model checker that offers many model checking algorithms including partial order reduction, LTL verification and distributed model checking. An overview of its architecture can be found in Fig. 1. By implementing the Pins, i.e., the partitioned interface to the next-state function, new language frontends can employ these algorithms. At its core, Pins consists of three functions: one that provides an initial state vector, a second, partitioned transition function that calculates successor states and, lastly, a state labelling function.

Fig. 1.

Modular Pins architecture of LTSmin [19]

LTSmin provides four backends:

• a sequential backend that implements an explicit state model checking algorithm similar to the one implemented in ProB,

• a symbolic backend that stores states as LDDs (List Decision Diagrams) [7],

• a multi-core backend that works similar to the sequential backend, but is capable of using multiple CPU cores on the same machine,

• a distributed backend in order to utilize multiple machines for model checking.

For this article, we will focus on the advances of the integration with ProB using the sequential and symbolic backends but also experiment with the multi-core backend. We have not done any experiment with the distributed backend yet.

1.2 ProB and the B-Method

ProB [25] is an open-source animator and model checker for several formalisms including B, Event-B, CSP, Z and TLA$^{+}$. It can be used in order to find invariant or assertion violations or deadlock states in machine specifications. While it implements a straightforward explicit state model checker, it also ships more advanced techniques, e.g., symmetry reduction [29], partial order reduction [15, 16] or symbolic model checking [22]. This style of symbolic model checking [9], where states are stored as predicates, must not be confused with the symbolic model checking that LTSmin provides, where states are stored as decision diagrams. ProB’s core is written in SICStus Prolog [10] and may also employ SMT solvers [23], such as Z3 and CVC4, or SAT solvers, such as Kodkod [28].

When integrating ProB into LTSmin, we focus on two formalisms: B (sometimes referred to as “classical B”) is part of the B-Method [3], where software is developed starting with a very abstract model that iteratively is refined to a concrete implementation. This method aims for software to be “correct by construction”. Event-B [1] is considered to be the successor of B that does not include constructs that often hinder formal proof in the language, e.g., conditional assignments or loops. Both formalisms offer a very high level of abstraction and are based on set theory and first-order logic.

1.3 Theoretical Background

We repeat the most important definitions used in [4] on the following contrived example:

Fig. 2.

Contrived B machine example

Definition 1

(Transition System). A Transition System (TS) is a structure $\left( \mathcal {S},\mathop {\rightarrow },I \right)$, where $\mathcal {S}$ is a set of states, $\mathop {\rightarrow }\subseteq \mathcal {S}\times \mathcal {S}$ is a transition relation and $I\subseteq \mathcal {S}$ is a set of initial states. Furthermore, let $\mathop {\rightarrow ^*}$ be the reflexive and transitive closure of $\mathop {\rightarrow }$, then the set of reachable states is $\mathcal {R} = \left\{ s \in \mathcal {S}\mid \exists s' \in I\mathrel {.}s' \mathop {\rightarrow ^*}s \right\}$.

Such transition systems are induced by both B and Event-B models. As all variables have to be typed, the set of states $\mathcal {S}$ is the Cartesian product of all types. All possible initial states are given in the INITIALISATION machine clause. The union of all operations define the transition relation $\mathop {\rightarrow }$. For symbolic model checking however, it is very important that the transition relation is split into groups.

Definition 2

(Partitioned Transition System). A Partitioned Transition System (PTS) is a structure $\mathcal {P} = \left( \mathop {S^\textsc {n}}, \mathcal {T}, \mathop {\rightarrow ^\textsc {m}}, I^\textsc {n} \right)$, where

• $\mathop {S^\textsc {n}}= S_1 \times \ldots \times S_\textsc {n}$ is the set of states, which are vectors of $\textsc {n}$ values,

• $\mathcal {T} = (\rightarrow _1,\ldots ,\rightarrow _{\textsc {m}})$ is a vector of M relations, called transition groups, ${\rightarrow _i} \subseteq \mathop {S^\textsc {n}}\times \mathop {S^\textsc {n}}$ ($\forall 1 \le i \le \textsc {m}$),

• $\mathop {\rightarrow ^\textsc {m}}= \bigcup _{i=1}^\textsc {m} {\rightarrow _i}$ is the overall transition relation induced by $\mathcal {T}$, i.e., the union of the $\textsc {m}$ transition groups, and

• $I^\textsc {n} \subseteq \mathop {S^\textsc {n}}$ is the set of initial states.

We write $\mathbf {s} \rightarrow _i \mathbf {t}$ when $\left( \mathbf {s}, \mathbf {t} \right) \in {\rightarrow _i}$ for $1 \le i \le \textsc {m}$, and $\mathbf {s} \mathop {\rightarrow ^\textsc {m}}\mathbf {t}$ when $\left( \mathbf {s}, \mathbf {t} \right) \in \mathop {\rightarrow ^\textsc {m}}$.

Strictly speaking, the transition relation in Definition 2 is not partitioned, as individual B operations can have same effect. We implemented an easy mental model where each transition group represents exactly one operation in the B model.

For the example in Fig. 2, the only initial state is $init ^{\left( c,x,y \right) } = \left( 100, 0, 0 \right)$. We agree on a notation where the ordering of the variables in an individual state is given once as a superscript. In LTSmin, the ordering of the variables is fixed and unambiguous. Then, $I^\textsc {n} = \left\{ {\left( 100, 0, 0 \right) } \right\}$, $\mathop {S^\textsc {n}}= \mathbb {Z} \times \mathbb {Z} \times \mathbb {Z}$ and $\mathcal {T} = \left( \mathtt {incx}, \mathtt {doublex}, \mathtt {incy}, \mathtt {incxmaybey} \right)$ with, e.g., $\mathtt {incx} = \{ \left( 100, 0, 0 \right) \rightarrow _{1} \left( 100, 1, 0 \right) ,$ $\left( 100, 0, 1 \right) \rightarrow _{1} \left( 100, 1, 1 \right) ,$ $\left( 100, 1, 0 \right) \rightarrow _{1} \left( 100, 2, 0 \right) , \ldots \}$.

Symbolic Model Checking and Event Locality. In many B models, operations only read from and write to a small subset of variables, which is known as event locality [11]. Symbolic model checking benefits from event locality, allowing reuse of successor states when only variables changed that are irrelevant to the state transition.

In order to employ LTSmin’s symbolic algorithms [7, 26, 27], ProB provides several dependency matrices about the B model that shall be checked: A read matrix and may-write matrix is used in order to determine independence between transition groups for symbolic model checking. These two matrices for Fig. 2 are given in Fig. 3. Entries are set to 1, if the operation reads or writes the variable, and otherwise to 0. Further matrices are shown once their use-case is introduced.

Fig. 3.

Dependency matrices

Fig. 4.

Overview of the tool integration LTSmin $\leftrightarrow$ProB

2 Architecture Overview of LTSmin min$\leftrightarrow$ProB Integration

LTSmin and ProB typically run as two separate processes which can be launched both manually or start each other. They are linked as shown in Fig. 4. The processes are linked via one IPC (local inter-process communication) socket per tool provided by ZeroMQ [18], a library offering distributed messaging. We employ a request-reply pattern on these sockets, where LTSmin sends requests and ProB responds. In order to handle messaging in ProB, we added a small layer in C.

In order to expose information about the loaded model to LTSmin, ProB’s response to an initial request includes, amongst others, names of state variables and transition groups, an initial state and dependency matrices.

LTSmin expects a model to have a single initial state, while B and Event-B models allow for nondeterministic initialization. Thus, the initial state transferred to LTSmin consists of dummy values for all variables. Furthermore, we add a state variable named that is initially set to false. Via a special transition $init_state which is only applicable if is false, the actual initial states of the specification are exposed. For all these states (and their successors), is set to true. This technicality leads to special cases in the entire implementation which we will omit.

In order to call ProB’s next-state function, LTSmin sends a request containing the transition group and a state. ProB then will answer with a list of successor states. Since ProB is implemented in Prolog, it is hard to exchange states reasonably. Prolog terms have a limited life-span when using SICStus’ foreign function interface. Thus, we serialize and deserialize state variables into/from blobs (binary large objects) by making use of an undocumented Prolog library named fastrw. Each variable is stored in a separate blob, such that, a state is only a vector of blobs for LTSmin. Naturally, repeated (de)serialization comes with an overhead that we chose to accept for now.

The labelling function is called in the same way, providing a label name and a state. ProB will answer with either true or false.

3 Implementation

In order to extend the prior integration, ProB needs to expose more of the B model to LTSmin. In this section, we describe what information is additionally exchanged, how it is calculated and used by considering the running example in Fig. 2.

3.1 State Labels and Invariant Checking

In a labelled transition system, a set of atomic propositions is assumed. An atomic proposition is any predicate that we will call “state label”. ProB will implement the labelling function, i.e., it will receive a state and a state label and return true or false.

The entire invariant can be seen as a single atomic proposition. However, if only some variables change from one state to its successor, not all conjuncts need to be re-evaluated. Thus, we split the invariant into its conjuncts. Each conjunct is announced as a state label to LTSmin by providing a unique identifier. In order to expose which state label depends on which variable, additionally a state label matrix is included.

In our example in Fig. 2, initially, four state labels are created. The corresponding state label matrix is shown in Fig. 5.

Fig. 5.

State label dependency matrix

Since predicates are split at conjunctions, well-definedness issues might arise. As an example, consider the following predicate: $x \ne 0 \wedge 100 \; mod \; x = 1$. ProB’s constraint solver will reorder the conjuncts in order to exclude any division by zero. Once the predicate is split into $x \ne 0$ and $100 \; mod \; x = 1$, it will only receive a single conjunct and cannot do any reordering. Thus, in a state with $x = 0$, the second conjunct on its own will result in a well-definedness error.

Thus, if a well-definedness error arose, another part of the original predicate has to be unsatisfied and we can assume the offending conjunct to be false as well.

Proof Information. Event-B models exported from Rodin [2] include information about discharged proof information. ProB uses this information, e.g., in order to avoid checking an invariant that has been proven to be preserved when a specific action is executed [5]. If an invariant has been fully proven to be correct, i.e., that it holds in the initial states and all transitions preserve it, we can exclude it from the list of invariants exposed to LTSmin.

Even though the machine in Fig. 2 is written in classical B, i.e., there is no proof information available, the two invariant conjuncts $x \in \mathbb {Z}$ and $y \in \mathbb {Z}$ are dropped. The type checker can already prove that they will hold. Thus, there is no need to check them separately.

3.2 Short States

In order to call ProB via an interface function, LTSmin needs to transmit the entire state to ProB. ProB then deserializes all variables individually before the interpreter is called. Obviously, not all values are required in order to calculate a state transition or evaluate a predicate, rendering some overhead obsolete. Such an interface function is called long function, analogously a state that consists of all state variables is called a long state.

Instead of transmitting the entire state, LTSmin can make use of the dependency matrix in order to project a long state to state vector that only contains the values of accessed variables. Such a state is named short state and is relative to either a state label or transition group. An interface function that receives a short state is, analogously, named a short function. Short states can also be expanded back to long states by inserting values for the missing variables, e.g., those of a predecessor or initial state.

Short states come in two flavors: firstly, regular short states are of a fixed size per transition group or state label and only contain values both written to and read from. Consider the initial state $init ^{\left( c,x,y \right) } = \left( 100, 0, 0 \right)$ from Fig. 2. The corresponding short state for $\mathtt {incx}$ only contains c and x since y is not accessed. The projected short state, thus, is $init _{short}^{\left( c,x \right) } = \left( 100, 0 \right)$.

On the other hand, R2W short states (read to write) differ in the contained variables. LTSmin passes only read variables to ProB which in turn answers with written variables only. For $\mathtt {incx}$, the R2W short state that is passed to ProB also is $init _{read}^{\left( c,x \right) } = \left( 100, 0 \right)$ because all written variables also are read. However, c is a constant, thus the value does not change. Thus, the returned state only consists of x, i.e., $init _{read}^{\left( c,x \right) } \rightarrow _{1} = init _{write}^{\left( x \right) }$ with $init _{write}^{\left( x \right) } = \left( 1 \right)$.

Because there might be non-deterministic write accesses to variables (“may write”), a so-called copy vector is additionally passed to LTSmin. This copy vector is a bitfield marking which variables were actually written to and which values are taken from an earlier state. Additionally, the must-write matrix is given to LTSmin in order to expose which variables will be updated every single time.

Fig. 6.

Must-write matrix

The must-write matrix for Fig. 2 is given in Fig. 6. The difference to the may-write matrix is printed in bold. Note that if an entry in the must-write matrix is 1, it has to be 1 in the may-write matrix, but not vice versa. Then, consider the operation $\mathtt {incxmaybeincy}$ from Fig. 2. This operation only writes to y when x is an even number. Thus, for $s^{\left( c,x,y \right) }_{read} = \left( 100, 2, 2 \right)$ and $s \rightarrow _{4} s^{\prime }$, ${s^{\prime }}^{\left( x,y \right) }_{write} = \left( 3, 3 \right)$ and $cpy^{\left( x,y \right) }_{s \rightarrow s^{\prime }} = \left( 0, 0 \right)$, because both variables were actually written to. However, for ${\hat{s}}^{\left( c,x,y \right) }_{read} = \left( 100, 3, 2 \right)$ and ${\hat{s}} \rightarrow _{4} \hat{s}^{\prime }$, $\hat{s}^{\prime \left( x,y \right) }_{~write} = \left( 4, 2 \right)$. Yet, $cpy^{\left( x,y \right) }_{\hat{s} \rightarrow \hat{s}^{\prime }} = \left( 0, 1 \right)$ since y was not written to and the old value was copied.

Internally, LTSmin may use both long and short states and convert freely between them. The ProB language frontend always communicates R2W short states in order to minimize overhead by communication and (de)serialization. However, the caching layer works on regular short states, while, e.g., the variable reordering uses long states.

3.3 Caching Mechanism

While the symbolic backend calls the next-state function once with a state that represents a set of states, the sequential backend calls it for each of the states and transition groups. Analogously, the same holds true for state labels and calls to the labelling function.

Since we already calculate dependency matrices, which contain information about which variables are read and, in case of the next-state function, are written to, we can calculate the corresponding short state instead. Then, in order to avoid transferring and (de)serializing states as well as calculating the same state transition or state label multiple times, we can store results in hash maps, one per transition group and state label each. These hash maps map the corresponding short state to either a list of (short) successors states or a Boolean value in case of state labels. Only if the lookup in the hash table fails, the state is transferred to ProB. Otherwise, LTSmin can calculate the result by itself.

Currently, all operations are cached. Obviously, as more variables are accessed by an operation, caching offers lower benefit in exchange to the amount of memory consumed.

3.4 Guard Splitting

Operations (aka events or state transitions) are guarded, i.e., the action part that substitutes variables may only be executed if the guard predicate is satisfied. When LTSmin asks ProB to calculate successor states for a given transition group, ProB will evaluate the guard and, if applicable, try to find all (or a limited amount of) successors.

It is easy to make the following two observations: firstly, it is often more performant to evaluate single conjuncts of a guard individually. Usually, they access only a very limited amount of variables and can easily be cached. As an example, the guard $x < c$ of $\mathtt {incx}$ in Fig. 2 only reads two state variables (of which one is constant). Secondly, the same conjunct might guard multiple operations and, if evaluated for one operation in the same state, does not require additional evaluation for another operation. In Fig. 2, both $\mathtt {incx}$ and $\mathtt {incxmaybey}$ share the same guard $x < c$.

LTSmin’s symbolic backend supports splitting the action from evaluating its guard. A new interface function next-action is provided that works similar to the next-state function, but assumes the guard of an operation to be true. Then, only the action part is evaluated. A special matrix (reads-action) is required for the next-action function that only contains variables that are read during the action part.

Additionally, each guard predicate is split into its conjuncts and associated with the corresponding transition groups in the guard matrix. Each conjunct is added to the state labels announced to LTSmin and their accessed variables are stored in the state label matrix. Parameter constraints however are considered to be part of the action. E.g., the guard $n > 0 \wedge n< c \wedge y < c$ of $\mathtt {incy(n)}$ in Fig. 2 is split into two: only $y < c$ is the actual guard for LTSmin and $n > 0 \wedge n < c$ is evaluated when calling the next-action function. The new matrices and the new rows in the state label matrix can be found in Fig. 7. Differences between the read matrix from Fig. 3 and the reads-action matrix are highlighted in bold.

Fig. 7.

Matrices for guard-splitting

3.5 Partial Order Reduction

Partial order reduction (POR) [30, 31] is a technique that reduces the amount of considered states based on a property that is checked. This is achieved by making use of additional information that can usually be inferred by static analysis.

In the following, we describe which relationships need to be calculated in order to achieve the best reduction with LTSmin.

Definition 3

(According with, based on [24]). Let $t_{1}, t_{2} \in \mathcal {T}$ be any two operations. We define $t_{1}$ to be according with $t_{2}$, iff

$$\forall s, s_{1}, s_{2} \in \mathcal {R} : s \xrightarrow {t_{1}} s_{1} \wedge s \xrightarrow {t_{2}} s_{2} \implies \exists s^{\prime } : s_{1} \xrightarrow {t_{2}} s^{\prime } \wedge s_{2} \xrightarrow {t_{1}} s^{\prime }$$

or as graphical representation:

We define that no $t \in \mathcal {T}$ accords with itself.

Accordance of transition groups expresses that they are independent from each other, i.e., depending on the property, not all interleavings have to be considered. ProB underapproximates the according-with relationship. Instead, the constraint $\forall s, s_{1}, s_{2} \in \mathcal {S} : s \xrightarrow {t_{i}} s_{1} \wedge s \xrightarrow {t_{j}} s_{2} \implies \exists s^{\prime } : s_{1} \xrightarrow {t_{j}} s^{\prime } \wedge s_{2} \xrightarrow {t_{i}} s^{\prime }$ is evaluated for a given pair $t_{i}, t_{j} \in \mathcal {T}, i \ne j$, considering the guards and the before-after predicates of both transitions. This does not ensure that any state is reachable. However, it is a valid overapproximation of the does not accord relationship matrix that is passed to LTSmin by negating all entries.

LTSmin uses a heuristic in order to determine which of the calculated stubborn sets [30] might yield the best state space reduction. It requires a good approximation of the necessary enabling sets to do so:

Definition 4

(Necessary Enabling Set (NES), based on [24]). Let g be any state label that is disabled in some state $s \in \mathcal {R}$, i.e. $\mathbf {\lnot g(s)}$.

A set of transitions $\mathcal {N}_g$ is called the necessary enabling set for g in s, if for all states $s^{\prime } \in \mathcal {R}$ with some sequence $s \xrightarrow {t_{1}, \dots , t_{n}} s^{\prime }$ and $\mathbf {g(s^{\prime })}$, for at least one transition $t_{i}$ ($1 \le i \le n$) we have $t_{i} \in \mathcal {N}_g$.

We can use an already existing implementation of the procedure (cf. [14], definition 2) in order to calculate the necessary enabling set. In the implementation, it is just tested for any given state, whether a single transition can enable the guard label. In particular, this means that the states s and $s^{\prime }$ in Definition 4 may not be reachable at all. This results in a safe approximation but may lose precision.

Along with the NES, a necessary disabling set (NDS) is approximated. It is calculated in the same way but uses the negation of the state label.

Fig. 8.

Reduction using co-enabledness

Information about the NES and NDS matrices can syntactically be approximated from the dependency matrix. Solving the given constraints often results in a better approximation and, thus, a better reduction.

Furthermore, with additional information one might prove that out of at least three transition, e.g., $t_1, t_2$ and $t^{\prime }$, some transitions, e.g., $t_2$ and $t^{\prime }$ might not be enabled at the same time. Then, not all interleaving of $t_1$ and $t_2$ need to be considered. This situation is depicted in Fig. 8, where $s_1$ does not have to be visited. Then, a may-be co-enabled matrix is calculated, based on the following definition:

Definition 5

(Co-Enabledness, based on [24]). Two state labels $l, l^{\prime } \in \mathcal {L}$ are co-enabled in a state $s \in \mathcal {R}$ iff they both evaluate to true in s, i.e. $l(s) = \textit{true} = l^{\prime }(s)$.

Again, instead of working on reachable states, it is checked whether there is any state in the Cartesian product of types where both labels are enabled. If the co-enabledness of two state labels cannot be determined, they are considered as may-be co-enabled.

While ProB offers an implementation partial order reduction as well [15, 16], the partial order reduction algorithm implemented in LTSmin uses a finer heuristic. ProB checks whether a transition can enable another transition, LTSmin uses information about whether individual guards of the event can be enabled, often resulting in a better reduction.

However, this reduction comes with a tradeoff: to calculate the additional matrices, more constraints have to be solved by ProB in order to determine the additional relationships, resulting in a longer analysis time. ProB only calculates accordance of transitions and one row in the NES matrix per transition instead of per guard conjunct. Furthermore, LTSmin does not allow both transitions to be enabled and not generating any successors at the same time. This is possible in ProB when no suitable parameters exist. Thus, an additional guard is added which is an existential quantification of the parameters and often rather costly to evaluate. This quantification has to be solved both on evaluation of the guard and computation of successor states.

3.6 LTL Formula Checking

In order to check LTL properties, both tools need to have access to the formula: only ProB is capable of dealing with atomic propositions properly since it implements the syntax and semantics of the B language. LTSmin, however, requires the formula in order to generate the corresponding Büchi automaton.

Thus, ProB parses the formula first. All atomic propositions in the formula are replaced with a newly generated state label. In order to evaluate these new atomic propositions, the state labelling function is extended in ProB. Furthermore, the formula is wrapped in a “next” operator in order to skip the artificial initial state introduced earlier. This modified formula is then pretty printed into a format that LTSmin can parse.

4 Evaluation

In this section, we will evaluate the performance of the tool integration of LTSmin and ProB using both the sequential and symbolic backend. We will compare the model checking time on several models from literature and industrial applications which are publicly available under https://github.com/pkoerner/prob-ltsmin-models. Benchmark scripts are included in the repositories as well.

Furthermore, we will compare the impact of the implementations of partial order reduction for a different set of models, where the state space can be reduced.

Each benchmark was run on a machine featuring two Intel Xeon IvyBridge E5-2697 with twelve cores each running at 2.70 GHz and 100 GB of RAM. Two CPUs were reserved for each run of invariant verification, partial order reduction and LTL model checking. For multi-core benchmarks, we reserved as many CPUs as there are worker threads plus one CPU for ZeroMQ overhead.

The given values are the median value of ten repetitions.

4.1 Invariant Checking

We benchmarked three backends on multiple B and Event-B models:

• ProB: the vanilla ProB model checker

• LTSmin (seq): the sequential backend of LTSmin with the ProB interpreter,

• LTSmin (sym): the symbolic backend of LTSmin without guard-splitting and the ProB interpreter.

We omit results with guard-splitting enabled since they are very similar to the symbolic backend without guard-splitting for applicable models, i.e., those written in classical B.

Runtimes and memory consumption can be found in Table 1. Runtimes of LTSmin’s sequential and symbolic backend do not include ProB’s startup time which includes parsing and minor analysis of the model. None of the considered models has any invariant violation and, thus, all models have to be explored exhaustively.

Table 1. Invariant checking performance (runtime in seconds, memory in MB) of ProB alone compared to LTSmin with ProB. $\dag$: Estimated runtime, $\ddag$: limited amount of initializations

Only for one of models benchmarked, the “Set Laws” machine, a single backend of LTSmin is slower than ProB. Apart from that, we can observe speed-ups ranging from two-fold up to more than two hundred times. For most models, LTSmin is at least an order of magnitude faster than ProB.

The “Train” machine cannot be checked by vanilla ProB on the benchmarking machine, as it runs out of main memory after three days, exploring about half the state space. Both LTSmin backends manage to verify the entire state space in several hours. Only in few instances, LTSmin requires more memory than ProB. Surprisingly, the sequential backend often requires an order of magnitude less memory, even though it maintains a cache. In the only instance where it uses more memory, i.e., “Earley Parser”, only few variables re-use the same values. Thus, almost no sharing between in states is possible and the entire fastrw representation for almost every state has to be stored.

Overall, LTSmin is able to outperform ProB in almost all instances. Obviously, caching is really important for the sequential backend. We tried two implementations of a similar caching mechanism for ProB in order to benefit from similar speed-ups: firstly, by hashing short states as well as asserting them as Prolog facts, and, secondly, by serializing the state via the fastrw library and storing the result in a hash map in C. However, neither implementation had a similar impact. Often, they even slowed ProB down. In the first case, we assume that the hashing algorithms for Prolog terms are too slow. For the second implementation, the overhead to serialize every state, in particular for cache lookups, was too costly.

4.2 LTL Model Checking

We benchmarked LTL model checking on a few of aforementioned models that are reasonably sized. Since no LTL formulas were included in the models, we arbitrarily picked some that allow reasoning about the models. ProB’s special syntax is used in the formulas: e(x) means that the operation x is enabled. The results are given in Table 2.

We can see that for LTL formulas that hold, the good speed-ups and low memory consumption of LTSmin that was presented in Sect. 4.1 can also be observed for LTL model checking. If a formula is not satisfied, LTSmin can be more than thousandfold faster. While ProB generates the state space of the transition system first, LTSmin features an on-the-fly LTL model checking algorithm where the state space consisting of the Cartesian product of the corresponding Büchi automaton and the actual transition system is generated as necessary. Thus, accepting loops can be found quickly without exploring the entire transition system and speed-ups may be more than thousandfold.

Table 2. Runtimes (in seconds) and speed-ups of LTL model checking. $\dag$: LTL formula does not hold. Speed-up compared to ProB without LTSmin.

4.3 Partial Order Reduction

From benchmarks conducted in [16, 20], it became clear that, in typical B and Event-B models, partial order reduction usually does not work well in combination with invariant verification. For the models above, none or very little reduction was achievable. Instead, we compare the results of partial order reduction for deadlock checking.

In ProB, we use the “least” heuristic for the partial order reduction. In order to reduce analysis time for LTSmin, the timeout is set to 20 ms per predicate.

Results are shown in Table 3 comparing the performance of ProB’s POR for deadlock checking with the one of LTSmin. B models that offer no reduction with either tool are omitted (which are more than half). Again, the startup time of ProB that includes parsing the machine file, is not included.

Table 3. Runtimes (in seconds) and impact of POR in ProB alone and LTSmin with ProB for deadlock checking.

As can be seen in Table 3, LTSmin is – as discussed in Sect. 3.5 – able to find a reduction that is equal to ProB’s or even better (for the “Set Laws” machine, the additional state is the artificial initial state). Indeed, for the “Mercury Orbiter” and “Landing Gear”, ProB cannot reduce the state space at all with the given heuristic, whereas LTSmin reduces the state space by about a quarter up to a half.

However, fine-tuning of the time-outs for the static analysis is important. For machines with many unique guards, analysis time can easily exceed model checking time. This can be observed for the “Landing Gear” and the extremely reduced “Four Slot”. With the default time-out value of 300 ms, the analysis time of the “Mercury Orbiter” can exceed a minute, which is more than four times the time required for model checking without any reduction. A reason could be that the constraint solver cannot solve the necessary predicates easily and time-outs are raised often.

4.4 Multi-core Model Checking

In order to evaluate the performance of the multi-core backend, we performed multi-core invariant verification on the five B models with the largest runtime in Sect. 4.1.

The runtime of runs with different amount of workers are shown in Table 4. Speed-ups are visualized in Fig. 9. This time, ProB’s startup time is included because the multi-core extension of LTSmin starts up ProB.

Fig. 9.

Speed-ups of multi-core LTSmin+ProB model checking for complex models

Table 4. Runtimes (in seconds) and speed-ups of multi-core LTSmin with ProB model checking on the high-performance cluster. $\ddag$: Limited amount of initializations

Currently, each worker thread maintains its own cache. Since caching works fairly well for many B machines, it is quite costly to fill each cache individually. This explains that often, for the first few workers the speed-up is nearly linear, but grows slower when more than ten workers participate.

An exception is the “Earley Parser”: the standalone sequential backend does not offer much speed-up (cf. Sect. 4.1). Thus, the caching effects are lower. Additionally, ProB spends much time deserializing the state variables because the Prolog terms grow quite large. Hence, a more linear speed-up is possible for many workers.

5 Conclusion, Related and Future Work

In this paper, we presented and evaluated significant improvements of the existing link of ProB and LTSmin. It allows state-of-the-art model checking of industrial-sized models with large state spaces, where the vanilla ProB model checker struggles due to time or memory constraints. E.g., the “Train” example can only be checked successfully with ProB on its own by distributing the workload onto several machines, whereas with LTSmin, it could be verified on an ordinary notebook or workstation.

We have compared symbolic reachability analysis to the impact of alternative techniques that can speed up state space generation, e.g., partial order reduction and symmetry reduction in [4]. A discussion of the impact of algorithms that are implemented in both LTSmin and ProB can also be found in Sect. 4.

Additionally, there is another toolset named libits [12]. It supports, like LTSmin, symbolic model checking using decision diagrams, variable reordering and LTL as well as CTL model checking. As we understand, its input formalisms are translated into its guarded action language (GAL). An integration for B might prove to be infeasible because a constraint solver is required in order to compute some state transitions and would have to be implemented in GAL itself. We do not know yet whether linking ProB with libits in order to compute state transitions is possible.

The caching performed by LTSmin seems to be particularly efficient. For several realistic examples, the ProB and LTSmin link achieves two to three orders of magnitude improvements in runtime. Yet, there are several aspects that require future work: currently, the ProB front-end of LTSmin does not support parallel symbolic model checking with Sylvan [32]. Furthermore, caches are local per worker. A shared cache will most likely improve the scaling for massive parallel model checking. Additionally, the cache does not implement R2W semantics, which loses information about write accesses and requires more memory and additional state transformations.

Moreover, there is room for interesting research: while we know from experience that, for most B models, partial order reduction often only has little to no impact on the state space, we are unsure why. Would alternative algorithms perform better? Is the constraint solver not strong enough? Is the approximation given to LTSmin not precise enough? Does partial order reduction not perform with the modeling style employed in B? If so, are there any patterns which hinder it? Additionally, a proper survey of distributed model checking of B and Event-B specifications – which we did not touch upon due to page limitations – between, e.g. LTSmin’s distributed backend, ProB’s distb [21] and TLC [35] should be considered.

With the gained experience and shared know-how about both LTSmin and ProB, we now aim to extend the implementation for CSP$\parallel$B, where the execution of classical B machine is guided by a CSP specification. While ProB provides both an animator and model checker for this formalism, ProB currently is not a satisfactory tool for this formalism. Interleaving of several processes causes an enormous state space explosion that we hope the symbolic capabilities of LTSmin can manage.