Abstract
This paper describes another application of the SOFL three-step specification approach in specifying a railway interlocking system in industrial setting. We also explore the way of deriving hazard conditions from formal specifications, and propose a way to analyze the conditions for the assurance of the safety of the interlocking system in the early stage of the development. Our experience shows that SOFL is much more accessible by ordinary practitioners than other existing well-known formal methods and effective in helping practitioners deepen their understanding of the system details.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Boehm, B.W., Basili, V.R.: Software defect reduction top 10 list. IEEE Comput. 34(1), 135–137 (2001)
Bowen, J., Stavridou, V.: Safety-critical methods and systems, formal standards. Softw. Eng. J. 8(4), 189–209 (1993)
Bjørner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978). doi:10.1007/3-540-08766-4
Diller, A.: Z: an introduction to formal methods 23(9), 10–23 (1990). Wiley
Abrial, J.-R.: Modeling in Event-B System and Software Engineering. Cambridge University Press, Cambridge (2010), ISBN-13 978-0-521-89556-9
Efficient Development of Safe Railway Applications Software with EN 50128 Objectives Using SCADE Suite, 3rd edn.. Esterel Technologies, SA (2012)
Liu, S.: Formal engineering for industrial software development using the SOFL method. Springer, Heidelberg (2004), ISBN 3-540-20602-7
Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language LUSTR. IEEE Trans. Softw. Eng. 18(9), 785–793 (1992)
Liu, S., Chen, Y., Nagoya, F., McDermid, J.A.: Formal specification-based inspection for verification of programs. IEEE Trans. Softw. Eng. 38(5), 1100–1122 (2012)
Liu, S., Chen, Y.: A relation-based method combining functional and structural testing for test case generation. J. Syst. Softw. 81(2), 234–248 (2008)
Liu, S., Nakajima, S.: A decompositional approach to automatic test case generation based on formal specifications. In: 4th IEEE International Conference on Secure Software Integration and Reliability Improvement, Singapore, 9–11 June, pp. 147–155 (2010)
Liu, S., Nakajima, S: A “Vibration” method for automatically generating test cases based on formal specifications. In: 18th Asia Pacific Conference on Software Engineering (APSEC 2011), 5–8 December, pp. 73–80. IEEE CS Press, VNU-HCM, Vietnam (2011)
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 369–387 (2000)
DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE), Perros-Guirec, France, 13–16 October, pp. 199–213 (1992)
Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, Jeannette M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999). doi:10.1007/3-540-48119-2_22
Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Yu.: Verifying Chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262–280. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54108-7_14
Zou, L., Zhan, N., Franzle, M., Qin, S.: Verifying simulink diagrams via a hybrid hoare logic pover. In: International Conference on Embedded Software (EMSOFT), Montreal, QC, 29 September 2013–4 October 2013, pp. 1–10 (2013)
Horste, M., Hungar, A., Schnieder, E.: Modelling functionality of train control systems using petri nets. In: FM-RAIL-BOK Workshop, Madrid, Spain, September 23–24, 2013, pp. 46–50 (2013)
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, Sanjit A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378–393. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_29
Study cases of Prover technology, http://www.prover.com/company/casestudies/
Qian, J., Liu, J., Chen, X., Sun, J.: Formal design and verification of zone controller. In: 21st Asia-Pacific Conference on Software Engineering (APSEC 2014), 1–4 December 2014, pp. 375–382. IEEE CS Press, Jeju (2014)
Qian, J., Liu, J., Chen, X., Sun, J.: Modeling and verification of zone controller: the SCADE experience in china’s railway systems. In: ICSE Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS), 23 May 2015, pp. 48–54. IEEE, Florence (2015)
Acknowledgment
This work was supported by CASCO. Shaoying Liu was also partly supported by JSPS KAKENHI grant Number 26240008.
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
Luo, J., Liu, S., Wang, Y., Zhou, T. (2017). Applying SOFL to a Railway Interlocking System in Industry. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2016. Lecture Notes in Computer Science(), vol 10189. Springer, Cham. https://doi.org/10.1007/978-3-319-57708-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-57708-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57707-4
Online ISBN: 978-3-319-57708-1
eBook Packages: Computer ScienceComputer Science (R0)