Coverage visualization and analysis of net inscriptions in coloured Petri net models

Hence, we first need to address what we want MC/DC coverage to mean in the context of CPN models. If we first consider guard expressions on transitions, then we have two interesting questions related to coverage: if there is a guard, we know from the state space (or simulation) report whether the transition has occurred and hence whether the guard expression has evaluated to true. However, we do not know whether during the calculation of enabling by CPN Tools it ever has been false. If the guard had never evaluated to false, this may indicate a problem in the model or the requirements it came from, since apparently that guard was not actually necessary. Furthermore, if a decision in a guard is a complex expression, then as per MC/DC, we would like to see evidence that each condition contributed to the outcome. Neither case can be deduced from the state space report or via the CTL model checker of CPN Tools as the executions only contain transition bindings that have occurred and hence cases where the guard has evaluated to true.

In the following, we describe how we instrument the guards on transitions such that coverage data can be obtained. We developed an automated instrumentation based on the .cpn XML file of CPN Tools in combination with an SML parser. Arc expressions are handled analogously. Guards in a CPN model are written following the general form of a comma-separated list of Boolean expressions (decisions): A special case is the expression which may have two effects: if the variable var is bound already via a pattern in another expression (arc or guard) of the transition, then this is indeed a Boolean equality test (decision). If, however, var is not bound via other expressions, then this assigns the value of exp to the variable var and does not contribute to any guarding effect.

We consider general Boolean expressions which may make use of the full feature set of the SML language for expressions, most importantly Boolean binary operations, negation, conditional expressions with if–then–else and function calls. Simplified, we handle:

Function symbols f cover user-defined functions as well as (built-in) relational operators such as <, \(=\); we do not detail the overall nature of arbitrary SML expressions, but refer the reader to [14] for a comprehensive discussion. The automatic instrumentation also processes the definition of SML functions in the body of the .cpn XML file, which were not considered in our manually instrumented solution. We do not provide instrumentation to measure coverage of pattern matching in function definitions and expressions.

SSE or simulation of the model is not in itself sufficient to determine the outcome of the overall expression and its sub-expressions: guards are not explicitly represented, and we only have the event of taking the transition in the state space, but no value of the guard expressions. Hence, we need to rely on side effects during model execution to record the intermediate results. Our key idea is to transform every sub-expression and the overall decision into a form which will use SML’s file input/output to emit a log entry that we can collect and analyse. The coverage statistics is calculated from the logged entries through a Python script that is easy to reuse in other contexts.

For the necessary instrumentation, a transformation of guard and arc expressions, we essentially create an interpreter for Boolean expressions: when guards are checked (in a deterministic order due to SML’s semantics from left to right), we traverse a term representation of the Boolean expression and output the intermediate results. The Boolean expressions that are found in the definition of the SML functions will also trigger log messages during the SSE or simulation of the model.

We have designed a data type (see Listing 1) that can capture the above constructs, and define an evaluation function (see Listing 2) on it. As we later need to map coverage reports back to code, for overall expressions and atomic proposition , we introduce a component of type string that allows this identification. The evaluation function eval collects the result of intermediate evaluations in a list data structure, and the function (implementation not shown) turns this result into a single Boolean value that is used in the guard, and as a side effect outputs the truth value outcome for individual conditions. As an example, if we consider a guard: ; then we can transform this guard in a straightforward manner into . It is important to notice that this does not give us the (symbolic) Boolean expressions, as we still leave it to the standard SML semantics to evaluate the , while abstractly we refer to the AP as a condition named “1.” We elide expression and proposition names for clarity in the text when not needed.

Any sub-expression must be total and not crash and abort the model execution. A short-circuiting evaluation needs to explicitly incorporate the or operator and becomes more verbose; hence, for example, becomes .

We can likewise apply the transformation to Boolean expressions in arc expressions: any Boolean expression is transformed into , resulting for example in the transformation of into

Figure 1 shows the sub-modules contained in the Paxos CPN model [15] called the initial Proposer and it is associated to the InitProposer substitution transition. It initializes Proposers to obtain a new leader and receive a client request for consensus. Then, the value of the current round number of the leader and the value of the received client request will be presented on the port places as tokens, respectively [15].

The ”InitProposer” module is one of several modules of the Paxos model, and the arc and guard expressions in the other modules were transformed in a similar manner. The figure also illustrates how, after evaluating coverage data, we indicate full coverage by colouring the guard green, otherwise red.

