SOFL- A Better Approach for Formal Specification: A Case Study Based Comparison

Abstract — Formal Methods are necessary for the specification, development and verification of safety critical systems. Formal Languages help us to identify errors at an early stage in the development process and can aid in reducing overall system development costs. Despite their benefits, formal methods are not widely accepted in the industry due to the need for high abstraction and a mathematical labor pool. The SOFL (Structured Object-Oriented Formal Language) methodology can be effective and efficient for safety critical systems. Some major issues with formal languages like higher abstraction levels, the need of mathematical skills, developer maturity and high costs can be overcome by using SOFL. SOFL specifically encapsulates three major layers: 1) structured methodology in the early stage of development, 2) object oriented methodology at the detailed level and 3) incorporation of formal methods. In this paper, we have tested the SOFL 3-step approach for the formal specification of a Railway Signaling System, already implemented by using Zed. Afterward we performed a comparison, using certain parameters identified from literature, to assess the appropriateness of Zed and SOFL methodology for the formal specification of a safety critical system. We found SOFL as an instinctive and perceptive for formal specification which overcome the limitations of other formal languages