An approach to specifying and verifying safety-critical systems with practical formal method SOFL

One of the primacy concerns in developing computer embedded safety-critical systems is how to develop quality software. Software must fulfill its functional requirements and must not contribute to the violation of safety properties of the entire system. To this end, capturing error free and satisfactory functional requirements is crucial before proceeding to the subsequent development phases. We describe an approach to specifying and verifying software for safety-critical systems with the practical formal method SOFL (Structured-Object-based-Formal Language). Requirements specification focuses on the functionality of the software, but with the consideration of safety constraints and its interaction with the surrounding operational environment. The verification of specifications can be carried out using three techniques: data flow reachability checking, specification, testing, and rigorous proofs, respectively. We apply this approach to a realistic railway crossing controller for a case study and analyzes its result