Towards a Model-Checker for Circus

Abstract

Among several approaches aiming at the correctness of systems, model-checking is one technique to formally assess system models regarding their desired/undesired behavioural properties. We aim at model-checking the notation that combines Z, CSP, and Morgan’s refinement calculus, based on the Unifying Theories of Programming. In this paper, we experiment with approaches for capturing processes in CSP, and for each approach, we evaluate the impact of our decisions on the state-space explored as well as the time spent for such a checking using FDR. We also experimented with the consequences of model-checking CSP models that capture both state invariants and preconditions of models.

1 Introduction

The use of formal methods provides a way to rigorously specify, develop, and verify complex systems. Among several approaches aiming at the correctness of systems, model-checking formally assesses given systems regarding their desired/undesired behavioural properties, through exhaustive checking of a finite model of that system.

Woodcock and Cavalcanti defined  [38], which is a formal language that combines structural aspects of a system using the Z language [40] and the behavioural aspects using CSP [36], along with the refinement calculus [23] and Dijkstra’s guarded commands [10]. Its semantics is based on the Unifying Theories of Programming (UTP) [18]. In addition, a refinement calculus for was developed by Oliveira [27], currently considered the de-facto reference for , using tool support with ProofPower-Z [28]. More recently, Foster et al. introduced Isabelle/UTP, supporting  [11]. Moreover, has a refinement calculator, CRefine [8], and an animator for , Joker [26]. However, for model-checking, is usually translated by hand to machine-readable CSP ($CSP_M$) [35] and then FDR [14] is used. We applied that method in our response to the Haemodialysis case study for ABZ’16 [16]. Model checking through FDR allows the user to perform a wide range of analysis, such as checks for refinement, deadlock, livelock, determinism, and termination.

Some related work on techniques for model-checking was presented by Freitas [12] where a refinement model checker based on automata theory [19] and the operational semantics of  [39] was formalised in Z/Eves [34]. He also prototyped a model checker in Java. Moreover, Nogueira et al. [24] also presented a prototype of a model checker based on the operational semantics of within the Microsoft FORMULA [21] framework. However, they could not provide a formal proof of the soundness of their approach, since FORMULA does not have an available formal semantics. Yet another approach for model-checking was defined by Ye and Woodcock [41], who defined a link from to $CSP\Vert B$ with model-checking using ProB [31]. Finally Beg [4] prototyped and investigated an automatic translation that supports a subset of constructs.

Since $CSP_M$ does not have a notion of variables for state as in Z, or even the B-Method, we have to somehow capture them in order to obtain a $CSP_M$ model as similar as possible to the original one. Therefore, one could either use a memory model [25, 30] in order to manage the values of the state variables, or else, to adopt the idea of state-variable parametrised processes [4].

Following the results presented in ABZ’16 [16], which involved manual translation, we decided to develop ¹, an automatic translator from into $CSP_M$, aiming at model-checking with FDR. Our tool was then built based on the strategy presented in Sect. 5.3 of Deliverable 24.1 [29], from the COMPASS project [37], that defines a rigorous but manual translation strategy aiming at obtaining $CSP_M$ specifications from .

This paper reports design decisions regarding different approaches for model checking and experimental results obtained for specifications. Such experiments were enough to identify an effective general form for any $CSP_M$ model derived from , where FDR could perform refinement checks with reduced time and memory consumption compared to existing approaches from the literature.

2 Background

A specification is in some sense an extension of Z [40] in that it takes the paragraphs of Z and adds new paragraph forms that can define channels, processes and actions. Channels correspond to CSP events:

$$\begin{aligned} \mathbf{channel }\,\,c : T \end{aligned}$$

actions can be considered as CSP processes extended with the ability to read and write shared variables, usually defined using a Z schema:

$$\begin{aligned} LocVars \mathrel {\widehat{=}}[v_1 : T_1, \dots , v_n : T_n] \end{aligned}$$

A process is an encapsulation of process-local shared variables and actions that access those local variables, along with a ‘main’ action.

