Abstract
With the increasing dependency of our society on automated systems, their correctness is of uttermost importance. Formal methods for software development, such as the B-Method, belong to rigorous approaches that may ensure the correctness. They offer mathematical apparatuses to prove that the software under development meets the corresponding requirements. But the need to comprehend such apparatus makes formal methods unpopular with students. They may not see the reasons why to use them. And many formal method courses do not include executable software development or the software developed is not used in an appropriate environment. Both problems are addressed by the TD/TS2JC toolset, described in this chapter. The toolset provides an appropriate virtual railway environment, where verified software controllers can run. The controllers can be developed with any formal method that offers translation to the Java programming language. The chapter also describes two of several control interfaces the toolset supports. It also introduces a compact, four to six hour long, course on verified software development with the B-Method, which utilizes the toolset.
This chapter is a result of the implementation of the Erasmus+ Key Action 2 project No. 2017-1-SK01-KA203-035402: “Focusing Education on Composability, Comprehensibility and Correctness of Working Software”.
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
Notes
- 1.
The control module used in this case is the one from Listing 2 and the method is on lines 49–51.
- 2.
We use the term “specification unit” as the corresponding parts (units) of formal specifications are named differently in different FMs. For example, they are called operations in the B-Method, events in the Event-B and schemas in the Perfect Developer.
- 3.
Technically, the enumerated sets are classes, too.
- 4.
If a scenario contains switches, their getters are mandatory, too.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New Yor (2010)
Almeida, J.B., Frade, M.J., Pinto, J.S., De Sousa, S.M.: Rigorous Software Development: An Introduction to Program Verification. Springer, London (2011). https://doi.org/10.1007/978-0-85729-018-2
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_13
Korečko, Š.: TD/TS2JavaConn toolset package. https://hron.fei.tuke.sk/korecko/FMInGamesExp/resources/allInOneTDTS2J.zip (2019)
Korečko, Š.: Verified software development in B-Method short course package (2019). https://hron.fei.tuke.sk/korecko/cefp19/cefp19BmethodPack.zip
Korečko, Š, Sobota, B.: Computer games as virtual environments for safety-critical software validation. J. Inf. Organ. Sci. 41(2), 197–212 (2017)
Korečko, Š., Sorád, J.: Using simulation games in teaching formal methods for software development. In: Queirós, R. (ed.) Innovative Teaching Strategies and New Learning Paradigms in Computer Programming, pp. 106–130. IGI Global (2015)
Korečko, Š, Sorád, J., Dudláková, Z., Sobota, B.: A toolset for support of teaching formal software development. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 278–283. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_21
Lano, K.: The B Language and Method: A Guide to Practical Formal Development, 1st edn. Springer, New York (1996). https://doi.org/10.1007/978-1-4471-1494-9
Larsen, P., Fitzgerald, J., Riddle, S.: Practice-oriented courses in formal methods using vdm++. Formal Aspects Comput. 21(3), 245–257 (2009). https://doi.org/10.1007/s00165-008-0068-5
Liu, S., Takahashi, K., Hayashi, T., Nakayama, T.: Teaching formal methods in the context of software engineering. SIGCSE Bull. 41(2), 17–23 (2009). https://doi.org/10.1145/1595453.1595457
Reed, J.N., Sinclair, J.E.: Motivating study of formal methods in the classroom. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 32–46. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_3
Schneider, S.: The B-Method: An Introduction. Cornerstones of Computing, Palgrave (2001)
Spivey, J.M., Abrial, J.: The Z Notation. Prentice Hall Hemel Hempstead, Englewood Cliffs (1992)
Train director homepage (2020). https://www.backerstreet.com/traindir/en/trdireng.php
Atelier B homepage (2021). https://www.atelierb.eu/en/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Korečko, Š. (2023). Utilizing Rail Traffic Control Simulator in Verified Software Development Courses. In: Porkoláb, Z., Zsók, V. (eds) Composability, Comprehensibility and Correctness of Working Software. CEFP 2019. Lecture Notes in Computer Science, vol 11950. Springer, Cham. https://doi.org/10.1007/978-3-031-42833-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-031-42833-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-42832-6
Online ISBN: 978-3-031-42833-3
eBook Packages: Computer ScienceComputer Science (R0)