Rule-Based Consistency Checking of Railway Infrastructure Designs

Railway 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 (chiefly in terms of memory, known as state-space explosion problem). 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 railway 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, developed under the name RailCOMPLETE (R). We apply this tool chain in a Norwegian railway project, the upgrade of the Arna railway station.