$$\begin{aligned}&\mathbf{process }\,\,ProcName ~\mathrel {\widehat{=}}~ \mathbf{begin }\\&\qquad \mathbf{state }\,\,PState == LocVars\\&\qquad PBody ~\mathrel {\widehat{=}}~ \langle \text {action defn.} \rangle \\&\qquad PInit ~\mathrel {\widehat{=}}~ \langle \text {action defn.} \rangle \\&\qquad PMain ~\mathrel {\widehat{=}}~ PInit ;PBody\\&\quad \bullet \,\,PMain\\&\mathbf{end }\end{aligned}$$

processes can only communicate with the external environment via channels, while actions can also communicate via the local variables of their containing process. Processes can be modified and combined with each other, using the following CSP operators: sequential composition (;  ), non-deterministic choice ($\sqcap$), external choice ($\Box$), alphabetised parallel ($[\![\dots ]\!]$), interleaving ($|||$), iterated versions of the above (e.g., $\sqcap _{e \in E} \bullet \dots$), and hiding ($\mathbin \backslash$).

  actions can be built with the CSP operators detailed above, as well as the following CSP constructs: termination ($\text {Skip}$), deadlock ($\text {Stop}$), abort($\text {Chaos}$), event prefix ($\rightarrow$), guarded action (&), and recursion ($\mu$). In addition a action can be defined by a Z schema, or Dijkstra-style guarded commands, including variable assignment ($:=$). Note that actions cannot be defined as standalone entities at the top level of a specification.

Parallel composition of actions differs from that in CSP, in that we need to also specify which variables each side is allowed to modify. Parallel action composition, written as $A_1\, [\![\, ns_1\, |\, cs\, |\, ns_2\, ]\!]\, A_2$ states that action $A_i$ may only modify variables listed in $ns_i$, where $ns_1$ and $ns_2$ are disjoint, and both actions must synchronise on events listed in cs. The semantics is that each side runs on its own copy of the shared variables, and the final state is obtained by merging the (disjoint) changes when both sides have terminated.

  also allows the use of local declarations in a variety of both process and action contexts. For actions, we can declare local variables, using $\mathbf{var }\,\,x:T \bullet \,\,A$ which introduces variable v of type T which is only in scope within A. Variations of these can be used to define parameterised actions, of which the most relevant here is one that supports read-write parameters.

Finally, there is a refinement calculus for , which is a fusion of those for both Z and CSP (failures-divergences)[27].

3 Translating to $CSP_M$ using

Our first attempt to model check the haemodialysis (HD) specification [16], was to manually translate it into $CSP_M$, and adjust its state-space until the desired checks could be successfully completed. This manual translation was error-prone, and this motivated the development of a mechanised translator. Our plan was to provide a high degree of automation to minimise error-prone human interventions, in such a way that we have a basis for arguing for its correctness.

We started the development based on the translation strategy developed for the EU COMPASS project and described in deliverable D24.1 [29, Section 5]. It specifies the translation in two parts: a function $\varOmega$ that maps a specification to an equivalent specification using only the CSP subset of the language; and a function $\varUpsilon$ that translates CSP-as- into machine-readable $CSP_M$ (Fig. 1).

Fig. 1.

(derived from [29, Fig. 7, p77])

Mapping into $CSP_M$

Function $\varOmega$ has two phases: $\varOmega _P$ and $\varOmega _A.$ Function $\varOmega _P$ extracts mutable state from the input state-rich ($Circus_{SR}$) process $P_{SR}$ and gathers it in a new Memory action, while replacing direct references to state in $P_{SR}$ with appropriate “get” and “set” messages that communicate with that Memory, to obtain a state-poor ($Circus_{SP}$) process $P'_{SP}$. Function $\varOmega _A$ then translates $P'_{SP}$ into its CSP equivalent $P''_{SP}$, by replacing -specific actions by CSP-as- ($Circus_{CSP}$) equivalents. All of the transformations done by $\varOmega _P$ and $\varOmega _A$ are valid refinement steps, each of which are in fact equivalences, defined in D24.1 [29, §5.3 and App. A].

3.1 The Memory Model

The need for a memory model arises from the fact that CSP does not naturally capture the notion of mutable state. One solution for that is to produce a state-poor process that communicates with a Memory model [25] that stores the values of state components and local variables from the original state-rich processes. Initially, our memory model was very similar to that in D24.1, with some differences in naming conventions. In our approach, we defined a notation for renaming the variables allowing the user to easily identify which are (global) state components, or local variables. Variables are renamed by adding a prefix $sv\_$ or $lv\_$ indicating respectively a state or local variable.

As part of the translation strategy, the $CSP_M$ environment is redefined in terms of the type system. Based on the work of Mota et al. [25], D24.1 defined a union type UNIVERSE containing any type defined in the specification. When translated into $CSP_M$, use is made of the subtype facility of that language to manage the universe construction. Moreover, the names of every state component and local variable are defined as elements of a type NAME.

$$\begin{aligned} NAME \,::\,= sv\_v_1 | sv\_v_2 | \ldots | sv\_v_n | lv\_l_1 | \ldots | lv\_l_k \end{aligned}$$

The approach makes use of a set of bindings, BINDING, which maps all the names, NAME, into the UNIVERSE type. In [29], a function $\delta$ is defined as a mapping between each variable in NAME and its type, where each type ($T_i$ is a subtype of UNIVERSE), and is used to define Memory.

$$\begin{aligned}&BINDING == NAME \rightarrow UNIVERSE\\&\delta == \{sv\_v_1 \mapsto T_1, sv\_v_2 \mapsto T_2, \ldots , sv\_v_n \mapsto T_3 , \ldots , lv\_l_k \mapsto T_m \} \end{aligned}$$

As a result of applying the $\varOmega$ functions, the state of a process is replaced by a Memory action parameterised by a read/write binding ($\mathbf{vres }\,\,b$), which manages the mutable state, offering mget and mset channels carrying name/value pairs (n.v).

$$\begin{aligned}&Memory \mathrel {\widehat{=}}\mathbf{vres }\,\,b:BINDING \bullet \,\,\\&\qquad (\Box n:\mathrm {dom}\,\,b \bullet \,\,mget.n!b(n) \rightarrow Memory(b)) \\&\qquad \Box ~(\Box n:\mathrm {dom}\,\,b \bullet \,\,mset.n?nv:(nv \in \delta (n)) \rightarrow Memory(b \oplus \{n \mapsto nv\}))\\&\qquad \Box ~terminate \rightarrow \text {Skip}\end{aligned}$$

Note, that while syntactically a action, Memory uses only the CSP subset of Such a Memory process runs in parallel with the main action of the translated process, communicating through the channels mget and mset. Moreover, the process execution ends when the terminate signal is triggered. The above three channels compose the $MEM_I$ channel set: .

The final specification puts the original process after $\varOmega$-translation in parallel with the memory model, synchronising on the $MEM_I$ channels, which are themselves hidden at the top-level, with the binding as a top-level parameter. Note that the semantics of this at the top-level involves a non-deterministic choice² of the values in the initial binding b. This results in the following CSP form:

$$\begin{aligned} \sqcap b : BINDING \bullet \,\,\left( \begin{array}{l} (\varOmega _A(P) ; terminate \rightarrow \text {Skip}) \\ \parallel _{MEM_I} Memory(b) \end{array}\right) \backslash MEM_I \end{aligned}$$

Deliverable D24.1 contains manual proofs of the correctness of the translation [29, Appendix K].

4 Upgrading the Memory Model

With the initial version of the tool, we took examples from D24.1 (e.g. the ring-buffer example [29, Appendix D.2, p163]) and automatically translated them and then succesfully performed FDR checks. However, when we turned our attention to the somewhat larger HD model, we immediately uncovered some limitations of the basic translation, which were overcome by changing the memory model.

4.1 Limitation 1: Z Types vs. $CSP_M$ Types

The use of the UNIVERSE type, the $CSP_M$ subtype feature, and a function written in $CSP_M$ to map a name to its specific type, worked fine if all the types in UNIVERSE were a sub-type of one supertype. In the D24.1 examples, all types were sub-types of the natural numbers. However, in the HD model we were developing, we had a mixture of natural sub-types, and enumerations. The type system in $CSP_M$ does not consider enumeration types to be isomorphic to subtypes of any sufficiently large number type. We could have generated those isomorphisms, but these would have complicated the back-annotation problem, whenever a counter-example was found using FDR. Instead, we partitioned UNIVERSE and BINDING into the distinct supertypes present in the model.

We then changed the top-level view to have a non-deterministic choice over all the distinct bindings.

$$\begin{aligned}&\sqcap b_{T_1}:BINDING_{T_1}, \dots , b_{T_k}:BINDING_{T_k}\\&\qquad \bullet \,\,\left( \begin{array}{l} (\varOmega _A(P) ; terminate \rightarrow \text {Skip}) \\ \parallel _{MEM_I} Memory(b_{T_1}, \dots , b_{T_k}) \end{array}\right) \backslash MEM_I \end{aligned}$$

4.2 Limitation 2: FDR Time/Space Explosion

We quickly discovered that using this translation, we could only check models with a small number of state variables, usually less than ten, with even the hand-translation of the HD model done for the original case-study being more effective. We proceeded to experiment with transformations to the memory model, justified by the refinement laws.

Variables Have Non-deterministic Start Values. We first changed the top-level non-deterministic choice over the various bindings by replacing it with parameters.

$$\begin{aligned}&\mathbf{var }\,\,b_{T_1}:BINDING_{T_1}, \dots , b_{T_k}:BINDING_{T_k} \bullet \,\,\\&\qquad \left( \begin{array}{l} (\varOmega _A(P) ; terminate \rightarrow \text {Skip}) \\ \parallel _{MEM_I} Memory(b_{T_1}, \dots , b_{T_k}) \end{array}\right) \backslash MEM_I \end{aligned}$$

This is an equivalence, as $(\mathbf{var }\,\,x:T \bullet \,\,A(x)) = (\sqcap x:T \bullet \,\,A(x)$). However, FDR treats the latter as being parameterised by x and requires it to be given an initial value. This means that we can only check a very strong proper refinement, rather than the full equivalence. However, we argue that in the safety-critical domain in general, it is always mandatory to initialise all variables. If Init is an action that initialises each variable precisely once with a constant value, with no intervening participation in events, then, regardless of the assignment ordering or any arbitrary initial value of any variable, the outcome is always the same: $s' = S_0$, where $S_0$ is the assignment of those constants to the coprresponding variables. If we insist on proper initialisation, then equivalence is restored. Given that the main usage of model-checking takes place in safety critical domains, we consider this a reasonable trade-off, particularly because it resulted in FDR performance improvements. However, our experiments revealed that a process translated this way, with more than ten state variables, still could not be checked with FDR in a reasonable time.

Distributed Memory Model. The final step, was to do more partitioning, moving to a situation were every variable gets its own memory process. The supertype bindings were retained at the top-level, but each variable’s memory process was parameterised by the relevant binding with its domain restricted to just the name of that variable. So, for example, if variable $n_i$ has a type whose supertype is T, then we first define a binding $b_T$ for that supertype, and use it to parameterise a memory action for all variables of that supertype, which is itself the parallel composition of a memory process for each such variable, all synchronising on terminate, but interleaving all the mget and mset events:

Here $N \vartriangleleft \mu$ restricts the domain of map $\mu$ to set N. We then define a parameterised process that represents a single variable:

$$\begin{aligned}&MemoryTVar(n,b) \mathrel {\widehat{=}}\\&\qquad mget.n.b(n) \rightarrow MemoryTVar(n,b) \\&\quad \Box ~ mset.n?nv:\delta (n) \rightarrow MemoryTVar(n,b \oplus {n \mapsto nv}) \\&\quad \Box ~ terminate \rightarrow \text {Skip}\end{aligned}$$

The entire memory is constructed by putting the memories for each supertype in parallel, in the same way as for the individual variable processes.

This last transformation produced a marked improvement in the time and memory consumption of FDR when checking models.