The general format from the instrumentation step is a sequence of colon-delimited rows, where each triple in a row captures a single decision with the truth values of all conditions in a fixed order and the outcome. As an example, see Script 4.1. The name (stemming from the first argument to an above) is configurable and should be unique in the model; and derived from the name of the element (guard or arc) the expression is attached to. This makes it easy to later trace coverage results for this name back to the element in the model. We recommend to derive the name from the element (guard or arc) the expression is attached to. This makes it easy to later trace coverage results for this name back to the element in the model, and for the user to navigate to the sub-module containing the element should they desire to do so.

Our Python tool parses the log file and calculates coverage information. It prints the percentage of decisions that are MC/DC and branch covered in textual mode and in GNU Plot syntax (see charts in Fig. 3). The output contains individual reports in the form of the truth tables for each decision, which summarizes the conditions that are fired during the execution of the CPN model, and sets of pairs of test cases per condition that show the independence effect of that condition.

In the case that the decision is not MC/DC covered, the information provided by the Python script helps to infer the remaining valuations of the truth tables that should be evaluated in order to fulfil this criteria. In the example in Script 4.2, the first condition (leftmost column in the table) has multiple complementary entries where the expression only varies in one bit (e.g. rows 0001 and 1001) and the output changes (0 to 1). The R set shows three such pairs for condition 1, but no complementary entries at all are found in the truth table for conditions 2, 3 and 4, and hence indicated as empty sets [] by Python. This information can then be used by developers to drill down into parts of their model, e.g. through simulation, that have not been covered adequately yet.

It is straightforward to capture executions of multiple runs of the Petri net: our API supports passing initialization functions that reconfigure the net between runs. However, as there is no standardized way of configuring alternative initial markings or configurations in CPN Tools, the user has to actively make use of this API. In the default configuration, only the immediate net given in the model is evaluated, and no further alternative configurations are explored.

As an example, we show in Listing 3 how we make use of this feature in the MQTT model, where alternative configurations were easily discoverable for us: the signature of MC/DC generation with a simple test-driver is

where the

first argument is a timeout for the SSE, the second is a function with side effects that manipulates the global configurations that are commonly used in CPN Tools to parameterize models, the next argument is a list of different configurations, followed by the filename for writing results to.

This function will always first evaluate the initial model configuration and then have additional runs for every configuration. Internally, it calls into CPN Tools’ function for the actual SSE. Hence the first -invocation in Listing 3 will execute a full SSE without timeout, whereas the second -invocation would produce three subsequent runs logged into the same file, again without a default timeout. The test-driver can easily be adapted to different scenarios or ways of reconfiguring a model. Alternatively, traces can also be produced in separate files that are then concatenated for the coverage analysis.

To visualize the coverage information in a graphical CPN model, we provide another Python script which parses the CPN model and changes the colour of guards in the CPN model based on coverage data. We take both the original model under test and the coverage results as input arguments and produce a new model where covered arcs and transitions are highlighted in green, whereas the uncovered parts are highlighted in red.

Figure 2 gives an overview of our experimental setup. Initially, we have the original CPN model under test and we instrument it by transforming SML expressions into a form that as a side effect prints how conditions were evaluated and the overall outcome of the decision (cf. Section 3). Second, we run the SSE on the instrumented model and then reconfigure the configuration (initial marking) with any additional initial configurations if they are obvious from the model. As the side effect of SSE, we run the MC/DC generation which gives as output a log file containing the information of evaluations of conditions in arcs expressions and guards and the decision outcome. Finally, we run the MC/DC analyser (cf. Sect. 4) that determines whether each decision is MC/DC covered or not. In addition, it reports the branch coverage (BC), by checking whether each of the possible branches in each decision has been taken at least once.

Furthermore, we visualize the coverage information in the CPNs models taking as input the original CPN model and the results of how conditions and decisions are MC/DC evaluated. This results in the coloured CPN model where the covered parts are coloured in green and the uncovered parts are presented in red. Figure 1a shows a CPN model structure of an original model and Fig. 1b shows the instrumented CPN model after coverage analysis where covered and uncovered parts are highlighted. Table 2 presents the summary of the percentage of how much the tested CPN models are MC/DC and BC covered. The percentage is calculated as the number of covered conditions over the total number of conditions in case of MC/DC and the ratio of covered decisions/branches to the total number of decisions/branches.

