Skip to main content

Verification

In the area of software engineering, formal verification is an interesting subject. Verification is a formal approach to prove the correctness of programs by means of mathematical models and techniques.

In this process, a program is checked against a set of correctness properties, also called the specification. A program is said to be correct, if the specification conforms to the implementation.

By proving specific properties of some software, this type of testing assists in developing safe and reliably software. In fact, many bugs cannot be detected by traditional means such as unit tests.

One type of verification technique is the so-called model checking, which is implemented in Bigraph Framework.

The algorithm employed here is based on the directed model checking explained in

Creating a Model Checker​

This code example shows how to create a model checker object for pure bigraphs:

PureReactiveSystem reactiveSystem = new PureReactiveSystem();
// Add an agent and reaction rules

/* code omitted */

// create model checking options
ModelCheckingOptions opts = ModelCheckingOptions.create();

// Create the pure bigraph model checker
PureBigraphModelChecker modelChecker = new PureBigraphModelChecker(reactiveSystem,
            BigraphModelChecker.SimulationType.BREADTH_FIRST,
            opts);
modelChecker.execute();

Some remarks:

  • The execute() method may throw a BigraphSimulationException
  • Simulation types are covered here.
  • Model checking options are explained here.

Reachability Checking​

The model checking procedure implemented in Bigraph Framework is especially suited for so-called reachability checking.

Event Listeners​

One may listen to specific events that are thrown during the simulation. This gives the user the possibility to interact with the simulation and fire additional actions or to log these events and evaluate them later, additionally to the final built reaction graph.

Therefore, the interface ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>> must be implemented and added to a model checker instance. It provides methods to listen when a reaction rule is applied or when the verification process finished, for instance.

For example, see here on how to listen for predicate evaluation results.

Asynchronous Execution​

To perform the model checking asynchronously, call the BigraphModelChecker#executeAsync():

Future<ReactionGraph<PureBigraph>> reactionGraphFuture = modelChecker.executeAsync();
ReactionGraph<PureBigraph> pureBigraphReactionGraph = reactionGraphFuture.get();

The executeAsync() method does not block the execution and returns a Future object to fetch the result later. It contains the complete reaction graph of the simulated BRS.

One can then export the transition system by calling modelChecker.exportReactionGraph(pureBigraphReactionGraph).

Provide a custom executor service​

The java.util.concurrent.ExecutorService is used to submit tasks of the model checker.

Bigraph framework offers to provide a custom ExecutorService by implementing the interface org.bigraphs.framework.core.providers.ExecutorServicePoolProvider, found in the bigraph-core dependency. The class BigraphModelChecker uses the java.util.ServiceLoader (see https://docs.oracle.com/javase/tutorial/ext/basics/spi.html#the-serviceloader-class to search for an implementation.

A default executor service provider is provided within the bigraph-rewriting dependency which creates a fixed thread pool.

Safety and Liveness Properties​

As long as the transition system is being built from a BRS specification, the provided predicates of the user are checked simultaneously for each new computed state in the course of a BRS simulation.

note

A user can listen to these events. Therefore, the interface ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>> must be implemented and added to the model checker instance.

These predicates come in two forms: as safety properties or as liveness properties. The former represents a state in the system that should not occur, whereas the later denote a system state that eventually occurs. By this we can test if a program never reaches a "bad state" (safety), or correctly terminates (reaching a desirable state), possibly producing a result (liveness).

Some further safety properties are: partial correctness, absence of deadlocks, and mutual exclusion (see [1]).

tip

Fairness properties are important for reactive systems. Safety is easier to check than liveness.

Simulation types​

The frameworks builds the reaction graph in the course of the simulation. Only the canonical form of an agent is stored in the graph to reduce the number of admissable states in order to minimize the state-space explosion problem.

Breadth-first simulation​

The algorithm described in [1] is implemented.

The respective reaction graph of the above example is shown below after the BFS simulation finished.

imgs

This form of simulation provides no guarantee that the simulation will end at some point.

Random simulation​

This type of simulation starts to apply a set of given reaction rules on an initial agent. After the reaction graph is expanded, the simulation randomly selects a new state and repeats the process. In other words, it follows only on path at random until now further rules can be applied. This form of simulation provides no guarantee that the simulation will end at some point or that the simulation will eventually reach a desired state.

Random Run #1Random Run #2
imgsimgs

Regarding the first random run of our example (left-hand figure above), rules (r0) and (r4) were applied on the agent. The algorithm was selecting the second agent (the one where (r4) points to), however, also stops here, since no further rules could be applied.

If the agent were chosen (where (r0) points to), rules (r1), (r2) and (r3) could be applied. This case is illustrated in the right-hand figure above.

Additional Model Checking Options​

Model checking options may be provided to the model checker. Therefore, the class ModelCheckingOptions needs to be created. An example is shown below.

ModelCheckingOptions opts = ModelCheckingOptions.create();
opts
        .and(transitionOpts()
                .setMaximumTransitions(100)
                .setMaximumTime(60)
                .allowReducibleClasses(true)
                .rewriteOpenLinks(false)
                .create()
        )
        .and(ModelCheckingOptions.exportOpts()
                .setReactionGraphFile(Paths.get(TARGET_DUMP_PATH, "transition_graph.png").toFile())
                .setPrintCanonicalStateLabel(false)
                .setOutputStatesFolder(Paths.get(TARGET_DUMP_PATH, "states/").toFile())
                .create()
        )
;

The individual options are divided into several categories which can be accessed by their respective builder classes. Currently, the following categories are available:

  • ModelCheckingOptions.TransitionOptions
  • ModelCheckingOptions.ExportOptions

They are explained in the following.

Transition options​

Stopping Criteria​

Notice that ModelCheckingOptions.TransitionOptions let us specify some stopping criteria by acquiring its builder by calling ModelCheckingOptions.TransitionOptions.transitionOpts():

  • Maximal Number of transitions to allow
  • Time
  • ...

The following methods are available through the ModelCheckingOptions.transitionOpts() builder instance to adjust the canonical string encoding algorithm of bigraphs, which is used for cycle checking of the transition system:

  • TransitionOptions.Builder#allowReducibleClasses(bool)
  • TransitionOptions.Builder#rewriteOpenLinks(bool)

The default values are good for most of the cases.

Export options​

The ModelCheckingOptions.ExportOptions class allows specifying a file path where the reaction graph (i.e., transition system) and the individual states shall be written to. If these options are left empty then the graphs are not exported. Also one can decide if the state labels of the reaction graph are simple identifiers a1, a2, a3, ... or canonical string encodings of bigraphs in its graphic output.

References​