Get Started with S#
To get started with S#, read the overview that gives an introduction to S#, its design goals and supported features. [Installation and setup](Installation and Setup) explains how S# is installed and run, and what its hardware and software requirements are. Our S#-related publications and [related work and tools](Related Work and Tools) are listed as well.
Case Studies Modeled and Analyzed with S#
There are several case studies in the S# repository that are used to design and evaluate S#'s modeling and analysis features. The [pressure tank](Pressure Tank Case Study) is the running example used throughout the Wiki.
- Pressure Tank
- Radio-Controlled Railroad Crossing
- Height Control
- Hemodialysis Machine
- Robot Cell
- Pill Production
Systematic Modeling of Safety-Critical Systems with S#
S# provides a domain specific modeling language embedded into the C# programming language and the .NET runtime environment. While S# models are represented as C# programs, they are still models of the safety-critical systems to be analyzed; in particular, some parts of those programs represent the physical environment, hardware components, hydraulic subsystems, etc., none of which are software. S# models are closely related to SysML blocks representing actual system components. [Faults](Fault Modeling), obviously an important concept in the context of safety analysis, can be conveniently modeled. Models are modular and can be flexibly composed.
Analyzing Safety-Critical Systems with S#
S#'s model execution approach unifies model simulations, model tests, visualizations, and fully exhaustive [model checking](Model Checking) by executing the S# models in the exact same way with consistent semantics regardless of whether a simulation is run or some formula is model checked. Standard C# tools like Visual Studio can be used for model development and analysis; in particular, models can be debugged even while model checking. Automated [safety analyses](Safety Analysis) and model checking in general are highly efficient even despite the high level of expressiveness of S#'s modeling language.