When model checking, S# exhaustively enumerates all reachable states of a model, checking all combinations of nondeterministic choices. S# models can be checked with two model checkers: LTSMin, an explicit-state model checker developed by the University of Twente, as well as S#'s own model checker. Integration with LTSMin occasionally proved difficult due to the different languages, platforms, and tools that LTSMin (C, GCC, Linux) and S# (C#, Visual Studio, Windows) are running on and developed for. We therefore got better results by developing our own model checker based on LTSMin's sophisticated algorithms. In a way, S#'s model checker is a .NET implementation of a subset of LTSMin's features. The following table gives an overview of what is supported by which S# model checking back-end.

In general, prefer using S#'s own model checker if it supports the features you need. We plan to continue improving S#'s model checker, adding features such as LTL and CTL model checking. In the long term, we plan to use LTSMin solely as a test oracle for S#'s own model checker.

Be sure to understand S#'s [model life-cycle](Model Life-Cycle) before continuing.

After minor code adjustments by the S# compiler, the C# code constituting a S# model is executed using its normal .NET semantics while model checking; consequently, models can be debugged during model checking using the standard Visual Studio debugger.

A S# model consists of a hierarchy of Component instances, each having fields that form the component's state. Fields are allowed to be of most .NET types, including arrays as well as references to other components. For efficient storage and comparison, Component states are serialized and deserialized to and from fixed-sized byte arrays at runtime. The set of states is finite, therefore heap allocations during model checking are unsupported.

S# first computes all serialized initial states of a model to initialize the model checker. Subsequently, S# computes all serialized successor states for all serialized source states that it has encountered: For all combinations of nondeterministic choices, in particular for all combinations of fault activations, the given state is deserialized so that all component instances can compute their successor states, which are subsequently serialized and passed to the model checker. As S# models execute arbitrary C# statements, S# models can make use of most of C#'s language features as well as many .NET libraries and classes such as List<T>, for example.

The only allowed source of nondeterminism within a model are faults and invocations of the family of Choice.Choose* functions. Other sources of nondeterminism, such as race conditions of threads, are not captured by S#; consequently, threads should not be used in any S# model. There are two reasons why a state might not have any successors at all: Either Component updates do not terminate or the execution is aborted abnormally due to an unhandled exception, for example. Both cases indicate bugs in the model or in the S# runtime that are readily discoverable.

Again, S# executes the models during model checking. It creates a corresponding Kripke structure on-the-fly that is passed to the model checker piece by piece for actual model checking, that is, to check whether an LTL formula or an invariant is violated. If a violation is detected, a counter example is generated that consists of a sequence of states and nondeterministic choices that can be played back by the simulator for model debugging purposes.

For the [pressure tank running example](Pressure Tank Case Study), for instance, invariants and LTL formulas can be model checked as described in the following.

Model checking of invariants determines whether a formula holds for all reachable states of a model. It is recommended to use S#'s own model checker to analyze invariants instead of using LTSMin.

try
{
    // 1
    var model = new Model();

    // 2; important: do not write 'var noFaults = ...' as that would evaluate the
    // formula immediately
    Formula invariant = !model.Tank.IsRuptured;

    // 3
    var result = ModelChecker.CheckInvariant(model, invariant);

    // 4
    if (result.FormulaHolds)
       Console.WriteLine($"Formula holds for all {result.StateCount} states.");
    else
       result.CounterExample.Save("counter example");
}
// 5
catch (AnalysisException e)
{
    Console.WriteLine($"Exception during model checking: {e.InnerException.Message}");
    e.CounterExample?.Save("counter example");
}

1. The model that should be analyzed is initialized. In this case, there are no constructor parameters; generally, though, models can be parameterized to allow for different model configurations in order to combine and check various design alternatives of a safety-critical system.

2. A Formula is constructed that assert that the tank never ruptures. It is absolutely imperative to declare the invariant variable to be of type Formula. If you use bool or var instead, the formula is evaluated immediately and the model checker checks the resulting constant.

3. The invariant !model.Tank.IsRuptured is checked for model, that is, the formula is checked for all reachable states of the model; if it is violated, result.FormulaHolds is false. Invariants cannot make use of any temporal operators and are evaluated separately for each state.

S# automatically selects its own model checker to conduct the analysis. If you want to use LTSMin instead, replace the line with the following code:

var result = new LtsMin().CheckInvariant(model, !model.Tank.IsRuptured);

Note how you do not have to declare a variable for the invariant but can also declare it inline instead when invoking CheckInvariant.

4. S# returns a result object that can be used to determine whether the formula holds. If it does not hold, result.CounterExample contains the generated counter example (always null when using LTSMin) that can be saved to disk using the CounterExample.Save method. The result object also provides access to the number of states and transitions that were reached during model checking.

5. Model checking might fail due to an AnalysisException being thrown; other types of exceptions should not be possible and would indicate a S# bug. If the wrapped exception exposed through e.InnerException was thrown by the model, the e.CounterExample contains a counter example that demonstrates how the exception can be reached. C#'s conditional access operator ?. is used to save the counter example to disk if e.CounterExample is not null. If the counter example is null, it is either a S# bug or the LTSMin back-end was used for model checking, which does not support counter example generation.

Note: Never try to use hidden variables in a formula when model checking with LTSMin.

Model checking of LTL formulas is only supported with LTSMin.

// requires the following static import for the convenient use of LTL operators:
// using static SafetySharp.Analysis.Operators;

try
{
    // 1
    var model = new Model();

    // 2; important: do not write 'var noFaults = ...' as that would evaluate the
    // formula immediately
    Formula noFaults =
        !model.Sensor.SuppressIsEmpty.IsActivated &&
        !model.Sensor.SuppressIsFull.IsActivated &&
        !model.Pump.SuppressPumping.IsActivated &&
        !model.Timer.SuppressTimeout.IsActivated;

    var result = ModelChecker.Check(model, G(noFaults).Implies(!F(model.Tank.IsRuptured)));

    // 3
    if (result.FormulaHolds)
       Console.WriteLine($"Formula holds.");
}
// 4
catch (AnalysisException e)
{
    Console.WriteLine($"Exception during model checking: {e.InnerException.Message}");
}

1. The model that should be analyzed is initialized. In this case, there are no constructor parameters; generally, though, models can be parameterized to allow for different model configurations in order to combine and check various design alternatives of a safety-critical system.

2. A Formula is constructed that assert that none of the faults contained in the model are ever [activated](Fault Modeling). It is absolutely imperative to declare the noFaults variable to be of type Formula. If you use bool or var instead, the formula is evaluated immediately and the model checker checks the resulting constant.

3. The LTL (G noFaults) -> !F model.Tank.IsRuptured is checked for model S# automatically selects LTSMin to conduct the analysis as its own model checker does not supports LTL

4. Same as for invariant checks except that no counter example is generated.

5. Same as for invariant checks except that no counter example is generated.

Note: Never try to use hidden variables in a formula when model checking with LTSMin.

Further examples for model checking with S# can be found in the case study projects.