Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum
Tóm tắt
Từ khóa
Tài liệu tham khảo
Abrial, J.: The B-Book—Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Abrial, J.: Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.: The ABZ-2018 case study with Event-B. In: ABZ, Volume 10817 of LNCS, pp. 322–337. Springer (2018)
Abrial, J., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)
Arcaini, P., Jezek, P., Kofron, J.: Modelling the Hybrid ERTMS/ETCS Level 3 case study in S pin. In: ABZ, Volume 10817 of LNCS, pp. 277–291. Springer (2018)
Couto, R., Campos, J.C., Macedo, N., Cunha, A.: Improving the visualization of Alloy instances. In: F-IDE@FLoC, Volume 284 of EPTCS, pp. 37–52 (2018)
Cunha, A., Macedo, N.: Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. In: ABZ, Volume 10817 of LNCS, pp. 307–321. Springer (2018)
Dghaym, D., Poppleton, M., Snook, C.: Diagram-led formal modelling using iUML-B for Hybrid ERTMS Level 3. In: ABZ, Volume 10817 of LNCS, pp. 338–352. Springer (2018)
EEIG ERTMS Users Group: Hybrid ERTMS/ETCS Level 3—principles. http://www.ertms.be/sites/default/files/2018-03/16E0421A_HL3.pdf 16E042, version 1A (2017)
EEIG ERTMS Users Group: Hybrid ERTMS/ETCS Level 3—principles. https://ertms.be/sites/default/files/2018-07/16E0421C_HL3-clean.pdf 16E042, version 1C (2018)
ERA, UNISIG, and EEIG ERTMS Users Group: Glossary of unisig terms and abbreviations. https://www.era.europa.eu/filebrowser/download/492_en SUBSET-023, issue 3.3.0 (2016)
Fotso, S., Frappier, M., Laleau, R., Mammar, A.: Modeling the Hybrid ERTMS/ETCS Level 3 standard using a formal requirements engineering approach. In: ABZ, Volume 10817 of LNCS, pp. 262–276. Springer (2018)
Hansen, D., Leuschel, M., Schneider, D., Krings, S., Körner, P., Naulin, T., Nayeri, N., Skowron, F.: Using a formal B model at runtime in a demonstration of the ETCS Hybrid Level 3 concept with real trains. In: ABZ, Volume 10817 of LNCS, pp. 292–306. Springer (2018)
Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS/ETCS Level 3 case study. In: ABZ, Volume 10817 of LNCS, pp. 251–261. Springer (2018)
Holzmann, G.J.: The SPIN Model Checker-Primer and Reference Manual. Addison-Wesley, Boston (2004)
INESC TEC and ONERA: Electrum Analyzer, v1.0. Available under the MIT License at https://github.com/haslab/Electrum/releases/tag/v1.0 (2018)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)
Leuschel, M., Butler, M.: ProB: A model checker for B. In: FME, Volume 2805 of LNCS, pp. 855–874. Springer (2003)
Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: SIGSOFT FSE, pp. 373–383. ACM (2016)
Mammar, A., Frappier, M., Fotso, S., Laleau, R.: An Event-B model of the Hybrid ERTMS/ETCS Level 3 standard. In: ABZ, Volume 10817 of LNCS, pp. 353–366. Springer (2018)
Mammar, A., Laleau, R.: On the use of domain and system knowledge modeling in goal-based Event-B specifications. In: ISoLA, Volume 9952 of LNCS, pp. 325–339 (2016)
Moreira, J.M., Cunha, A., Macedo, N.: An ORCID based synchronization framework for a national CRIS ecosystem. F1000Research 4, 181 (2015)
Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, pp. 29–30. http://eprints.soton.ac.uk/365301/ (2014)
Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)