Safety-critical systems are expected to operate safely under regular circumstances as well as in many degraded situations. In the latter case, these systems have to cope with one or more components that are not working as specified, while at the same time they have to avoid (serious) economical or environmental damage, injuries, or even loss of lives. S# provides a modeling language specifically designed to express important safety-related concepts such as faults and the physical environment of a safety-critical system. For safety assessments, model simulations as well as formal safety analyses are supported.

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# brings forward well-established software engineering principles and best practices to the modeling and analysis of safety-critical systems during all phases of development. It is an integrated approach that fosters the systematic development of comprehensible, adequate, and modular models of safety-critical systems, while also allowing the use of formal safety analysis techniques for rigorous safety assessment.

• Expressive, modular modeling language based on the C# programming language: S# provides a component oriented domain specific language built on top of C# that facilitates a [systematic modeling approach](Systematic Modeling of Safety-Critical Systems) including [fault modeling](Fault modeling) and model composition.

• Fully automated and efficient formal safety analyses: Formal analysis techniques allow for sound reasoning about safety-critical aspects of system designs with mathematical rigor. Based on a such a technique, S# automatically and efficiently [assesses the safety](Safety Analysis) of the modeled safety-critical systems, hiding the details of the underlying formal mechanisms.

• Efficient formal analyses using fully exhaustive model checking: S# supports [fully exhaustive model checking](Model Checking) of the modeled systems to check the soundness of the models.

• Support for model simulations, model tests, model debugging, and model visualizations: Model development is supported by simulations, automated regression test, and in particular, by model visualizations.

• Extensive tool support based on standard .NET tools and libraries such as Visual Studio: S# can make use of standard refactoring capabilities, debuggers, UI designers for visualizations, continuous integration with automated regression tests, etc. that are available for C# and .NET development.

Instead of inventing a completely new modeling language and corresponding tools, S# models are written in a domain specific language that is embedded into the C# programming language with full access to all .NET libraries and tools. S# models therefore profit from state-of-the-art code editing and debugging features. Even though S# models are represented as code, they are still models, albeit executable ones; conceptually, they are at a higher level of abstraction than actual code. The implementation of a safety-critical system's software is typically done in the C or C++ programming languages and compiled for specific embedded microcontrollers – S# does not try to change that.

The S# modeling language inherits all of C#'s language features and expressiveness. Only the parts of a S# model that are simulated or model checked are restricted to a subset of C#: For these parts, arbitrary object construction as well as other more sophisticated features such async/await are not supported. For supporting infrastructure code that sets up test cases or composes system design variants, however, none of these restrictions apply.