Table 2 presents the experimental results for the eleven example models [15‐20]. For each model, we consider the number of executed decisions (second column) in arcs and guards. Column Model decisions refers to the number of decisions that have been instrumented in the model. The number of decisions observed in the model and in the log file may deviate in case some of the decisions are never executed, in which case they will not appear in the log file. We indicate them in brackets if during our exploration we did not visit, and hence log, each decision at least once. In the case of DisCSP, there are two guard decisions which were never executed. The column Non-trivial decisions gives the number of the decisions (out of all decisions) that have at least two conditions in the model, as they are the interesting ones while checking independence effect. If a decision has only one condition, it is not possible to differentiate MC/DC from DC. Columns \({\text {MC/DC}}(\%)\) and \({\text {BC}}(\%)\) present the coverage percentage for the CPN models under test. We record the ratio of covered decisions to the total number of decisions. Due to the large (maybe infinite) state space, we set the timeout to 600 s: in most models, running longer SSE do not increase the coverage metrics in terms of the number of arcs and guards expression executed.

MC/DC is covered if all the conditions show the independence effect on the outcome. BC is covered if all the branches are taken at least once. This makes MC/DC a stronger coverage criterion compared to BC, which we will also see in the following graphs. Figure 3 shows the coverage results as the ratio of covered decisions to the number of executed decisions in guards and arcs for both MC/DC and BC. The plots show that the covered decisions increase as the model (and hence the decisions) is being executed. Note that the x-axis does not directly represent execution time of the model: the state space explorer prunes states that have been already visited (which takes time), and hence, as the SSE progresses the number of expressions evaluated per time unit will decrease. In case an expression was executed with the same outcome, the coverage results do not increase, since those test cases have already been explored. Our instrumentation does not have a significant impact on the execution time of the model. Considering the time taken for the full SSE of the finite state models, for instance DisCSP model, both without and with instrumentation, it takes 212 seconds versus 214 seconds, respectively. It is around 1% of overhead which is the cost for the instrumentation.

The CPNABS model and T34PIM model have many single condition (trivial) decisions, and their coverage percentage is higher compared to other models. The Paxos model has less than a half of its decisions covered for both BC and MC/DC with a small percentage difference. The VM model and MQTT with timeout have also less percentage in coverage and both have a high number of non-trivial decisions, which puts more weight on having a suitable test suite to achieve good MC/DC coverage. In addition, we considered additional configurations without timeout for the SSE in the MQTT model and compared the coverage metrics when the configurations are set to timeout. As shown in Fig. 3a, b, the MC/DC and BC percentage increased from 11.11 to 21% and 22.22% to 65.22%, respectively. It is interesting to observe the quality differences of the curves for the tested models. Some of the tested models have less than half of their decisions covered. This should attract the attention of developers and they should assess whether they have tested their models enough, as these results indicate that there is something that might be considered doubtful and require to revisit their test suite. Two factors affect the coverage percentage results presented for these models: A main result of our analysis of the example models is that none of the models (including those for which the state space could be fully explored) have full MC/DC or BC. This confirms our hypothesis that code coverage of net inscriptions of CPN models can be of interest to developers, such as revealing not taken branches of the if–then–else arc expressions, never executed guard decisions, conditions that do not independently affect the outcome and some model design errors. Our results show that even for full SSE, we may still find expressions that are not MC/DC covered. Assuming that the model is correct, improving coverage then requires improving the test suite. This confirms the relevance and added value of performing coverage analysis of net inscriptions of CPN models over the dead places/transitions report as part of the state space generation. A natural next step in a model development process would be for the developers to revisit the decisions that are not MC/DC covered and understand the underlying reason. For the models that we have co-published, we can indeed confirm that the original models were not designed with a full test suite in mind, neither from the initial configuration, nor through embedded configurations like for example the MQTT model.

Our general approach to coverage analysis presents several directions forward which would help developers get a better understanding of their models: firstly, while generating the full state space is certainly the preferred approach, this is not feasible if the state space is inherently infinite or too large. Simulation of particular executions could then be guided by results from the coverage and try to achieve higher coverage in parts of the model that have not been explored yet. However, while selecting particular transitions to follow in a simulation is straightforward, manipulating the data space for bindings used in guards is a much harder problem and closely related to test case generation (recall the CPNs also rely on suitable initial states, which are currently given by developers). Making use of feedback between the state of the simulation and the state of the coverage would, however, require much tighter integration of the tools.