Applying SOFL to specify a railway crossing controller for industry

This paper describes an application of the formal engineering method SOFL (Structured-Object-based-Formal Language) to specifying a realistic railway crossing controller for potential use in industry. As the railway crossing controller is a safety critical and real-time system, this application demonstrates the capability of SOFL for developing safety-critical and real-time systems and provides a foundation for implementing such a software controller in practice. It also shows that appropriate integration of structured methods with graphical notation, formal notation, and natural language offers a good readability and traceability as well as an effective mechanism for reducing complexity of systems