Skip to main content
SpringerLink
Log in

Verification of Scheme Plans Using CSP\(||\)B

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8368))

Included in the following conference series:

Abstract

The paper presents a tool-supported approach to graphically editing scheme plans and their safety verification. The graphical tool is based on a Domain Specific Language which is used as the basis for transformation to a CSP\(\parallel \)B formal model of a scheme plan. The models produced utilise a variety of abstraction techniques that make the analysis of large scale plans feasible. The techniques are applicable to other modelling languages besides CSP\(\parallel \)B. We use the ProB tool to ensure the safety properties of collision, derailment and run-through freedom.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    OnTrack available for download from http://www.csp-b.org.

  2. 2.

    Examples available for download from http://www.csp-b.org.

  3. 3.

    EMF and GMF stand for Eclipse Modeling Framework and Graphical Modeling Project, respectively.

References

  1. Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Combining event-based and state-based modelling for railway verification. Technical report CS-12-02, University of Surrey (2012)

    Google Scholar 

  2. Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Using ProB and CSP\(||\)B for railway modelling. In: Proceedings of IFM 2012 and ABZ 2012 Posters and Tool Demos Session, pp. 31–35 (2012)

    Google Scholar 

  3. Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Railway modelling in CSP\(||\)B: The double junction case study. Electron. Commun. EASST 53 (2012)

    Google Scholar 

  4. Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP\(||\)B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2013. LNCS, vol. 7857, pp. 193–208. Springer, Heidelberg (2013)

    Google Scholar 

  5. James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Technical report CS-13-03, University of Surrey (2013)

    Google Scholar 

  6. James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: OnTrack: an open tooling environment for railway verification. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 435–440. Springer, Heidelberg (2013)

    Google Scholar 

  7. James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT (to appear)

    Google Scholar 

  8. Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17(4), 390–422 (2005)

    Article  MATH  Google Scholar 

  9. Winter, K., Robinson, N.: Modelling large railway interlockings and model checking small ones. In: Proceedings of the 26th Australasian Computer Science Conference, pp. 309–316. Australian Computer Society, Inc. (2003)

    Google Scholar 

  10. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  11. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  12. Morgan, C.: Of wp and CSP. In: Beauty is our business: a birthday salute to E. W. Dijkstra, pp. 319–326 (1990)

    Google Scholar 

  13. ProB: The ProB animator and model checker (ProB 1.3.6-final). http://www.stups.uni-duesseldorf.de/ProB. Accessed 1 May 2013

  14. Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley Professional, Upper Saddle River (2009)

    Google Scholar 

  15. Kolovos, D., Rose, L., Paige, R., García-Domínguez, A.: The Epsilon Book. The Eclipse Foundation (2012)

    Google Scholar 

  16. Bjørner, D.: Formal software techniques for railway systems. In: CTS 2000 (2000)

    Google Scholar 

  17. Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683–709 (2011)

    Article  MathSciNet  Google Scholar 

  18. Sabatier, D., Burdy, L., Requet, A., Guéry, J.: Formal proofs for the NYCT line 7 (flushing) modernization project. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 369–372. Springer, Heidelberg (2012)

    Google Scholar 

  19. Simpson, A., Woodcock, J., Davies, J.: The mechanical verification of solid-state interlocking geographic data. In: Formal Methods Pacific 97. Springer, Heidelberg (1997)

    Google Scholar 

  20. Morley, M.J.: Safety in railway signalling data: a behavioural analysis. In: 6th International Workshop on HOLTPA, pp. 464–474. Springer, Heidelberg (1993)

    Google Scholar 

  21. Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)

    Article  Google Scholar 

  22. Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS/FORMAT 2010, pp. 107–115 (2011)

    Google Scholar 

  23. Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlockings. ENTCS 250, 19–31 (2009)

    Google Scholar 

  24. James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. Electr. Commun. EASST 35 (2010)

    Google Scholar 

  25. Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A., Tchaltsev, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378–393. Springer, Heidelberg (2012)

    Google Scholar 

  26. Winter, K.: Model checking railway interlocking systems. Aust. Comput. Sci., Commun. 24(1), 303–310 (2002)

    Google Scholar 

  27. Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  28. Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS/FORMAT, pp. 107–115 (2010)

    Google Scholar 

  29. Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246–260. Springer, Heidelberg (2012)

    Google Scholar 

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

    Google Scholar 

  31. Heitmeyer, C.L., Kirby, J., Labaw, B.G., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans. Softw. Eng. 24(11), 927–948 (1998)

    Article  Google Scholar 

  32. Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways - an approach in timed CSP. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 54–68. Springer, Heidelberg (2012)

    Google Scholar 

Download references

Acknowlegements

Thanks to S. Chadwick and D. Taylor from the company Siemens Rail Automation for their support and encouraging feedback.

Author information

Authors and Affiliations

  1. Swansea University, Swansea, UK

    Philip James, Faron Moller & Markus Roggenbach

  2. University of Surrey, Surrey, UK

    Steve Schneider, Helen Treharne & Matthew Trumble

  3. University of Nottingham, Nottingham, UK

    Hoang Nga Nguyen

  4. VU University Amsterdam, Amsterdam, The Netherlands

    David Williams

Authors
  1. Philip James
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Faron Moller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hoang Nga Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Markus Roggenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Steve Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Helen Treharne
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Matthew Trumble
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. David Williams
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hoang Nga Nguyen .

Editor information

Editors and Affiliations

  1. Brunel University, Uxbridge, Middlesex, United Kingdom

    Steve Counsell

  2. Universidad Complutense de Madrid, Madrid, Spain

    Manuel Núñez

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

James, P. et al. (2014). Verification of Scheme Plans Using CSP\(||\)B. In: Counsell, S., Núñez, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science(), vol 8368. Springer, Cham. https://doi.org/10.1007/978-3-319-05032-4_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05032-4_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-05031-7

  • Online ISBN: 978-3-319-05032-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation