Rule-Based Consistency Checking of Railway Infrastructure Designs

Abstract

Railway systems designs deal with complex and large-scale, safety-critical infrastructures, where formal methods play an important role, especially in verifying the safety of so-called interlockings through model checking. Model checking deals with state change and rather complex properties, usually incurring considerable computational burden. In contrast to this, we focus on static infrastructure properties, based on design guidelines and heuristics. The purpose is to automate much of the manual work of the railway engineers through software that can do verification on-the-fly. In consequence, this paper describes the integration of formal methods into the design process, by formalizing relevant technical rules and expert knowledge. We employ a variant of Datalog and use the standardized “railway markup language” railML as basis and exchange format for the formalization. We describe a prototype tool and its (ongoing) integration in industrial railway CAD software. We apply this tool chain in a Norwegian railway project, the upgrade of the Arna railway station.