Abstract
Designs of railway infrastructure (tracks, signalling and control systems, etc.) need to comply with comprehensive sets of regulations describing safety requirements, engineering conventions, and design heuristics. We have previously worked on automating the verification of railway designs against such regulations, and integrated a verification tool based on Datalog reasoning into the CAD tools of railway engineers. This was used in a pilot project at Norconsult AS (formerly Anacon AS). In order to allow railway engineers with limited logic programming experience to participate in the verification process, in this work we introduce a controlled natural language, RailCNL, which is designed as a middle ground between informal regulations and Datalog code. Phrases in RailCNL correspond closely to those in the regulation texts, and can be translated automatically into the input language of the verifier. We demonstrate a prototype system which, upon detecting regulation violations, traces back from errors in the design through the CNL to the marked-up original text, allowing domain experts to examine the correctness of each translation step and better identify sources of errors. We also describe our design methodology, based on CNL best practices and previous experience with creating verification front-end languages.
Supported by the Norwegian Research Council project RailCons – Aut. Methods and Tools for Ensuring Consistency of Railway Designs, and by the Swedish Research Council grant nr. 2012-5746 – Reliable Multilingual Digital Communication: Methods and Applications.
This is a preview of subscription content, log in via an institution.
Notes
- 1.
Authorities typically make small adjustments to regulations several times per year, whereas engineering best practices can be revised at any time.
- 2.
Such expert knowledge is often seen as proprietary valuable assets of the company.
- 3.
- 4.
The examples presented in this text are English translations of originally Norwegian content.
- 5.
Norwegian infrastructure manager Bane NOR’s regulations: https://trv.jbv.no/.
References
Angelov, K., Camilleri, J.J., Schneider, G.: A framework for conflict analysis of normative texts written in controlled natural language. JLAP 82(5), 216–240 (2013). doi:10.1016/j.jlap.2013.03.002
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007). doi:10.1007/978-3-540-69061-0
Camilleri, J.J., Paganelli, G., Schneider, G.: A CNL for contract-oriented diagrams. In: Davis, B., Kaljurand, K., Kuhn, T. (eds.) CNL 2014. LNCS (LNAI), vol. 8625, pp. 135–146. Springer, Cham (2014). doi:10.1007/978-3-319-10223-8_13
Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge (2000)
James, P., Roggenbach, M.: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans. Math. Comput. Sci. 8(1), 11–38 (2014). doi:10.1007/s11786-014-0174-0
Johannisson, K.: Natural language specifications. In: Beckert et al. [3], pp. 317–333. doi:10.1007/978-3-540-69061-0_7
Kensing, F., Blomberg, J.: Participatory design: issues and concerns. Comput. Support. Coop. Work (CSCW) 7(3), 167–185 (1998). doi:10.1023/A:1008689307411
Kuhn, T.: A survey and classification of controlled natural languages. Comput. Linguist. 40(1), 121–170 (2014). doi:10.1162/COLI_a_00168
Ljunglöf, P.: Editing syntax trees on the surface. In: NoDaLiDa 2011, pp. 138–145 (2011)
Luteberget, B., Camilleri, J.J., Johansen, C., Schneider, G.: Participatory Verification of Railway Infrastructure Regulations using RailCNL (long version). Technical report 465, University of Oslo (2017)
Luteberget, B., Johansen, C.: Efficient verification of railway infrastructure designs against standard regulations. Formal Methods Syst. Des., 1–32 (2017). doi:10.1007/s10703-017-0281-z
Luteberget, B., Johansen, C., Steffen, M.: Rule-based consistency checking of railway infrastructure designs. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 491–507. Springer, Cham (2016). doi:10.1007/978-3-319-33693-0_31
Meza Moreno, M.S., Bringert, B.: Interactive multilingual web applications with grammatical framework. In: Nordström, B., Ranta, A. (eds.) GoTAL 2008. LNCS (LNAI), vol. 5221, pp. 336–347. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85287-2_32
Prisacariu, C., Schneider, G.: A dynamic deontic logic for complex contracts. J. Logic Algebr. Program. (JLAP) 81(4), 458–490 (2012). doi:10.1016/j.jlap.2012.03.003
Ranta, A.: Grammatical framework. J. Funct. Program. 14(2), 145–189 (2004). doi:10.1017/S0956796803004738
Ranta, A., Camilleri, J., Détrez, G., Enache, R., Hallgren, T.: Grammar tool manual and best practices. Technical report, MOLTO Deliverable D2.3, MOLTO Consortium, Göteborg (2012). http://www.molto-project.eu/biblio/deliverable/grammar-tools-and-best-practices
Ranta, A., Enache, R., Détrez, G.: Controlled language for everyday use: the MOLTO phrasebook. In: Rosner, M., Fuchs, N.E. (eds.) CNL 2010. LNCS (LNAI), vol. 7175, pp. 115–136. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31175-8_7
Sharp, H., Rogers, Y., Preece, J.: Interaction Design: Beyond Human-Computer Interaction. Wiley, New York (2007)
Ullman, J.D.: Principles of Database and Knowledge-Base Systems. CSPP, New York (1988)
Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for railway interlocking systems. In: FORMS/FORMAT 2014, pp. 200–209. TU Braunschweig (2014)
Wyner, A., et al.: On controlled natural languages: properties and prospects. In: Fuchs, N.E. (ed.) CNL 2009. LNCS (LNAI), vol. 5972, pp. 281–289. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14418-9_17
Acknowledgements
We thank Martin Steffen and Aarne Ranta for numerous useful interactions, and Claus Feyling (CEO of RailCOMPLETE AS) for allowing us to use the time of his engineers for testing our results and other railway specific interactions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Luteberget, B., Camilleri, J.J., Johansen, C., Schneider, G. (2017). Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL. In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-66197-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66196-4
Online ISBN: 978-3-319-66197-1
eBook Packages: Computer ScienceComputer Science (R0)