Welcome to S#

S# (pronounced "safety sharp") is a formal modeling framework and safety analysis framework for safety-critical systems developed by the Institute for Software & Systems Engineering at the University of Augsburg.

S# Features

• Expressive, modular modeling language based on the C# programming language
• Fully automated and efficient formal safety analyses
• Efficient formal analyses using fully exhaustive model checking
• Support for model simulations, model tests, model debugging, and model visualizations
• Extensive tool support based on standard .NET tools and libraries such as Visual Studio, providing model refactorings, debuggers, UI designers for visualizations, continuous integration with automated regression tests, etc.

Download S# and the Case Studies to Get Started

To get started with S#, please consult the Wiki. S# and the case studies are available under the MIT License.

Documents

• Wiki page with our S# related publications

• Quickstart S# for developers (Visual Studio 2017)

• Review S# Case Studies (Visual Studio 2015)

• Model and conduct DCCA on your own Case Studies with S# (Visual Studio 2015)

Example: Modeling with S#

The following small and incomplete example shows the model of a pressure sensor using the S#'s modeling language: The sensor checks whether a certain pressure level is reached. The example shows how safety-critical components and their required and provided ports are modeled in S#. The model also includes a fault that prevents the sensor from reporting that the pressure level is reached, possibly resulting in a hazard at the system level. For more details about modeling with S#, please consult the Wiki.

// Represents a model of a pressure sensor.
class PressureSensor : Component
{
  // The pressure level that the sensor reports.
  private readonly int _pressure;

  // A persistent fault that can occur nondeterminisitcally; once it has occurred,
  // it cannot disappear.
  private readonly Fault _noPressureFault = new PermanentFault();

  // Instantiates an instance of a pressure sensor. The maximum allowed pressure is
  // passed in as a constructor argument, allowing for easy configuration and
  // re-use of component models.
  public PressureSensor(int pressure)
  {
      _pressure = pressure;
  }

  // Required port. This is the port that the sensor uses to sense the actual
  // pressure level in some environment component.
  public extern int CheckPhysicalPressure();

  // Provided port. Indicates whether the pressure level that the sensor is
  // configured to report has been reached.
  public virtual bool HasPressureLevelBeenReached()
  {
      return CheckPhysicalPressure() >= _pressure;
  }

  // Represents the effect of the fault '_noPressureFault'.
  [FaultEffect(Fault = nameof(_noPressureFault)]
  class SenseNoPressure : PressureTank
  {
      // Overwrites the behavior of the sensor's provided port, always returning the
      // constant 'false' when the fault is activated.
      public override bool HasPressureLevelBeenReached()
      {
          return false;
      }
  }
}

Example: Safety Analysis with S#

To conduct fully automated safety analyses with S#, the following simple code is required. Analysis results are shown for the pressure tank case study; for more details, please see the Wiki.

var result = SafetyAnalysis.AnalyzeHazard(model, hazard);

result.SaveCounterExamples("counter examples");
Console.WriteLine(result);

=======================================================================
=======      Deductive Cause Consequence Analysis: Results      =======
=======================================================================

Elapsed Time: 00:00:02.1703065
Fault Count: 4
Faults: SuppressIsEmpty, SuppressIsFull, SuppressPumping, SuppressTimeout

Checked Fault Sets: 13 (81% of all fault sets)
Minimal Critical Sets: 1

   (1) { SuppressIsFull, SuppressTimeout }