In the next section we describe and discuss our experiments on the HD machine mode comparing some of approaches above. Moreover, we also compare the results obtained using other tools as a way of assessing our results.

5 Experimental Results

In this section we present the tests we performed using our tool, , exploring ways of overcoming any limitations from FDR, as well as comparing our approach with others from the literature. Firstly, we explore the interference of invariants and preconditions in $CSP_M$. Then, we compare with the model from [16]. We also the effects of using some compression techniques available in FDR. Finally, we compare different approaches for modeling the Ring Buffer case study.

One of the requirements when model-checking a system is to produce a model whose range of values is enough for covering any condition imposed by an operation. However, when including the state invariant, we are also restricting the range of values permitted to be used within the system. From the example of the chronometer [27], we know that both min and sec was declared as natural numbers. However, while thinking of a chronometer in the real world, we know that neither a second, nor a minute goes beyond 59 units, without flipping the next unit counter. Therefore, it is safe to restrict the range of min and sec to $0 \,..\,~60$, where 60 is an unexpected value in the system.

We experimented with the impact of explicitly including invariant and precondition checks using the example of the Chronometer [27], with a new process Chrono. When using the translation rules presented in [29], we noticed that it is hard for FDR to check the model: it was translated using the conversion from normalised schemas to specification statements and from there, to the appropriate rules that introduce a condition that checks if pre is satisfied. If satisfied, it behaves as a non-deterministic choice of values from the state variables that satisfies both invariant and precondition, followed by updating these values in the memory model. Otherwise, if pre is not satisfied, it behaves like Chaos.

Our example of the chronometer has only two state variables and the results obtained using FDR are enough to show how the invariant checks throughout the specification increase the time spent during the assertion check in FDR. We deliberately modified the original model with the inclusion of the state invariant restricting both min and sec to values below 60, in order to experiment with the translated model in FDR.

We illustrate our experiment in Table 1 while exploring the inclusion of state invariants and precondition verification in the chronometer model, and used the following derived models³:

D241:

Model manually translated using the approach from [29] without invariants and preconditions, using a non-deterministic choice of any set of bindings.

D241Inv:

Model manually translated using the approach from [29] including the invariants as a restriction to the bindings set.

D241Pre:

Model manually translated using the approach from [29] which includes precondition checks before the operations, but no invariants in the main action.

D241InvPre:

Combination of D241Inv and D241Pre.

CTOC:

Model translated using our improved translation rules, the result from our tool , as discussed in Sect. 4 (no invariant checks).

CTOCPre:

Extension of CTOC model where pre-condition checks, as done for D241Pre, are entered manually.

From the models above, our tool is able to automatically generate CTOC, CTOCPre was obtained by manually modifying CTOC, while the others were generated by hand. We performed checks for deadlock freedom⁴ using the translated models in the six variants above, combined with a different range of values for natural numbers, ranging from $\dots 3$ to $0 \dots 60$. For example, in a specification where the values for natural numbers are restricted to the range $0\,..\,10$, the process state was defined as $[min, sec: 0\,..\,10 \,|\, min< 10 \wedge sec < 10]$.

Table 1. Interference of invariants and preconditions in $CSP_M$—Deadlock freedom checks (in seconds unless indicated otherwise)

We noticed a first difference between models D241 and D241Inv, on one hand, and CTOC and CTOCPre on the other. The number of states visited for checks with the models D241 and D241Inv was over 10-fold larger than for CTOC and CTOCPre. However, the influence of a precondition check within an operation makes a significant reduction in the state exploration, but with the price of spending more time computing preconditions, as seen in Table 1, between CTOC and CTOCPre. Moreover, we also observed that the checks for invariants has a weaker effect on states visited, when comparing the results between D241InvPre and D241Pre. We also noticed that all variants of D241 were executed in a much larger time frame than the approaches using the translation from our tool, . However, the models generated by our tool do not include either invariants or preconditions.

