{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T09:51:30Z","timestamp":1790502690055,"version":"4.1.0"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s10009-019-00542-2","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T09:46:36Z","timestamp":1570700796000},"page":"349-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Modeling the hybrid ERTMS\/ETCS level 3 standard using a formal requirements engineering approach"],"prefix":"10.1007","volume":"22","author":[{"given":"Steve Jeffrey","family":"Tueno Fotso","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"Frappier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amel","family":"Mammar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"542_CR1","volume-title":"The B-book\u2013Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-book\u2013Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"542_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B\u2013System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B\u2013System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"542_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.: The ABZ-2018 case study with Event-B. In: Butler et\u00a0al. [11], pp. 322\u2013337","DOI":"10.1007\/978-3-319-91271-4_22"},{"key":"542_CR4","unstructured":"ANR-14-CE28-0009: Formose ANR project (2017)"},{"key":"542_CR5","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Jezek, P., Kofron, J.: Modelling the hybrid ERTMS\/ETCS level 3 case study in Spin. In: Butler et\u00a0al. [11], pp. 277\u2013291","DOI":"10.1007\/978-3-319-91271-4_19"},{"key":"542_CR6","doi-asserted-by":"publisher","unstructured":"Arora, C., Sabetzadeh, M., Briand, L.C.: An empirical study on the potential usefulness of domain models for completeness checking of requirements. Empir. Softw. Eng. 24(4), 2509\u20132539. \nhttps:\/\/doi.org\/10.1007\/s10664-019-09693-x","DOI":"10.1007\/s10664-019-09693-x"},{"key":"542_CR7","doi-asserted-by":"publisher","unstructured":"Bjrner, D.: Domain analysis and description principles, techniques, and modelling languages. ACM Trans. Softw. Eng. Methodol. 28(2), 8:1\u20138:67 (2019). \nhttps:\/\/doi.org\/10.1145\/3295738","DOI":"10.1145\/3295738"},{"key":"542_CR8","doi-asserted-by":"crossref","unstructured":"Broy, M.: Domain modeling and domain engineering: key tasks in requirements engineering. In: M\u00fcnch, J., Schmid, K. (eds.) Perspectives on the Future of Software Engineering. Essays in Honor of Dieter Rombach, pp. 15\u201330. Springer. Berlin (2013)","DOI":"10.1007\/978-3-642-37395-4_2"},{"key":"542_CR9","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3\u20137, 2018, pp. 884\u2013887. ACM (2018)"},{"key":"542_CR10","doi-asserted-by":"crossref","unstructured":"Butler, M.J., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 4157. Springer, Berlin (2006)","DOI":"10.1007\/11916246"},{"key":"542_CR11","doi-asserted-by":"crossref","unstructured":"Butler, M.J., Raschke, A., Hoang, T.S., Reichl, K. (eds.): Abstract State Machines, Alloy, B, TLA, VDM, and Z\u20136th International Conference, ABZ 2018, Southampton, UK, June 5\u20138, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10817. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4"},{"key":"542_CR12","unstructured":"Clancy, T.: The standish group CHAOS report. Project Smart pp. 8\u20139 (2014)"},{"key":"542_CR13","unstructured":"ClearSy: Atelier B: B System (2014). \nhttp:\/\/clearsy.com\/\n\n. Accessed Oct 2019"},{"key":"542_CR14","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N.: Validating the hybrid ERTMS\/ETCS level 3 concept with electrum. In: Butler et\u00a0al. [11], pp. 307\u2013321","DOI":"10.1007\/978-3-319-91271-4_21"},{"key":"542_CR15","unstructured":"Deploy Project: Rodin Atelier B Provers Plug-in (2017). \nhttps:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/atelier_b_provers.html\n\n. Accessed Oct 2019"},{"key":"542_CR16","doi-asserted-by":"crossref","unstructured":"Dghaym, D., Poppleton, M., Snook, C.F.: Diagram-led formal modelling using iUML-B for hybrid ERTMS level 3. In: Butler et\u00a0al. [11], pp. 338\u2013352","DOI":"10.1007\/978-3-319-91271-4_23"},{"key":"542_CR17","doi-asserted-by":"publisher","unstructured":"de Almeida Falbo, R., Guizzardi, G., Duarte, K.C.: An ontological approach to domain engineering. In: Proceedings of the 14th International Conference on Software Engineering and Knowledge Engineering, SEKE 2002, Ischia, Italy, July 15\u201319, 2002. pp. 351\u2013358. ACM (2002). \nhttps:\/\/doi.org\/10.1145\/568760.568822","DOI":"10.1145\/568760.568822"},{"key":"542_CR18","unstructured":"EEIG ERTMS Users Group: Hybrid ERTMS\/ETCS level 3: Principles. Ref. 16E042 Version 1C (2018)"},{"key":"542_CR19","unstructured":"Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS\/ETCS level 3 standard using a formal requirements engineering approach. In: Butler et\u00a0al. [11], pp. 262\u2013276"},{"key":"542_CR20","unstructured":"Fotso, S.J.T., Mammar, A., Laleau, R., Frappier, M.: Event-B expression and verification of translation rules between SysML\/KAOS domain models and B System specifications. In: Butler et\u00a0al. [11], pp. 55\u201370"},{"key":"542_CR21","doi-asserted-by":"publisher","unstructured":"Hacid, K., Ameur, Y.A.: Strengthening MDE and formal design models by references to domain ontologies. A model annotation based approach. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques\u20147th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10\u201314, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9952, pp. 340\u2013357 (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47166-2_24","DOI":"10.1007\/978-3-319-47166-2_24"},{"key":"542_CR22","doi-asserted-by":"crossref","unstructured":"Hansen, D., Leuschel, M., Schneider, D., Krings, S., K\u00f6rner, 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: Butler et\u00a0al. [11], pp. 292\u2013306","DOI":"10.1007\/978-3-319-91271-4_20"},{"key":"542_CR23","unstructured":"Hause, M., et\u00a0al.: The SysML modelling language. In: Fifteenth European Systems Engineering Conference. vol. 9. Citeseer (2006)"},{"key":"542_CR24","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Butler, M.J., Reichl, K.: The hybrid ERTMS\/ETCS level 3 case study. In: Butler et\u00a0al. [11], pp. 251\u2013261","DOI":"10.1007\/978-3-319-91271-4_17"},{"key":"542_CR25","volume-title":"The SPIN Model Checker-Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker-Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"542_CR26","unstructured":"Jackson, D.: Software Abstractions\u2014Logic, Language, and Analysis. MIT Press (2006). \nhttp:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=10928\n\n. Accessed Oct 2019"},{"key":"542_CR27","volume-title":"Software Requirements and Specifications\u2013A Lexicon of Practice","author":"MA Jackson","year":"1995","unstructured":"Jackson, M.A.: Software Requirements and Specifications\u2013A Lexicon of Practice. Principles and Prejudices. Addison-Wesley, Boston (1995)"},{"key":"542_CR28","unstructured":"Jetbrains: Jetbrains mps (2017). \nhttps:\/\/www.jetbrains.com\/mps\/"},{"issue":"1\u20132","key":"542_CR29","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s11334-009-0119-y","volume":"6","author":"R Laleau","year":"2010","unstructured":"Laleau, R., Semmak, F., Matoussi, A., Petit, D., Hammad, A., Tatibouet, B.: A first attempt to combine SysML requirements diagrams and B. Innov. Syst. Softw. Eng. 6(1\u20132), 47\u201354 (2010)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"542_CR30","doi-asserted-by":"crossref","unstructured":"Lecomte, T., D\u00e9harbe, D., Prun, \u00c9., Mottin, E.: Applying a formal method in industry: a 25-year trajectory. In: Formal Methods: Foundations and Applications\u201420th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29\u2013December 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10623, pp. 70\u201387. Springer (2017)","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"542_CR31","first-page":"732","volume-title":"Axiomatic design and fabrication of composite structures-applications in robots, machine tools, and automobiles","author":"DG Lee","year":"2005","unstructured":"Lee, D.G., Suh, N.P.: Axiomatic design and fabrication of composite structures-applications in robots, machine tools, and automobiles, p. 732. Oxford University Press, Oxford (2005)"},{"key":"542_CR32","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.J.: Prob: A Model Checker for B. Lecture Notes in Computer Science, vol. 2805, pp. 855\u2013874. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"542_CR33","doi-asserted-by":"crossref","unstructured":"Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: An Event-B model of the hybrid ERTMS\/ETCS level 3 standard. In: Butler et\u00a0al. [11], pp. 353\u2013366","DOI":"10.1007\/978-3-319-91271-4_24"},{"key":"542_CR34","doi-asserted-by":"crossref","unstructured":"Mammar, A., Laleau, R.: On the use of domain and system knowledge modeling in goal-based Event-B specifications. In: ISoLA 2016, Lecture Notes in Computer Science. pp. 325\u2013339. Springer","DOI":"10.1007\/978-3-319-47166-2_23"},{"key":"542_CR35","doi-asserted-by":"crossref","unstructured":"Matoussi, A., Gervais, F., Laleau, R.: A goal-based approach to guide the design of an abstract Event-B specification. In: Perseil, I., Breitman, K.K., Sterritt, R. (eds.) 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27\u201329 April 2011. pp. 139\u2013148","DOI":"10.1109\/ICECCS.2011.21"},{"issue":"1","key":"542_CR36","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1002\/j.2334-5837.2018.00484.x","volume":"28","author":"P Micouin","year":"2018","unstructured":"Micouin, P., Fabre, L., Becquet, R., Paper, P., Razafimahefa, T., Gu\u00e9rin, F.: Property model methodology: a landing gear operational use case. INCOSE Int. Symp. 28(1), 321\u2013336 (2018). \nhttps:\/\/doi.org\/10.1002\/j.2334-5837.2018.00484.x","journal-title":"INCOSE Int. Symp."},{"key":"542_CR37","first-page":"2","volume":"232","author":"F Nicola","year":"2017","unstructured":"Nicola, F., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS level 3: the game-changer. IRSE News View 232, 2\u20139 (2017)","journal-title":"IRSE News View"},{"issue":"3","key":"542_CR38","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/2.910904","volume":"34","author":"B Nuseibeh","year":"2001","unstructured":"Nuseibeh, B.: Weaving together requirements and architectures. Computer 34(3), 115\u2013119 (2001)","journal-title":"Computer"},{"key":"542_CR39","unstructured":"Openflexo: Openflexo project (2019). \nhttp:\/\/www.openflexo.org\n\n. Accessed Oct 2019"},{"key":"542_CR40","unstructured":"Openflexo: Openflexo sysml\/kaos tool (2019). \nhttps:\/\/downloads.openflexo.org\/Formose\/\n\n. Accessed Oct 2019"},{"key":"542_CR41","doi-asserted-by":"crossref","unstructured":"Pierra, G.: The PLIB ontology-based approach to data integration. In: IFIP 18th World Computer Congress. IFIP, vol. 156, pp. 13\u201318. Kluwer\/Springer (2004)","DOI":"10.1007\/978-1-4020-8157-6_2"},{"key":"542_CR42","unstructured":"Roques, A.: PlantUML: open-source tool that uses simple textual descriptions to draw UML diagrams. \nhttp:\/\/plantuml.sourceforge.net\/index.html\n\n (2015). Accessed Oct 2019"},{"key":"542_CR43","volume-title":"Encyclopedia of Database Systems","author":"S Bechhofer","year":"2018","unstructured":"Bechhofer, S.: Web ontology language (OWL). In: Liu, L., \u00d6zsu, M.T. (eds.) Encyclopedia of Database Systems, 2nd edn. Springer, New York (2018)","edition":"2"},{"issue":"1","key":"542_CR44","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"CF Snook","year":"2006","unstructured":"Snook, C.F., Butler, M.J.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"542_CR45","unstructured":"SYSTEREL: Rodin SMT Solvers Plug-in (2017). \nhttp:\/\/wiki.event-b.org\/index.php\/SMT_Solvers_Plug-in\n\n. Accessed Oct 2019"},{"key":"542_CR46","unstructured":"SysML\/KAOS requirements modeling of a road transportation system (2018) \nhttps:\/\/github.com\/stuenofotso\/SysML_KAOS_Domain_Model_Parser\/tree\/master\/Bonaventure_project"},{"key":"542_CR47","unstructured":"Tueno, S., Frappier, M., Laleau, R., Mammar, A., Barradas, H.R.: The Generic SysML\/KAOS Domain Metamodel. ArXiv e-prints, cs.SE (2018). \narXiv:1811.04732"},{"key":"542_CR48","unstructured":"Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Towards using ontologies for domain modeling within the SysML\/KAOS approach. In: IEEE Proceedings of MoDRE Workshop, 25th IEEE International Requirements Engineering Conference"},{"key":"542_CR49","unstructured":"Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML\/KAOS Domain Modeling Approach. ArXiv e-prints, cs.SE (2017). \narXiv:1710.00903"},{"key":"542_CR50","unstructured":"Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML\/KAOS Domain Modeling Language (Tool and Case Studies) (2017). \nhttps:\/\/github.com\/stuenofotso\/SysML_KAOS_Domain_Model_Parser\/tree\/master\n\n. Accessed Oct 2019"},{"key":"542_CR51","unstructured":"Tueno, S., Laleau, R., Mammar, A., Frappier, M.: SysML\/KAOS Approach on the Hybrid ERTMS\/ETCS Level 3 case study (2018). \nhttps:\/\/github.com\/stuenofotso\/SysML_KAOS_Domain_Model_Parser\/tree\/master\/ABZ18_ERTMS\n\n. Accessed Oct 2019"},{"key":"542_CR52","unstructured":"Tueno, S., Laleau, R., Mammar, A., Frappier, M.: SysML\/KAOS Domain Modeling Tool (2018). \nhttps:\/\/github.com\/stuenofotso\/SysML_KAOS_Domain_Model_Parser\n\n. Accessed Oct 2019"},{"key":"542_CR53","volume-title":"Requirements Engineering-From System Goals to UML Models to Software Specifications","author":"A van Lamsweerde","year":"2009","unstructured":"van Lamsweerde, A.: Requirements Engineering-From System Goals to UML Models to Software Specifications. Wiley, Hoboken (2009)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00542-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00542-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00542-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,8]],"date-time":"2020-10-08T19:23:27Z","timestamp":1602185007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00542-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["542"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00542-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"10 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}