Components

S# models consist of components that represent the real-world components of the actual systems as well as relevant parts of the modeled system's physical [environment](Systematic Modeling of Safety-Critical Systems). This page describes how individual S# components can be modeled and the parts a component consists of. Composing components together to form a model that can be analyzed with S# is explained on the models page. How relevant faults can be added to a component is described on the [fault modeling page](Fault Modeling). S#'s component modeling features are inspired by SysML's block definition diagrams and internal block diagrams.

Overview

S# models are component oriented with each component of the actual system being modeled as a component within the S# modeling language. Components hide their internal representation and state from outsiders. Provided and required ports handle the communication between components; two such ports of the same signature can be bound, with the binding triggering the behavior associated with the provided port whenever the required port is used. The underlying model of computation is a series of discrete system steps, where a constant amount of time passes between each step. Components can execute either sequentially or (conceptually) in parallel, but they implicitly share a global clock. The model of computation is not (yet) suitable for modeling continuous timing behavior or physical equations; S# therefore only allows for discrete modeling of the physical environment of a system.

In S#, the structure of a system is modeled as a (non-strict) hierarchy of components with explicit communication ports; the models can be parametrized to allow for different system configurations. The global behavior of the system is implicitly defined by the local behaviors of the individual components and their communication interrelationships.

S# components are represented by C# classes and component instances are represented by objects, i.e., by instances of the corresponding classes. The PressureSensor component of the pressure tank case study, for instance, is defined as a class that is derived from the Component base class as follows:

class PressureSensor : Component
{
    // ...
}

The C# class PressureSensor is used to represent the S# component type PressureSensor. A .NET object p = new PressureSensor() is a S# component instance of PressureSensor. Class inheritance, interfaces, and generics are also fully supported; they are most useful when modeling and analyzing different design variants of a safety-critical system.

Component State and Subcomponents

Components usually hide their internal state from other components; a component's state consists of all of its implicitly and explicitly declared fields. Fields can be of any supported .NET type; in particular, of primitive types such as int or bool, enum types, array types, List<T> instances, references to other components, etc.

The following example shows a non-exhaustive list of the different kinds of state that a component can have:

class C : Component
{
    int _i;
    bool[] _b;
    StateMachine<State> _s = /* initial state */;
    PressureSensor _sensor;

    bool P { get; set; }
}

C's state consists of: The integer field _i, the Boolean array field _b, a state machine field _s (see below), a reference to a PressureSensor instance _sensor, and an additional, implicitly declared field for the auto-implemented property P (P additionally declares two provided ports, see below). All of the fields can store different values while the system is analyzed with S#.

Range Restrictions

Range restrictions are a convenient and declarative way to restrict the allowed range of the values that can be stored in a field. Suppose a component has a field _count with an allowed range of 0 to 5, inclusive. In S#, this can be modeled as follows:

class C : Component
{
    [Range(0, 5, OverflowBehavior.Clamp)]
    int _count;
}

S# automatically ensures that only the values 0, 1, 2, 3, 4, or 5 can be stored in _count at the end of each system step; the value in _count can violate the range temporarily. How such violations are resolved is indicated by the OverflowBehavior: If Clamp is specified, the value is simply clamped to the upper or lower bound of the range, whatever is closer. WrapClamp does the same as Clamp but uses the opposite bound. A value of Error indicates that a RangeViolationException should be thrown whenever the range is violated. Such exceptions can be checked for using [model checking](Model Checking), which also generates a witness that shows how such a range violation can be reached.

Sometimes, it is not possible to statically determine the range of a field; the values used in an attribute such as in the example above have to be compile time constants. Alternatively, it is therefore possible to restrict the range in a component's constructor as follows:

class C : Component
{
    int _count;

    public C(int upperBound)
    {
        Range.Restrict(() => _count, 0, upperBound, OverflowBehavior.Clamp);
    }
}

State Space Optimizations

Some fields only store transient values that actually should not be part of a component's state. S# provides the [Hidden] attribute that can be used to mark fields that should not contribute to a component's state. The state of the following component therefore effectively consists of a single integer value only, even though three int fields are declared:

class C : Component
{
    [Hidden]
    int _i1;

    readonly int _i2;
    int _i3;
}

_i1 is not part of C's state because it is marked as [Hidden]. _i2 is not part of the state because it is declared as readonly; such fields can only be set in a component constructor and cannot change their value afterwards. Hence, while readonly fields are no compile time constants, they effectively are constant during S# analyses and therefore do not contribute to a component's state. The [Hidden] attribute can be used in places where the readonly keyword would be too restrictive.

Caution: Writes to readonly fields are only limited by the C# compiler; via reflection, the fields' values could still be changed.

Caution: S# does not make any guarantees for [Hidden] fields; if you mark the wrong fields as [Hidden], model checking results might no longer be adequate. You should ensure that hidden fields are always written to before they are read in a step; otherwise, any previously written value might be read from the field.

You should always mark references to subcomponents that never change with either readonly or [Hidden], as references that belong to a component's state make model checking more expensive. For instance, the controller of the pressure tank case study has [Hidden] references to the pump, sensor, and timer, because the case study model initializes those fields from outside the component (hence, not within Controller's constructor, so readonly cannot be used), but the actual values remain unchanged during analyses.

class Controller : Component
{
    [Hidden] public Pump Pump;
    [Hidden] public PressureSensor Sensor;
    [Hidden] public Timer Timer;
}

Fields of array and list types, for example, can also be marked as hidden. Consider the following:

class C : Component
{
    [Hidden(HideElements = true)]
    List<IComponent> _l;

    [Hidden(HideElements = false)]
    IComponent[] _a;
}

Marking a field that implements IEnumerable (such as arrays or List<T>) with [Hidden] only ensures that the reference to the array or list itself is not part of the component's state. The actual values stored in the list or array still are in the state by default. The [Hidden] attribute allows this behavior to be overwritten using the HideElements property. In the example above, _a is hidden, while all of its references are not hidden because HideElements is false; this is the default, hence HideElements = false could also have been omitted. For _l, on the other hand, the elements are hidden, hence they are also not part of the component's state.

Caution: While S# supports object references in a component's state, only objects known during model initialization can be referenced. That is, object allocation during simulations or model checking is unsupported and would result in an exception. In particular, classes like List<T> that might allocate when adding new items to the list must have sufficient memory preallocated during initialization. For List<T>, this can be achieved by setting the Capacity property to the maximum number of elements that are ever stored in the list. If the capacity is ever exceeded, an exception is thrown during analysis.

Ports

All methods and properties of a component are considered to be either required or provided ports. Ports allow communications between components via port bindings.

Provided Ports

Provided ports can be seen as "services" that a component provides to other components. A component declares provided ports as regular C# methods or properties; they can be virtual, abstract, or neither of which to support component inheritance and [fault modeling](Fault Modeling). An example:

class C : Component
{
    public virtual bool P1 => true;
    public virtual bool P2
    {
        get { return true; }
    }

    public int P3 { get; set; }

    public int P4(int a, out int b)
    {
        b = a;
        return a;
    }
}

The first two provided ports are declared as getter-only properties with an expression body (P1) or a statement body (P2). The third and fourth provided ports are declared as an auto-implemented property; the property implicitly declares an int state field and two provided ports, namely the getter int get_P3() and the setter void set_P3(int value). The fifth provided port is a method with an out parameter in addition to returning an integer.

Required Ports

Required ports can be seen as specifications of the "services" that a component requires from other components. A component declares required ports as regular C# methods or properties with the extern keyword; they can optionally be virtual to support component inheritance and [fault modeling](Fault Modeling). An example:

class C : Component
{
    public extern virtual bool P1 { get; }
	public extern bool P2 { get; set; }
    public extern int P3(int a, out int b);
}

The first required port is declared as a getter-only property. The second and third required ports are declared as an auto-implemented property, effectively declaring the required ports bool get_P2() and void set_P2(bool). The forth required port is a method with an out parameter in addition to returning an integer.

Port Bindings

