Formal Verification of the Danish Railway Interlocking Systems
| Autor: | Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska |
|---|---|
| Přispěvatelé: | Huisman, Marieke, van de Pol, Jaco |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: | |
| Zdroj: | Vu, L H, Haxthausen, A E & Peleska, J 2014, Formal Verification of the Danish Railway Interlocking Systems . in M Huisman & J van de Pol (eds), Pre-proceedings of 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014) . University of Twente, C T I T Workshop Proceedings Series, no. WP 14-01, pp. 257-258, 14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014, Enschede, Netherlands, 24/09/2014 . Technical University of Denmark Orbit |
| Popis: | In this paper, we present a method for formal verification of the new Danish railway interlocking systems. We made a generic and reconfigurable model of the behaviors and high-level safety properties of non-collision and nonderailment. This model accommodates sequential release – a new feature in the new Danish interlocking systems. Instantiating the generic model with interlocking configuration data results in a concrete model and high-level safety properties. Using bounded model checking and inductive reasoning, we are able to verify safety properties for model instances corresponding to railway networks of industrial size. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|