Finally, as a way of experimenting with the real world example of the chronometer, we examined the models with numbers ranging from 0 up to 60, as presented in the last row of Table 1. We see a significant difference among the results from the approaches evaluated, where the model using CTOC was evaluated (3 min) by FDR, which is 97% less time than the time spent to check the model using D241Inv (over 1h40) and 94% less than D241Pre (1h05). In general, the $CSP_M$ models (CTOC) translated using our tool were evaluated by FDR using a much smaller state space and were checked in less time than all the other models we tried. Such a result shows how different models of the same system can be affected by the checks of invariants and preconditions, as well as how optimising the memory model can result in much smaller state exploration when using FDR. Finally, we observed no correlation between time and state visited, in spite of the use (or not) of compression by default in FDR.

5.1 Haemodialysis (HD) Machine Experiments

The manual translation (herein byHand) of the  [16] HD model resulted in a $CSP_M$ specification with twice as many lines as the model. Using the CTOC translation results in $CSP_M$ with approximately 75% fewer lines than the corresponding file.

Our reference model was that of the HD machine running in parallel with a model of one of the case study requirements (R-1 [2, Section 4.2, p11]). The requirement model is effectively a monitor that observes the machine model, checking that it is satisfied, and deadlocking if it observes a violation. We then check the proposition that the HD model is correct w.r.t R-1 by showing that the combination is deadlock free. In addition to comparing various translation schemes, we also explored the effect of changing the size of our “natural number” type: $NatValue == 0 \,..\,N$, in order to estimate the number of states visited in FDR.

We explored the byHand and CTOC translation schemes with four ranges of NatValue size, with N up to a maximum of 90, as shown in Table 2. The only case where we could compare the two approaches was our first case, with $N=2$: it resulted in 9,409 states visited using byHand, in contrast with 811 states visited using CTOC, demonstrating a reduction of 91% in terms of states explored. Moreover, the execution time with the model generated using CTOC was equally reduced by 91% compared to the model using byHand. The “Plys” column indicates how deep the breadth-first search algorithm used by FDR went while checking. This is larger for the byHand model, and is independent of the value of N. Interestingly, after waiting more than 2 h, we were unable to obtain results from the model generated with byHand when we increased the N to 3. However, the model generated with CTOC, when tested using $n=90$, was executed in 35 s, which is still quicker than byHand with $N=2$. We also note that amount of memory used was constant, at 240 MB approx.

Table 2. Time for asserting deadlock freedom of the HD Machine in FDR4

We could not get results here for the D241 scheme as its translation of the HD model resulted in type errors being reported by FDR.

In addition to experiments that varied N above, we also explored how the number of variables, rather than the size of their datatypes, influenced the checking time. Using a hypothetical example having 12 state variables, checks using D241 were performed in 35 min, compared to 76 ms using CTOC. We observed segmentation faults using D241 with a more than 12 variables. However, checks using CTOC in an example with 42 state variables and $NatValue = 0\,..\,30$, were performed in 870 ms. What is clear is that with the CTOC translation scheme, namely one memory-process per state-variable, we can now handle models of considerable complexity.

5.2 Ring-Buffer Experiments

Another interesting example was to take the specification of the bounded reactive ring buffer, RB, from D24.1 [29, Appendix D.2, p. 163], based on the model presented in [7]. We compared the CTOC translation of this using  ($RB_{CTOC}$), with the by-hand translation in D24.1 [29, Appendix D.4, p166] ($RB_{CTOC}$). We firstly perform the usual tests like deadlock freedom and termination checks for $the RB_{CTOC}$ and for the $RB_{CTOC}$ specifications, as illustrated in Table 3.

Table 3. RingBuffer checks: deadlock and livelock freedom, and determinism.

We can see a clear difference between the states visited between the three approaches, notably those between $RB_{byH}$ and $RB_{CTOC}$ where the number of states and transitions visited was reduced considerably, as well as the amount of time spent by FDR4 to check the assertions.

