{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:37:00Z","timestamp":1742931420511,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030672195"},{"type":"electronic","value":"9783030672201"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-67220-1_1","type":"book-chapter","created":{"date-parts":[[2021,1,16]],"date-time":"2021-01-16T08:03:07Z","timestamp":1610784187000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model Translation from Papyrus-RT into the nuXmv Model Checker"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-6153","authenticated-orcid":false,"given":"Sneha","family":"Sahu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruth","family":"Schorr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7543-2671","authenticated-orcid":false,"given":"Inmaculada","family":"Medina-Bulo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8702-9257","authenticated-orcid":false,"given":"Matthias","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,17]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"1_CR2","unstructured":"Beaton, W.: Eclipse Papyrus for Real Time (Papyrus-RT). projects.eclipse.org, July 2017. https:\/\/www.eclipse.org\/papyrus-rt\/. Accessed 31 Aug 2020"},{"key":"1_CR3","unstructured":"Bozzano, M., et al.: nuXmv 1.1. 1 User Manual. FBK-Via Sommarive 18, 38055 (2016). https:\/\/es-static.fbk.eu\/tools\/nuxmv\/index.php?n=Documentation.Home. Accessed 31 Aug 2020"},{"key":"1_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0091-5","volume-title":"Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement","author":"M Broy","year":"2012","unstructured":"Broy, M., St\u00f8len, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4613-0091-5"},{"key":"1_CR5","unstructured":"Carlsson, M.G., Johansson, L.G.: Formal verification of UML-RT capsules using model checking. Master\u2019s thesis, Chalmers University of Technology (2009)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"1_CR7","unstructured":"Cavada, R., Cimatti, A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M.: NuSMV 2.6 Tutorial. FBK-irst-Via Sommarive 18, 38055 (2010)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"1_CR9","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: Othello Contracts Refinement Analysis Versions 1, 3 (2015)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-61474-5_93","volume-title":"Computer Aided Verification","author":"E Clarke","year":"1996","unstructured":"Clarke, E., McMillan, K., Campos, S., Hartonas-Garmhausen, V.: Symbolic model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 419\u2013422. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_93"},{"key":"1_CR11","unstructured":"Favre, J.M.: Towards a basic theory to model model driven engineering. In: 3rd Workshop in Software Model Engineering, WiSME, pp. 262\u2013271. Citeseer (2004)"},{"key":"1_CR12","unstructured":"Hili, N., Posse, E., Dingel, U., Beaulieu, A.: Supporting Material For EclipseCon\u201917 Unconference - Modeling & Analysis In Software Engineering. School of Computing, Queen\u2019s University (2017). https:\/\/flux.cs.queensu.ca\/mase\/papyrus-rt-resources\/supporting-material-for-eclipsecon17-unconference\/. Accessed May 2020"},{"key":"1_CR13","unstructured":"Hili, N., Posse, E., Dingel, J.: Calur: an action language for UML-RT. In: 9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Toulouse, France, January 2018. https:\/\/hal.archives-ouvertes.fr\/hal-01739675"},{"issue":"5","key":"1_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR15","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, vol. 1003. Addison-Wesley, Reading (2004)"},{"key":"1_CR16","unstructured":"IBM Knowledge Center: IBM Rational Software Architect RealTime Edition. https:\/\/www.ibm.com\/support\/knowledgecenter\/SS5JSH_9.5.0\/com.ibm.xtools.rsarte.legal.doc\/helpindex_rsarte.html. Accessed July 2020"},{"key":"1_CR17","unstructured":"Kanav, S., Aravantinos, V.: Modular transformation from AF3 to nuXmv. In: MODELS (Satellite Events), pp. 300\u2013306 (2017)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Koshy, T.: Finite-State-Machines. In: Discrete Mathematics with Applications, pp. 771\u2013802. Elsevier (2004)","DOI":"10.1016\/B978-012421180-3\/50008-5"},{"issue":"6","key":"1_CR19","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects Comput. 11(6), 637\u2013664 (1999)","journal-title":"Formal Aspects Comput."},{"key":"1_CR20","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). https:\/\/doi.org\/10.1007\/978-3-642-38613-8_23"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: The SMV system. In: Symbolic Model Checking, pp. 61\u201385. Springer, Boston (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6_4","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"1_CR22","unstructured":"Posse, E.: PapyrusRT: modelling and code generation. In: Workshop on Open Source for Model Driven Engineering (OSS4MDE 2015) (2015)"},{"issue":"1","key":"1_CR23","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10270-014-0399-z","volume":"15","author":"E Posse","year":"2016","unstructured":"Posse, E., Dingel, J.: An executable formal semantics for UML-RT. Softw. Syst. Model. 15(1), 179\u2013217 (2016)","journal-title":"Softw. Syst. Model."},{"key":"1_CR24","unstructured":"Posse, E., Rivet, C.: Papyrus-RT: high-level view of the general transformation architecture. Survey of Requirements Management Standards - Eclipsepedia, February 2017. http:\/\/wiki.eclipse.org\/Papyrus-RT\/Developer\/Design\/0.8\/Codegen_High_Level_Overview. Accessed 24 Apr 2019"},{"key":"1_CR25","unstructured":"Rivet, C., Posse, E., Toolan, D.: Getting Started with Papyrus for Real Time v1.0. Survey of Requirements Management Standards - Eclipsepedia, September 2017. https:\/\/wiki.eclipse.org\/Papyrus-RT\/User\/User_Guide\/Getting_Started. Accessed 24 Apr 2019"},{"key":"1_CR26","unstructured":"Sommerville, I.: An Insulin Pump Control System. Software Engineering 10th Edition, December 2014"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Zurowska, K., Dingel, J.: Symbolic execution of UML-RT state machines. In: Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC 2012, pp. 1292\u20131299. Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2245276.2231981","DOI":"10.1145\/2245276.2231981"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67220-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,11]],"date-time":"2022-12-11T22:27:04Z","timestamp":1670797624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-67220-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030672195","9783030672201"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67220-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"17 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","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":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}