Skip to content
S# is a formal modeling and safety analysis framework for safety-critical systems. It provides a domain specific modeling language and fully automated formal safety analysis tools based on C# and .NET.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Benchmark
Documents
Models
NuGet
SafetyCheckingTests
SafetyLustreTest
SafetySharpTests
Source
.gitignore
LICENSE.md
README.md
SafetyLustre.sln
SafetySharp.sln
SafetySharp.sln.DotSettings
nuget.config

README.md

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.

Links

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 }
You can’t perform that action at this time.