Formal Specification Of Environmental Aspects Of A Railway Interlocking System Based On A Conceptual Model

Relay-based Railway Interlocking Systems (RIS) are developed with the objective of controlling the movement of trains in a safe manner. However, these systems are generally specified by informal languages whose analyses are made by human inspection, which are error prone. A previous work presented an approach for specifying these systems in a formal language in order to automatically prove safety properties. Nevertheless, despite the impact of the environment over the system operation, the approach allows only the specification of the electrical components behaviour. Hence, the environment must be considered in the system specification in order to guarantee its safety. This paper presents the application of a higher level of modelling abstraction, conceptual modelling, which may provide a conceptual clarification of the RIS environment. This proposed conceptual model allows a semantic analysis of the environmental impact over the system and the description of other safety properties that have not been considered in the formal specification. In this work, an ontology built for the critical systems modelling is used in order to provide a terminological harmonisation between the physical elements of the system and the environment. The conceptual model allows a safety-oriented improvement of the RIS formal specification as well as it provides a common, shared and unambiguous view of both system and environment.