Adequate models of the systems to be analyzed are a prerequisite for model-based safety analysis. Consequently, S# provides specifically tailored modeling language concepts and recommends a systematic modeling approach that help to improve the adequacy of the models.

For safety analyses, S# obviously requires the modeling of relevant faults. The model of the intended system behavior must be extended with the occurrence patterns of faults as well as their local effects on the affected components. Subsequently, formal analysis techniques are able to reason about the system's global behavior in degraded situations. More details can be found in the Wiki's [fault modeling section](Fault Modeling).

Safety-critical systems typically follow the control-theoretical system partitioning into plants and controllers: The controllers constantly and continuously interact with their plants to prevent potentially bad plant behavior that might result in hazards. A controller internally has an implicit or explicit model of its plant, using sensors to predict and actuators to affect the plant's state and future behavior. Discrepancies can emerge between the controller's perceived plant state and the plant's actual state: Due to faults such as component failures or environmental disturbances, sensors can provide incorrect data or actuators can have unintended effects on the plant. Subsequently, the controller is likely to mispredict the plant's future behavior, omitting control actions or unknowingly issuing destructive actions that potentially result in hazards. Models of safety-critical systems must contain both plants and controllers in order to adequately represent such control failures for formal safety analyses.

The plant(s) of safety-critical systems represent those parts of the physical world that are indirectly influenced or observed by the systems' controllers (usually via actuators and sensors), such as the tank of the [pressure tank case study](Pressure Tank Case Study). The physical environment is required for the correct specification of safety hazards, as hazards typically result from a discrepancy between the plants' actual states and the states as they are perceived by the controllers. In turn, these discrepancies occur either because of systematic design errors, that is, the controllers are functionally incorrect, or because of occurrences of one or more component faults.

When modeling safety-critical systems, S#’s modeling methodology suggests to first identify the plants that the controllers are intended to indirectly observe and influence. In particular, it must be possible to express the safety hazards that are to be analyzed (typically exclusively) in terms of the plants. The next step consists of determining the sensors and actuators that are available to the controllers. Only then should the actual controller components be modeled, which can be comprised of multiple subcomponents of various kinds such as software components, hydraulic components, pneumatic components, etc. Faults are either modeled together with the individual components or they are added later in a separate step.

It is up to the safety engineer to decide which features of S#'s modeling language and analysis capabilities are used for the development of a safety-critical system. In fact, that decision can even vary based on the level of abstraction of a model: For instance, during the design exploration phase, a safety engineer might first create a highly abstract model of the desired system behavior without faults, using model checking to analyze the functional correctness of the system. In a second step, faults could be added, now using model checking to analyze the safety of the system. Subsequently, the model could be gradually refined to a less abstract, simulation-only one, even including the actual system software or hardware during later stages of the implementation phase. Using software engineering best practices, test cases for the models could be reused throughout all stages of development.