Formal development and verification of a distributed railway control system

Anne Elisabeth Haxthausen; J. Peleska

doi:10.1109/32.879808

Formal development and verification of a distributed railway control system

Anne Elisabeth Haxthausen
, J. Peleska

Research output: Contribution to journal › Journal article › Research › peer-review

1048 Downloads (Orbit)

Abstract

The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.

Original language	English
Journal	IEEE Transaction on Software Engineering
Volume	26
Issue number	8
Pages (from-to)	687-701
ISSN	0098-5589
DOIs	https://doi.org/10.1109/32.879808
Publication status	Published - 2000

Bibliographical note

Copyright: 2000 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

Access to Document

10.1109/32.879808

AnneFinal published version, 278 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

@article{29f1ac283bc14651bfbce09aec339cc1,

title = "Formal development and verification of a distributed railway control system",

abstract = "The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.",

author = "Haxthausen, \{Anne Elisabeth\} and J. Peleska",

note = "Copyright: 2000 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE",

year = "2000",

doi = "10.1109/32.879808",

language = "English",

volume = "26",

pages = "687--701",

journal = "IEEE Transaction on Software Engineering",

issn = "0098-5589",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "8",

}

TY - JOUR

T1 - Formal development and verification of a distributed railway control system

AU - Haxthausen, Anne Elisabeth

AU - Peleska, J.

N1 - Copyright: 2000 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

PY - 2000

Y1 - 2000

N2 - The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.

AB - The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.

U2 - 10.1109/32.879808

DO - 10.1109/32.879808

M3 - Journal article

SN - 0098-5589

VL - 26

SP - 687

EP - 701

JO - IEEE Transaction on Software Engineering

JF - IEEE Transaction on Software Engineering

IS - 8

ER -

Formal development and verification of a distributed railway control system

Abstract

Bibliographical note

Access to Document

OpenUrl availability

Fingerprint

Cite this