C#'s regular method invocation syntax or property reads and writes represent invocations of required and provided ports. Invoking a provided ports executes its behavior, that is, its body, optionally returning values via the method's or property's return value or ref and out parameters.

Required ports, on the other hand, have no body, hence they cannot be invoked unless they are bound to a provided port. Bound required ports therefore forward all invocations to the provided port they are bound to; invoking an unbound required port results in an UnboundPortException. Bindings are established by calling the Component.Bind() or ModelBase.Bind() methods as follows:

class C : Component
{
    public void ProvidedPort()
	{
		// ...
	}
}

class D : Component
{
    public extern void RequiredPort();
}

// somewhere during model initialization
var c = new C();
var d = new D();
Component.Bind(nameof(d.RequiredPort), nameof(c.ProvidedPort));

Ports are always bound for concrete component instances, never for types. That is, the Bind method in the example above binds the required port RequiredPort of the component instance d to the provided port ProvidedPort declared by component instance c. Ports are bound by name using C#'s nameof operator. The S# compiler and runtime ensure that the binding is established at runtime.

Component and Port Behavior

Behavior is code that is executed whenever a provided port is invoked. S# supports two kinds of behavior: Sequential behavior, i.e., regular C# statements and expressions, as well as state machine behavior. In order to support abstractions of actual system or environment behavior, nondeterminism is also supported.

Nondeterminism

Abstractions in a model naturally lead to nondeterminism. S# supports nondeterministic models, checking all combinations of nondeterministic choices during model checking. However, only nondeterminism that is actually known to S# can be exhaustively checked. If you are generating random numbers or have race conditions in you models due to the use of multiple threads, model checking will not be exhaustive. S# makes no attempt in preventing you from using such constructs, so it is your own responsiblity.

Therefore, the only source of nondeterminism within a model should be uses of S#'s Choice class and all of its helper methods; in particular, the family of Choose functions provided by the Component class for convenience. The following example shows how the Choose function can be used to nondeterministically return either true or false from a provided port:

class C : Component
{
    public bool P => Choose(true, false);
}

There are several overloads of the Choose methods that nondeterministically choose one of their provided arguments. ChooseFromRange, on the other hand, nondeterministically returns a value that lies within the given input range. ChooseIndex can be used when working with lists or arrays: Given the number of elements within an array or list, it chooses one valid index nondeterministically.

State Machines

State machines are sometimes a more natural fit to model certain behavioral aspects of a component. The following example demonstrates how state machines can be used to model the controller of the pressure tank case study:

class Controller : Component
{
	public enum State
	{
		Inactive,
		Filling,
		StoppedBySensor,
		StoppedByTimer
	}

	public readonly StateMachine<State> StateMachine = State.Inactive;

	public override void Update()
	{
		StateMachine
			.Transition(
				from: State.Filling,
				to: State.StoppedByTimer,
				guard: Timer.HasElapsed,
				action: Pump.Disable)
			.Transition(
				from: State.Filling,
				to: State.StoppedBySensor,
				guard: Sensor.IsFull,
				action: () =>
				{
					Pump.Disable();
					Timer.Stop();
				})
			.Transition(
				from: new[] { State.StoppedByTimer, State.StoppedBySensor, State.Inactive },
				to: State.Filling,
				guard: Sensor.IsEmpty,
				action: () =>
				{
					Timer.Start();
					Pump.Enable();
				});
	}
}

Adding a state machine to a component consists of three steps:

1. An enumeration is added to the component that names the individual states of the state machine; for the pressure tank controller, this enumeration is called State and comprises the four states Inactive, Filling, StoppedBySensor, and StoppedByTimer.

2. A field of type StateMachine<T> is added to the model. The generic parameter T is set to the enumeration declaring the state machine's state type. The state machine's initial state is specified either by simply assigning the state to the state machine field as shown above, or by explicitly instantiating a new state machine instance such as new StateMachine<State>(State.Inactive). Multiple initial states, one of which is chosen nondeterministically, are also supported.

3. The state machine's transitions are specified in some ports of the component by invoking the Transition method on the StateMachine<T> instance. Multiple calls to Transition can be chained as shown above. A transition consists of mandatory source states (the from parameter), mandatory target states (the to parameter), and optional guards and actions.

A transition is only enabled when the state machine is currently in one of the transition's source states and the guard evaluates to true; if the guard is omitted, it is always assumed to be true. If multiple transitions are enabled, one is chosen nondeterministically. The chosen transition's optional action is executed once the state has been updated. If the action is omitted, it is assumed to be () => {}, i.e., the empty action without any effects. If a transition has multiple target states and the transition is enabled and chosen, one target state is chosen nondeterministically.

Both actions and guards can be arbitrary C# expressions having side effects, nondeterministic choices, port invocations, etc. Guards that affect the state machines state should be avoided; actions, however, are free to change the state machine's state again.

Caution: It makes a difference whether multiple calls to Transition are chained. In the following example, state machine s1 will end up in state State.S1, while s2 will end up in state State.S2 when initially in State.S0:

s1.Transition(from: State.S0, to: State.S1).Transition(from: State.S1, to: State.S2);
s2.Transition(from: State.S0, to: State.S1);
s2.Transition(from: State.S1, to: State.S2);

Assuming both state machines are in state State.S0, the chained Transition invocations of s1 considers all possible transitions simultaneously. Obviously, only the first transition is enabled, so the state is changed to State.S1. For s2, on the other hand, there is only one enabled transition that changes the state to State.S1. Then another state change is attempted, which again has an enabled transition that changes the state to State.S2.

Consequently, state machine transitions can make use of S#'s sequential code execution behavior. That is, they can change their state multiple times, if necessary; for instance, transitions can be executed in a while loop until no further transition is enabled, i.e., until a fixpoint is reached. Moreover, state changes can be triggered in response to a port call. For instance, if a state machine should transition from state State.S0 to State.S1 whenever the port P is invoked and some condition holds that depends on the port invocation arguments:

class C : Component
{
    // ...
    StateMachine<State> _s = /* ... */;

    public void P(int x)
    {
        _s.Transition(from: State.S0, to: State.S1, guard: x > 0);
    }
}

Component Updates

The Component base class declares the virtual Update method that all components can override. During analyses, S# calls the Update methods of all root components. The behaviors of the Update methods are therefore the only way to start triggering state changes and calling provided and required ports; if no root component overrides Update, the model would effectively not have any behavior.

Caution: S# only calls the Update methods of the root components; the Update methods of all other components must be called explicitly, if necessary. For convenience, S# provides an Update(IComponent[]) method and mulitple overloads that invoke the Update methods of all given components in the order of the components in the given array. The pressure tank controller, for instance, uses this Update method as follows:

public class Controller : Component
{
    public Pump Pump;
    public Timer Timer;
    public PressureSensor Sensor;

    public override void Update()
    {
        Update(Sensor, Timer, Pump);

        // ...
    }
}

It is best practice to always call the Update method of all subcomponents, regardless of whether they actually override Update. In the above example, only Timer actually overrides Update, whereas Pump and PressureSensor do not. Since overriding Update is considered to be an implementation detail of each component, omitting the call to Update would couple the controller to the actual component types PressureSensor and Pump. Therefore, the controller could not be reused when a different sensor type derived from PressureSensor is used that actually overrides Update, even though the provided and required ports would otherwise be the same.

Model of Computation

S# currently has a very straightforward model of computation. It is sufficient to model the case studies in the repository as well as some additional ones. We expect future versions of S# to support more sophisticated models of computations.

S# models consists of sequences of steps, where a constant amount of time passes between steps. Steps are divided into two phases: First, the Update methods of all [environment](Systematic Modeling of Safety-Critical Systems) components are executed, then all Update methods of the system components are invoked. The order of invocation within these two groups is unspecified. In general, there should never be direct data dependencies between components of the same group. Instead, we expect data between two system components, for instance, to be exchanged using some environment component; radio- based communication between two system components could be modeled that way. At the conceptual level, this restriction results in all components within the environment and the system groups to be executed in parallel with no direct interactions with each other.

S# currently has no support for modeling timing behavior or complex physical equations. Both would be nice to have, however, especially for modeling controller and environment components, respectively.