OnTrack: The Railway Verification Toolset

P. James; F. Moller; Hoang Nga Nguyen; M. Roggenbach; H. Treharne; X. Wang

doi:10.1007/978-3-319-47169-3_21

OnTrack: The Railway Verification Toolset

P. James, F. Moller, Hoang Nga Nguyen, M. Roggenbach, H. Treharne, X. Wang

Research output: Contribution to conference › Paper

2 Citations (Scopus)

Abstract

The verification of railway interlocking systems is a challenging task for which a number of different modelling, simulation and verification approaches have been proposed. In this paper, we present the OnTrack toolset. In OnTrack, application data for the railway domain is represented using a domain specific language. This data can be entered manually or imported from standard data formats. OnTrack then comprises of a number of different model transformations that allow the user to automatically generate formal models for a specific approach, e.g., in CASL, CSP, or CSP||B. Other transformations offer abstractions on the application data to address scalability.

Original language	English
Pages	294-296
DOIs	https://doi.org/10.1007/978-3-319-47169-3_21
Publication status	Published - 5 Oct 2016
Event	7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016

Conference

Conference	7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
Abbreviated title	ISoLA 2016
Country/Territory	Greece
City	Corfu
Period	10/10/16 → 14/10/16

Bibliographical note

The full text is not available on the repository

Access to Document

10.1007/978-3-319-47169-3_21

Cite this

@conference{b24a2c71963a442a859c6d95898dee49,

title = "OnTrack: The Railway Verification Toolset",

abstract = "The verification of railway interlocking systems is a challenging task for which a number of different modelling, simulation and verification approaches have been proposed. In this paper, we present the OnTrack toolset. In OnTrack, application data for the railway domain is represented using a domain specific language. This data can be entered manually or imported from standard data formats. OnTrack then comprises of a number of different model transformations that allow the user to automatically generate formal models for a specific approach, e.g., in CASL, CSP, or CSP||B. Other transformations offer abstractions on the application data to address scalability.",

author = "P. James and F. Moller and Nguyen, \{Hoang Nga\} and M. Roggenbach and H. Treharne and X. Wang",

note = "The full text is not available on the repository; 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

year = "2016",

month = oct,

day = "5",

doi = "10.1007/978-3-319-47169-3\_21",

language = "English",

pages = "294--296",

}

TY - CONF

T1 - OnTrack: The Railway Verification Toolset

AU - James, P.

AU - Moller, F.

AU - Nguyen, Hoang Nga

AU - Roggenbach, M.

AU - Treharne, H.

AU - Wang, X.

N1 - The full text is not available on the repository

PY - 2016/10/5

Y1 - 2016/10/5

N2 - The verification of railway interlocking systems is a challenging task for which a number of different modelling, simulation and verification approaches have been proposed. In this paper, we present the OnTrack toolset. In OnTrack, application data for the railway domain is represented using a domain specific language. This data can be entered manually or imported from standard data formats. OnTrack then comprises of a number of different model transformations that allow the user to automatically generate formal models for a specific approach, e.g., in CASL, CSP, or CSP||B. Other transformations offer abstractions on the application data to address scalability.

AB - The verification of railway interlocking systems is a challenging task for which a number of different modelling, simulation and verification approaches have been proposed. In this paper, we present the OnTrack toolset. In OnTrack, application data for the railway domain is represented using a domain specific language. This data can be entered manually or imported from standard data formats. OnTrack then comprises of a number of different model transformations that allow the user to automatically generate formal models for a specific approach, e.g., in CASL, CSP, or CSP||B. Other transformations offer abstractions on the application data to address scalability.

UR - https://www.scopus.com/pages/publications/84993939750

U2 - 10.1007/978-3-319-47169-3_21

DO - 10.1007/978-3-319-47169-3_21

M3 - Paper

SP - 294

EP - 296

T2 - 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation

Y2 - 10 October 2016 through 14 October 2016

ER -

OnTrack: The Railway Verification Toolset

Abstract

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this