Skip to main content
SpringerLink
Log in
Book cover

International Conference on Software Engineering and Formal Methods

SEFM 2017: Software Engineering and Formal Methods pp 87–103Cite as

Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10469))

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. 1.

    Authorities typically make small adjustments to regulations several times per year, whereas engineering best practices can be revised at any time.

  2. 2.

    Such expert knowledge is often seen as proprietary valuable assets of the company.

  3. 3.

    http://railcomplete.no.

  4. 4.

    The examples presented in this text are English translations of originally Norwegian content.

  5. 5.

    Norwegian infrastructure manager Bane NOR’s regulations: https://trv.jbv.no/.

References

  1. 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

    Article  MathSciNet  MATH  Google Scholar 

  2. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. 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

    Book  Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  6. 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

    Article  MathSciNet  MATH  Google Scholar 

  7. Johannisson, K.: Natural language specifications. In: Beckert et al. [3], pp. 317–333. doi:10.1007/978-3-540-69061-0_7

  8. Kensing, F., Blomberg, J.: Participatory design: issues and concerns. Comput. Support. Coop. Work (CSCW) 7(3), 167–185 (1998). doi:10.1023/A:1008689307411

    Article  Google Scholar 

  9. Kuhn, T.: A survey and classification of controlled natural languages. Comput. Linguist. 40(1), 121–170 (2014). doi:10.1162/COLI_a_00168

    Article  Google Scholar 

  10. Ljunglöf, P.: Editing syntax trees on the surface. In: NoDaLiDa 2011, pp. 138–145 (2011)

    Google Scholar 

  11. 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)

    Google Scholar 

  12. 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

    Article  Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. 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

    Chapter  Google Scholar 

  15. 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

    Article  MathSciNet  MATH  Google Scholar 

  16. Ranta, A.: Grammatical framework. J. Funct. Program. 14(2), 145–189 (2004). doi:10.1017/S0956796803004738

    Article  MathSciNet  MATH  Google Scholar 

  17. 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

  18. 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

    Chapter  Google Scholar 

  19. Sharp, H., Rogers, Y., Preece, J.: Interaction Design: Beyond Human-Computer Interaction. Wiley, New York (2007)

    Google Scholar 

  20. Ullman, J.D.: Principles of Database and Knowledge-Base Systems. CSPP, New York (1988)

    Google Scholar 

  21. 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)

    Google Scholar 

  22. 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

    Chapter  Google Scholar 

Download references

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

  1. RailComplete AS, Sandvika, Norway

    Bjørnar Luteberget

  2. Department of Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden

    John J. Camilleri & Gerardo Schneider

  3. Department of Informatics, University of Oslo, Oslo, Norway

    Christian Johansen

Authors
  1. Bjørnar Luteberget
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John J. Camilleri
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christian Johansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gerardo Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christian Johansen .

Editor information

Editors and Affiliations

  1. University of Trento, Trento, Italy

    Alessandro Cimatti

  2. Mälardalen University, Västerås, Sweden

    Marjan Sirjani

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation