Abstract
OnTrack automates workflows for railway verification, starting with graphical scheme plans and finishing with automatically generated formal models set up for verification. OnTrack is grounded on an established domain specification language (DSL) and is generic in the formal specification language used. Using a DSL allows the formulation of abstractions that work for verification in several formal specification languages. Here, we demonstrate the workflow using CSP||B and suggest how to extend the tool with further formal specification languages.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bjørner, D.: Formal Software Techniques for Railway Systems. In: CTS 2000 (2000)
dos Santos, O.M., Woodcock, J., Paige, R.F.: Using model transformation to generate graphical counter-examples for the formal analysis of xUML models. In: ICECCS, pp. 117–126. IEEE Computer Society (2011)
Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley Professional (2009)
Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 261–275. Springer, Heidelberg (2012)
Iliasov, A., Romanovsky, A.: SafeCap domain language for reasoning about safety and capacity. In: Workshop on Dependable Transportation Systems. IEEE CS (2012)
James, P., Roggenbach, M.: Designing domain specific languages for verification: First steps. In: ATE 2011. CEUR (2011)
Kolovos, D., Rose, L., Paige, R., García-Domínguez, A.: The Epsilon Book. The Eclipse Foundation (2012)
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and Model Checking Abstractions of Complex Railway Models using CSP∥B. In: HVC 2012. LNCS (to be published)
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Railway modelling in CSP∥B: the double junction case study. In: AVOCS 2012. EASST (2012)
Invensys Rail: Invensys Rail Data Model – Version 1A (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S. (2013). OnTrack: An Open Tooling Environment for Railway Verification. In: Brat, G., Rungta, N., Venet, A. (eds) NASA Formal Methods. NFM 2013. Lecture Notes in Computer Science, vol 7871. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38088-4_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-38088-4_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38087-7
Online ISBN: 978-3-642-38088-4
eBook Packages: Computer ScienceComputer Science (R0)