Executable Specifications of Safety-Critical Systems with S#

:Model-based safety analysis techniques use formal methods to rigorously assess the risks associated with safety-critical systems. The adequacy of the results obtained from those formal techniques, however, is greatly influenced by the quality and comprehensibility of the underlying formal models. We introduce our S# modeling framework (pronounced "safety sharp"), an executable, systematic, high-level specification language and tool suite specifically designed for the convenient modeling and formal analysis of safety-critical systems. This paper shows how S# facilitates and improves model simulation, debugging, and testing during all stages of the development of such systems.