Semi-formal safety requirement specification using SysML state machine Diagrams

For safety relevant and critical systems a crucial part of the development is a concise and complete safety requirement definition. We show how requirements can be modeled with graphical, semiformal means using the systems modeling language SysML. However, aiming at an unambiguous and formal requirement definition and verification, we do not focus on diagrams that are typically used for requirement definitions, e.g. the SysML requirement, parametric and use case diagrams. We rather use the state machine diagram to define safe and unsafe states as well as sequences of states that are expected within the overall system and within subsystems. We show how generic types of safety requirements are represented using extended versions of state machine diagrams. To this end we model expressions that are similar in semantics to linear temporal logic expressions using the SysML state machine diagrams. In particular, we can distinguish, whether a strict sequence of states is requir ed or some kind of intermediate states are allowed within the sequence, e.g. from an unintended initial unsafe state to a final safe state in case of an active safety function. Finally, we will indicate how this approach can be used in future to verify that overall state machine diagrams of systems or subsystems fulfill these formalized requirements.