{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T01:02:45Z","timestamp":1726102965385},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030614669"},{"type":"electronic","value":"9783030614676"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-61467-6_30","type":"book-chapter","created":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T01:04:26Z","timestamp":1603674266000},"page":"467-485","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-7196-6609","authenticated-orcid":false,"given":"Davide","family":"Basile","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-0636-5663","authenticated-orcid":false,"given":"Alessio","family":"Ferrari","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Masullo","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-4562-8777","authenticated-orcid":false,"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Piattino","sequence":"additional","affiliation":[]},{"given":"Daniele","family":"Trentini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,27]]},"reference":[{"key":"30_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"30_CR2","unstructured":"ASTRail Deliverable D4.3: Validation Report. \nhttp:\/\/astrail.eu\/download.aspx?id=d7ae1ebf-52b4-4bde-b25e-ae251fd906df"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-98938-9_2","volume-title":"Integrated Formal Methods","author":"D Basile","year":"2018","unstructured":"Basile, D., et al.: On the industrial uptake of formal methods in the railway domain. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20\u201329. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-98938-9_2"},{"issue":"2","key":"30_CR4","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH ter Beek","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119\u2013135 (2011). \nhttps:\/\/doi.org\/10.1016\/j.scico.2010.07.002","journal-title":"Sci. Comput. Program."},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-030-30942-8_46","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"MH ter Beek","year":"2019","unstructured":"ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762\u2013772. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-30942-8_46"},{"key":"30_CR6","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST 2006), pp. 125\u2013126. IEEE (2006). \nhttps:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"30_CR7","unstructured":"Bendisposto, J., et al.: ProB 2.0 tutorial. In: Butler, M., Hallerstede, S., Wald\u00e9n, M. (eds.) Proceedings of the 4th Rodin User and Developer Workshop. TUCS Lecture Notes, Turku Centre for Computer Science (2013)"},{"key":"30_CR8","doi-asserted-by":"publisher","unstructured":"Berglehner, R., Rasheeq, A.: An approach to improve SysML railway specification using UML-B and EVENT-B. In: Poster at the 3rd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail 2019) (2019). \nhttps:\/\/doi.org\/10.13140\/RG.2.2.21925.45288","DOI":"10.13140\/RG.2.2.21925.45288"},{"key":"30_CR9","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/j.ress.2013.06.032","volume":"120","author":"S Bernardi","year":"2013","unstructured":"Bernardi, S., et al.: Enabling the usage of UML in the verification of railway systems: the DAM-rail approach. Rel. Eng. Syst. Saf. 120, 112\u2013126 (2013). \nhttps:\/\/doi.org\/10.1016\/j.ress.2013.06.032","journal-title":"Rel. Eng. Syst. Saf."},{"key":"30_CR10","doi-asserted-by":"publisher","unstructured":"Besnard, V., Brun, M., Jouault, F., Teodorov, C., Dhaussy, P.: Unified LTL verification and embedded execution of UML models. In: Proceedings of the 21th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems (MoDELS 2018), pp. 112\u2013122. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3239372.3239395","DOI":"10.1145\/3239372.3239395"},{"key":"30_CR11","unstructured":"Bhaduri, P., Ramesh, S.: Model Checking of Statechart Models: Survey and Research Directions. CoRR cs.SE\/0407038 (2004). \nhttp:\/\/arxiv.org\/abs\/cs.SE\/0407038"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-69489-2_39","volume-title":"Models in Software Engineering","author":"M Broy","year":"2007","unstructured":"Broy, M., Crane, M.L., Dingel, J., Hartman, A., Rumpe, B., Selic, B.: 2$$^{nd}$$ UML 2 semantics symposium: formal semantics for UML. In: K\u00fchne, T. (ed.) MODELS 2006. LNCS, vol. 4364, pp. 318\u2013323. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69489-2_39"},{"key":"30_CR13","unstructured":"Bui, N.L.: An analysis of the benefits of EULYNX-style requirements modeling for ProRail. Ph.D. thesis, Technische Universiteit Eindhoven (2017). \nhttps:\/\/research.tue.nl\/files\/91220589\/2017_09_28_ST_Bui_L.pdf"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-58298-2_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Butler","year":"2020","unstructured":"Butler, M., et al.: The first twenty-five years of industrial use of the B-method. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 189\u2013209. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-58298-2_8"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-51738-4_3","volume-title":"Cyber Physical Systems. Design, Modeling, and Evaluation","author":"G Caltais","year":"2017","unstructured":"Caltais, G., Leitner-Fischer, F., Leue, S., Weiser, J.: SysML to NuSMV model transformation via object-orientation. In: Berger, C., Mousavi, M.R., Wisniewski, R. (eds.) CyPhy 2016. LNCS, vol. 10107, pp. 31\u201345. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-51738-4_3"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-540-24732-6_17","volume-title":"Model Checking Software","author":"J Chen","year":"2004","unstructured":"Chen, J., Cui, H.: Translation from adapted UML to Promela for CORBA-based applications. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 234\u2013251. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24732-6_17"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-16561-0_18","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"N Coste","year":"2010","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 128\u2013142. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16561-0_18"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11557432_8","volume-title":"Model Driven Engineering Languages and Systems","author":"ML Crane","year":"2005","unstructured":"Crane, M.L., Dingel, J.: UML vs. classical vs. Rhapsody statecharts: not all models are created equal. In: Briand, L., Williams, C. (eds.) MODELS 2005. LNCS, vol. 3713, pp. 97\u2013112. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11557432_8"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36742-7_15"},{"key":"30_CR21","unstructured":"European Committee for Electrotechnical Standardization: CENELEC EN 50128 \u2013 Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems, June 2011. \nhttps:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-05032-4_13","volume-title":"Software Engineering and Formal Methods","author":"A Fantechi","year":"2014","unstructured":"Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167\u2013183. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-05032-4_13"},{"key":"30_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-47169-3_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"A Fantechi","year":"2016","unstructured":"Fantechi, A., Ferrari, A., Gnesi, S.: Formal methods and safety certification: challenges in the railways domain. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 261\u2013265. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47169-3_18"},{"key":"30_CR24","doi-asserted-by":"publisher","unstructured":"Fantechi, A., Fokkink, W., Morzenti, A.: Some trends in formal methods applications to railway signaling. In: Gnesi, S., Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications, chap. 4, pp. 61\u201384. Wiley (2013). \nhttps:\/\/doi.org\/10.1002\/9781118459898.ch4","DOI":"10.1002\/9781118459898.ch4"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11576280_5","volume-title":"Formal Methods and Software Engineering","author":"H Fecher","year":"2005","unstructured":"Fecher, H., Sch\u00f6nborn, J., Kyas, M., de Roever, W.-P.: 29 new unclarities in the semantics of UML 2.0 state machines. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 52\u201365. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11576280_5"},{"key":"30_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-030-18744-6_15","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"A Ferrari","year":"2019","unstructured":"Ferrari, A., et al.: Survey on formal methods and tools in railways: the ASTRail approach. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 226\u2013241. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-18744-6_15"},{"issue":"3","key":"30_CR27","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1109\/MS.2013.44","volume":"30","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Fantechi, A., Gnesi, S., Magnani, G.: Model-based development and formal methods in the railway industry. IEEE Softw. 30(3), 28\u201334 (2013). \nhttps:\/\/doi.org\/10.1109\/MS.2013.44","journal-title":"IEEE Softw."},{"key":"30_CR28","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the 42nd International Conference on Software Engineering (ICSE), pp. 62\u201374. ACM (2020). \nhttps:\/\/doi.org\/10.1145\/3377811.3380373","DOI":"10.1145\/3377811.3380373"},{"key":"30_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2020","unstructured":"Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 3\u201369. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-58298-2_1"},{"key":"30_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-68270-9_1","volume-title":"ModelEd, TestEd, TrustEd","author":"H Garavel","year":"2017","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3\u201326. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-68270-9_1"},{"issue":"2","key":"30_CR31","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10009-015-0377-y","volume":"18","author":"T Gibson-Robinson","year":"2016","unstructured":"Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149\u2013167 (2016). \nhttps:\/\/doi.org\/10.1007\/s10009-015-0377-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"30_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-32759-9_25","volume-title":"FM 2012: Formal Methods","author":"O Grumberg","year":"2012","unstructured":"Grumberg, O., Meller, Y., Yorav, K.: Applying software model checking techniques for behavioral UML models. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 277\u2013292. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32759-9_25"},{"key":"30_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-25271-6_12","volume-title":"Formal Methods for Components and Objects","author":"H Hvid Hansen","year":"2011","unstructured":"Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J., dos Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 225\u2013250. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-25271-6_12"},{"key":"30_CR34","unstructured":"Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dynamic and hierarchical UML state machines. In: Proceedings of the 3rd International Workshop on Model Development, Validation and Verification (MoDeVa 2006), pp. 94\u2013110. University of Queensland (2006)"},{"key":"30_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395\u2013414. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45739-9_23"},{"key":"30_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-030-45237-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Lang","year":"2020","unstructured":"Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. TACAS 2020. LNCS, vol. 12079, pp. 57\u201376. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-45237-7_4"},{"key":"30_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-38613-8_23","volume-title":"Integrated Formal Methods","author":"S Liu","year":"2013","unstructured":"Liu, S., et al.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 331\u2013346. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38613-8_23"},{"key":"30_CR38","unstructured":"L\u00f6fving, C., Bor\u00e4lv, A: X2Rail-2 Deliverable D5.1, Formal Methods (Taxonomy and Survey), Proposed Methods and Applications, May 2018. \nhttps:\/\/projects.shift2rail.org\/download.aspx?id=b4cf6a3d-f1f2-4dd3-ae01-2bada34596b8"},{"issue":"3","key":"30_CR39","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-018-0488-3","volume":"20","author":"F Mazzanti","year":"2018","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transf. 20(3), 263\u2013288 (2018). \nhttps:\/\/doi.org\/10.1007\/s10009-018-0488-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"30_CR40","unstructured":"ModelDriven: The fUML Reference Implementation. \nhttps:\/\/github.com\/ModelDriven\/fUML-Reference-Implementation\/blob\/master\/README.md"},{"key":"30_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-540-24732-6_9","volume-title":"Model Checking Software","author":"I Ober","year":"2004","unstructured":"Ober, I., Graf, S., Ober, I.: Validation of UML models via a mapping to communicating extended timed automata. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 127\u2013145. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24732-6_9"},{"key":"30_CR42","unstructured":"Object Management Group: Unified Modelling Language, December 2017. \nhttps:\/\/www.omg.org\/spec\/UML\/About-UML\/"},{"key":"30_CR43","unstructured":"Object Management Group: Precise Semantics of UML Composite Structure (PSCS), March 2018. \nhttps:\/\/www.omg.org\/spec\/PSCS\/1.1\/PDF"},{"key":"30_CR44","unstructured":"Object Management Group: OMG Systems Modeling Language (OMG SysML), November 2019. \nhttp:\/\/www.omg.org\/spec\/SysML\/1.6\/"},{"key":"30_CR45","unstructured":"Oliveira, R., Dingel, J.: Supporting model refinement with equivalence checking in the context of model-driven engineering with UML-RT. In: Burgue\u00f1o, L., et al. (eds.) Proceedings of the 20th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2017) \u2013 Satellite Events. CEUR Workshop Proceedings, vol. 2019, pp. 307\u2013314. CEUR-WS.org (2017). \nhttp:\/\/ceur-ws.org\/Vol-2019\/modevva_2.pdf"},{"key":"30_CR46","unstructured":"OMG: Action Language for Foundational UML (Alf) \u2013 Concrete Syntax for a UML Action Language, July 2017. \nhttps:\/\/www.omg.org\/spec\/ALF\/1.1"},{"key":"30_CR47","unstructured":"OMG: Semantics of a Foundational Subset for Executable UML Models (fUML), December 2018. \nhttps:\/\/www.omg.org\/spec\/FUML\/1.4\/PDF"},{"key":"30_CR48","unstructured":"P\u00e9tin, J.F., Evrot, D., Morel, G., Lamy, P.: Combining SysML and formal methods for safety requirements verification. In: Proceedings of the 22nd International Conference on Software & Systems Engineering and their Applications (ICSSEA 2010) (2010). \nhttps:\/\/hal.archives-ouvertes.fr\/hal-00533311\/document"},{"key":"30_CR49","series-title":"Series in Engineering and Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-1-4615-5229-1_17","volume-title":"Behavioral Specifications of Businesses and Systems","author":"AJH Simons","year":"1999","unstructured":"Simons, A.J.H., Graham, I.: 30 things that go wrong in object modelling with UML 1.3. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. SECS, vol. 523, pp. 237\u2013257. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/978-1-4615-5229-1_17"},{"key":"30_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-25271-6_13","volume-title":"Formal Methods for Components and Objects","author":"C Snook","year":"2011","unstructured":"Snook, C., Savicks, V., Butler, M.: Verification of UML models by translation to UML-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 251\u2013266. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-25271-6_13"},{"key":"30_CR51","unstructured":"UNISIG: RBC-RBC Safe Communication Interface \u2013 SUBSET-098, February 2012. \nhttps:\/\/www.era.europa.eu\/sites\/default\/files\/filesystem\/ertms\/ccs_tsi_annex_a_-_mandatory_specifications\/set_of_specifications_3_etcs_b3_r2_gsm-r_b1\/index063_-_subset-098_v300.pdf"},{"key":"30_CR52","unstructured":"UNISIG: FIS for the RBC\/RBC Handover \u2013 SUBSET-039, December 2015. \nhttps:\/\/www.era.europa.eu\/sites\/default\/files\/filesystem\/ertms\/ccs_tsi_annex_a_-_mandatory_specifications\/set_of_specifications_3_etcs_b3_r2_gsm-r_b1\/index012_-_subset-039_v320.pdf"},{"key":"30_CR53","unstructured":"Visual Paradigm: What is Unified Modeling Language (UML)?. \nhttps:\/\/www.visual-paradigm.com\/guide\/uml-unified-modeling-language\/what-is-uml\/"},{"key":"30_CR54","doi-asserted-by":"publisher","unstructured":"Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), pp. 176\u2013184. IEEE (2005). \nhttps:\/\/doi.org\/10.1109\/APSEC.2005.70","DOI":"10.1109\/APSEC.2005.70"},{"key":"30_CR55","doi-asserted-by":"publisher","unstructured":"Zhang, S.J., Liu, Y.: An automatic approach to model checking UML state machines. In: Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement (SSIRI-C 2010), pp. 1\u20136. IEEE (2010). \nhttps:\/\/doi.org\/10.1109\/SSIRI-C.2010.11","DOI":"10.1109\/SSIRI-C.2010.11"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61467-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T01:09:52Z","timestamp":1603674592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61467-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030614669","9783030614676"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61467-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"27 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}