We also experimented to check the failures-divergences refinement ($P \sqsubseteq _{FD} Q$) between the three approaches, each pair in both directions. Since we know that the specification $RB_{CTOC}$ is a translation from the same model of the handmade translation of $RB_{byH}$, we expect that $RB_{byH}$ and $RB_{CTOC}$ are equivalent to each other, $RB_{byH} \sqsubseteq _{FD} RB_{CTOC}$ and $RB_{CTOC} \sqsubseteq _{FD} RB_{byH}$, which is true, as seen below in row 1 and 3.

Table 4. Refinement checks between models of the Ring Buffer example

Interestingly, if we compare the states and transitions visited, as well as the execution time from Tables 3 with 4, given a refinement $A \sqsubseteq _{FD} B$, the states and transitions visited are almost the same as when checking B for deadlock freedom.

During our experiments, we also compared our model with the Ring Buffer model $RB_{KW}$, based on [40, Chapter 22], produced using the approach of Ye and Woodcock [41] for translating into CSP||B, for model checking using ProB [22]. Such an approach is similar [29, p. 116] but makes use of Z schemas as actions that are currently not available in our translation scheme. In our experiments, we observed that the model $RB_{KW}$ is refined by both $RB_{CTOC}$ and $RB_{byH}$, but the refinement in the reverse direction does not hold, i.e., $RB_{KW}$ is not a refinement of neither $RB_{CTOC}$ nor $RB_{byH}$, as it is a more abstract model since its data aspects of specification are defined in B.

Unfortunately, the structure defined for our translation strategy is not fully supported by ProB, which was used to test $RB_{KW}$ [42]. ProB is another model-checker, which like FDR, also allows the user to animate specifications. It was originally developed for the B language, but it has been extended and now it supports other formal languages such as CSP, Z, Event-B [1], as well as combined languages such as CSP||B. We observed that the use of subtype, in our models, is not fully supported by the ProB tool, causing some commands like “model-check” to result in errors. However, we were able to animate our translated specification using ProB, and to execute the same assertion check, as in FDR: we obtained similar results to those when running FDR.

On the other side, the tests performed with the $CSP_M$ specification of $RB_{KW}$ using FDR failed the checks for deadlock freedom and determinism. The results obtained from ProB can be related to what we obtained in FDR in terms of the behavior of the system: the counterexample given can be used to animate the CSP||B model in ProB, causing the same effect: deadlock. However, we have no way to fully compare both approaches since CSP||B takes into account the system state in ProB, whereas we only have the $CSP_M$ side of the model, which captures the behavior of the system, but does not captures the system state. The most obvious explanation for the deadlock in $RB_{KW}$ is that the state (modeled in B) influences control-flow that results in deadlock situations being avoided.

5.3 Compression Experiments

An important aspect when using FDR is the availability of compression techniques [33] in order to reduce the number of states, reducing the time spent for refinement checking. A compression transforms a labelled-transition system (LTS) into a corresponding one, which is expected to be smaller and more efficient whilst using it for checks in FDR. Currently, FDR applies compressions in parallel compositions by default, which is the main structure we use in our memory model. We explored a few other compression tecniques, such as sbisim, which determines the maximal strong bisimulation [5], and wbisim, which computes the maximal weak bisimulation. Depending on the compression used, the number of states visited, were indeed reduced, as illustrated in Table 5.

Table 5. Experimenting $CSP_M$ compression techniques with the HD Machine

Although the states/transitions/plys visited were considerably reduced using the compression techniques mentioned above, there was little impact on overall execution time, and the number of states visited are independent of the size of NatValue, while the number of transitions grows slowly. However, the results obtained here are related to the model of the HD machine, and it is difficult to identify which compression technique will be most effective in a general case, and indeed, further experiments are required.

6 Future Work

Our plans for future work include exploring other industrial-scale case studies [3, 15, 17], as a way of identifying the kind of constructs that would be suitable to have available in our translation tool. We have a particular interest in specifying a translation strategy for Z schemas used as actions within a process. The best approach would be to use Z Refinement Calculus [6]. For now, our tool deals only with those schemas that in fact can be translated into assignments. We intend to explore the operators for Z schemas and the refinement laws that can be applied accordingly.

