User menu

Verification of Railway Interlocking - Compositional Approach with OCRA

Bibliographic reference Limbrée, Christophe ; Cappart, Quentin ; Pecheur, Charles ; Tonetta, Stefano. Verification of Railway Interlocking - Compositional Approach with OCRA.RSSR2016 (Paris, du 28/06/2016 au 30/06/2016). In: Reliability, Safety, and Security of Railway Systems, 2016
Permanent URL http://hdl.handle.net/2078.1/178596
  1. Antoni, M., Ammad, N.: Formal Validation Method and Tools for French Computorized Railway Interlocking Systems, pp. 1–10, June 2008
  2. Bradley Aaron R., SAT-Based Model Checking without Unrolling, Lecture Notes in Computer Science (2011) ISBN:9783642182747 p.70-87, 10.1007/978-3-642-18275-4_7
  3. Busard Simon, Cappart Quentin, Limbrée Christophe, Pecheur Charles, Schaus Pierre, Verification of railway interlocking systems, 10.4204/eptcs.184.2
  4. Cappart, Q., Limbrée, C., Schaus, P., Legay, A.: Verification by discrete simulation of interlocking systems. In: Proceedings of the 29th Annual European Simulation and Modelling Conference, EUROSIS, October 2015
  5. Cavada Roberto, Cimatti Alessandro, Dorigatti Michele, Griggio Alberto, Mariotti Alessandro, Micheli Andrea, Mover Sergio, Roveri Marco, Tonetta Stefano, The nuXmv Symbolic Model Checker, Computer Aided Verification (2014) ISBN:9783319088662 p.334-342, 10.1007/978-3-319-08867-9_22
  6. Cimatti A., Giunchiglia F., Mongardi G., Romano D., Torielli F., Traverso P., Formal Verification of a Railway Interlocking System using Model Checking, 10.1007/s001650050022
  7. Cimatti Alessandro, Griggio Alberto, Mover Sergio, Tonetta Stefano, IC3 Modulo Theories via Implicit Predicate Abstraction, Tools and Algorithms for the Construction and Analysis of Systems (2014) ISBN:9783642548611 p.46-61, 10.1007/978-3-642-54862-8_4
  8. Cimatti Alessandro, Clarke Edmund, Giunchiglia Enrico, Giunchiglia Fausto, Pistore Marco, Roveri Marco, Sebastiani Roberto, Tacchella Armando, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Computer Aided Verification (2002) ISBN:9783540439974 p.359-364, 10.1007/3-540-45657-0_29
  9. Cimatti Alessandro, Corvino Raffaele, Lazzaro Armando, Narasamdya Iman, Rizzo Tiziana, Roveri Marco, Sanseviero Angela, Tchaltsev Andrei, Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System, Computer Aided Verification (2012) ISBN:9783642314230 p.378-393, 10.1007/978-3-642-31424-7_29
  10. Cimatti Alessandro, Dorigatti Michele, Tonetta Stefano, OCRA: A tool for checking the refinement of temporal contracts, 10.1109/ase.2013.6693137
  11. Cimatti, A., Dorigatti, M., Tonetta, S.: Ocra: Othello Contracts Refinement Analysis Versions 1,3. FBK (2015)
  12. Cimatti Alessandro, Tonetta Stefano, Contracts-refinement proof system for component-based embedded systems, 10.1016/j.scico.2014.06.011
  13. Claessen, K., Sörensson, N.: A liveness checking algorithm that counts. In: FMCAD, pp. 52–59. IEEE (2012)
  14. Claessen, K., Sorensson, N.: A liveness checking algorithm that counts. In: Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22–25, 2012, pp. 52–59 (2012). http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462555
  15. Clarke, J.E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
  16. Duggan, P., Borälv, A.: Mathematical proof in an automated environment for railway interlockings. IRSE News Issue 217, Institution of Railway Signal Engineers, 2–6 December 2015. www.irse.org
  17. Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS/FORMAT, pp. 107–115 (2010)
  18. Graf Susanne, Saidi Hassen, Construction of abstract state graphs with PVS, Computer Aided Verification (1997) ISBN:9783540631668 p.72-83, 10.1007/3-540-63166-6_10
  19. Johnston Wendy, Winter Kirsten, van den Berg Lionel, Strooper Paul, Robinson Peter, Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking, FM 2006: Formal Methods (2006) ISBN:9783540372158 p.524-540, 10.1007/11813040_35
  20. McMillan Kenneth L., Symbolic Model Checking, ISBN:9781461363996, 10.1007/978-1-4615-3190-6
  21. Pnueli Amir, The temporal logic of programs, 10.1109/sfcs.1977.32
  22. Sun Pengfei, Collart-dutilleul Simon, Bon Philippe, A model pattern of railway interlocking system by Petri nets, 10.1109/mtits.2015.7223292
  23. Tonetta Stefano, Abstract Model Checking without Computing the Abstraction, FM 2009: Formal Methods (2009) ISBN:9783642050886 p.89-105, 10.1007/978-3-642-05089-3_7
  24. Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 223–238. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-319-17581-2_15
  25. Winter Kirsten, Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (2012) ISBN:9783642340314 p.246-260, 10.1007/978-3-642-34032-1_24
  26. Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Oudshoorn, M. (ed.) Twenty-Fifth Australasian Computer Science Conference (ACSC 2003), pp. 309–316 (2003)
  27. Xu Tianhua, Tang Tao, Gao Chunhai, Cai Baigen, Logic verification of Collision Avoidance System in train control systems, 10.1109/ivs.2009.5164402