Formal Verification of Railway Timetables - Using the UPPAAL Model Checker

Anne E. Haxthausen*, Kristian Hede

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

44 Downloads (Pure)

Abstract

This paper considers the challenge of validating railway timetables and investigates how formal methods can be used for that. The paper presents a re-configurable, formal model which can be configured with a timetable for a railway network, properties of that network, and various timetabling parameters (such as station and line capacities, headways, and minimum running times) constraining the allowed train behaviour. The formal model describes the system behaviour of trains driving according to the given railway timetable. Model checking can then be used to check that driving according to the timetable does not lead to illegal system states. The method has successfully been applied to a real world case study: a time table for 12 trains at Nærumbanen in Denmark.

Original languageEnglish
Title of host publicationFrom Software Engineering to Formal Methods and Tools, and Back
PublisherSpringer
Publication date1 Jan 2019
Pages433-448
ISBN (Print)978-3-030-30984-8
DOIs
Publication statusPublished - 1 Jan 2019
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11865 LNCS
ISSN0302-9743

Keywords

  • Formal methods
  • Model checking
  • Railways
  • Timetables
  • UPPAAL

Cite this

Haxthausen, A. E., & Hede, K. (2019). Formal Verification of Railway Timetables - Using the UPPAAL Model Checker. In From Software Engineering to Formal Methods and Tools, and Back (pp. 433-448). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol.. 11865 LNCS https://doi.org/10.1007/978-3-030-30985-5_25
Haxthausen, Anne E. ; Hede, Kristian. / Formal Verification of Railway Timetables - Using the UPPAAL Model Checker. From Software Engineering to Formal Methods and Tools, and Back. Springer, 2019. pp. 433-448 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11865 LNCS).
@inbook{16cbeed7999943ff9f7480b10cab7e27,
title = "Formal Verification of Railway Timetables - Using the UPPAAL Model Checker",
abstract = "This paper considers the challenge of validating railway timetables and investigates how formal methods can be used for that. The paper presents a re-configurable, formal model which can be configured with a timetable for a railway network, properties of that network, and various timetabling parameters (such as station and line capacities, headways, and minimum running times) constraining the allowed train behaviour. The formal model describes the system behaviour of trains driving according to the given railway timetable. Model checking can then be used to check that driving according to the timetable does not lead to illegal system states. The method has successfully been applied to a real world case study: a time table for 12 trains at N{\ae}rumbanen in Denmark.",
keywords = "Formal methods, Model checking, Railways, Timetables, UPPAAL",
author = "Haxthausen, {Anne E.} and Kristian Hede",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-30985-5_25",
language = "English",
isbn = "978-3-030-30984-8",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "433--448",
booktitle = "From Software Engineering to Formal Methods and Tools, and Back",

}

Haxthausen, AE & Hede, K 2019, Formal Verification of Railway Timetables - Using the UPPAAL Model Checker. in From Software Engineering to Formal Methods and Tools, and Back. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11865 LNCS, pp. 433-448. https://doi.org/10.1007/978-3-030-30985-5_25

Formal Verification of Railway Timetables - Using the UPPAAL Model Checker. / Haxthausen, Anne E.; Hede, Kristian.

From Software Engineering to Formal Methods and Tools, and Back. Springer, 2019. p. 433-448 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11865 LNCS).

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

TY - CHAP

T1 - Formal Verification of Railway Timetables - Using the UPPAAL Model Checker

AU - Haxthausen, Anne E.

AU - Hede, Kristian

PY - 2019/1/1

Y1 - 2019/1/1

N2 - This paper considers the challenge of validating railway timetables and investigates how formal methods can be used for that. The paper presents a re-configurable, formal model which can be configured with a timetable for a railway network, properties of that network, and various timetabling parameters (such as station and line capacities, headways, and minimum running times) constraining the allowed train behaviour. The formal model describes the system behaviour of trains driving according to the given railway timetable. Model checking can then be used to check that driving according to the timetable does not lead to illegal system states. The method has successfully been applied to a real world case study: a time table for 12 trains at Nærumbanen in Denmark.

AB - This paper considers the challenge of validating railway timetables and investigates how formal methods can be used for that. The paper presents a re-configurable, formal model which can be configured with a timetable for a railway network, properties of that network, and various timetabling parameters (such as station and line capacities, headways, and minimum running times) constraining the allowed train behaviour. The formal model describes the system behaviour of trains driving according to the given railway timetable. Model checking can then be used to check that driving according to the timetable does not lead to illegal system states. The method has successfully been applied to a real world case study: a time table for 12 trains at Nærumbanen in Denmark.

KW - Formal methods

KW - Model checking

KW - Railways

KW - Timetables

KW - UPPAAL

U2 - 10.1007/978-3-030-30985-5_25

DO - 10.1007/978-3-030-30985-5_25

M3 - Book chapter

AN - SCOPUS:85073683321

SN - 978-3-030-30984-8

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 433

EP - 448

BT - From Software Engineering to Formal Methods and Tools, and Back

PB - Springer

ER -

Haxthausen AE, Hede K. Formal Verification of Railway Timetables - Using the UPPAAL Model Checker. In From Software Engineering to Formal Methods and Tools, and Back. Springer. 2019. p. 433-448. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11865 LNCS). https://doi.org/10.1007/978-3-030-30985-5_25