In addition, we also plan to establish a link between and Isabelle/UTP [11], so that we can use their mechanised UTP semantics for to verify the correctness of our Haskell implementation. Moreover, our tool also has a refinement “calculator” embedded in it, which implements the laws listed in Appendix A of the Deliverable 24.1 [29, p.147], which can easily be extended to the other refinement laws proved by Oliveira [27] in the near future.

We can eliminate the use of $CSP_M$ subtyping in CTOC (the process-per-variable model), and simplify “get” and “set” prefixes of the forms mget.n.v and mset.n.v to $get\_n.v$ and $set\_n.v$ respectively, where we now have dedicated channels per variable. However, the relationship of this new form to CTOC is no longer a simple equivalence as there are now different events in the two models.

Finally, in terms of improvement of our tool, compared to other approaches [9], it would also be interesting to review the parser of Z and from in order to rewrite it to be in conformance with the International Standards Organization (ISO) standards, ISO/IEC 13568:2002 [20], which describes the syntax, type system and semantics of Z formal notation. Moreover, we would like to include the libcspm library⁵ into in order to be able to parse the relevant code included in our definition of the assertion LaTeX environment. Such an attempt would help a user wishing to review any fault in the $CSP_M$ specification translated from .

Finally, we can envisage work in the future that might extend the benefits gained here to the wider model-checking community. One possibility is extending the translator to target model-checkers other than FDR. This would require us to have either a rigourosly defined embedding, of the subset of CSP that we produce, into the modelling language of the proposed checker, or have a way of linking the semantics of the target modelling language to and/or CSP to verify the correctness of direct output in that language. The second aspect concerns the possibility that our approach can be adapted to work within another model-checking eco-system entirely. ne key advantage in having a state-rich form is the ability to easily describe state changes that only modify small parts of the state (compare $P = w:=y-x;Q$ with $P(u,v,w,x,y,z) = Q(u,v,y-x,x,y,z)$). We note that the CADP system, which is based on LOTOS (state-poor), has already moved in this direction, with tools now working with LTN (LOTOS New Technology, state-rich), using a LTN to LOTOS translator [13]. Do other modelling notations have state-rich forms that are hard to check, but have good checkers for state-poor forms?

7 Conclusions

In this paper we evaluated possible approaches for translating into $CSP_M$, for model checking using FDR. Our main concern was how the state of a process could be captured in $CSP_M$ in such a way that FDR could handle a large amount of state variables and an even larger range of values. We then produced several models of $CSP_M$ specifications translated from and also explored the consequences of including both state invariants and preconditions of actions in the $CSP_M$ models. Such a research resulted in the development of , a tool for model checking , through the automatic translation from to $CSP_M$, and therefore, being able to use FDR for refinement checks. development was developed in 24 months, and has a total of over 26 thousand lines of Haskell code.

We observed that a distributed memory model, rather than a centralised one, as proposed by Mota et al. [24] is beneficial for larger states. Moreover, the time spent as well as the state exploration from FDR’s refinement checks is larger when capturing preconditions and state invariants. Another observation from our experiments is that we were able to reduce the state exploration even more by refining our model to one where the bindings were explicitly defined by , rather than considering a non-deterministic choice over such bindings, as per the original manual translation. This is justified by assuming that every state variable should be initialised prior to its use in the process. The outcome is that we now have a mechanised translator from to $CSP_M$ that produces tractable models, and allows the use of FDR on larger case studies than has been possible up to now.

We should clarify that our approach to produce parametrised processes is not an attempt to use the bindings data-independently [32, p. 453]. That is solving a different problem, namely finding a finite size of a type that is suitable to demonstrate the correctness for any finite or even infinite size of such type. Moreover, to date, our approach is unable to generate counterexamples or any kind of back annotation to the models, and thus is in our plans for future work.

We used the HD machine and the ring buffer case studies as examples in order to test the capabilities of our tool whilst model checking the automatically translated models in FDR. Our aim was to contribute to reducing FDR’s workload in order to model check larger systems. We learned that a practical implementation/mechanisation of a theory may reveal difficulties that could not otherwise be discovered without extensive use of a tool prototype, especially when applying it to larger case studies.