{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T16:10:45Z","timestamp":1772122245972,"version":"3.50.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2023,6]]},"DOI":"10.1007\/s10270-022-01043-8","type":"journal-article","created":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T07:03:02Z","timestamp":1667286182000},"page":"941-968","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal translation of YAWL workflow models to the Alloy formal specifications: a testing application"],"prefix":"10.1007","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1795-0996","authenticated-orcid":false,"given":"Mehran","family":"Rivadeh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Seyed-Hassan","family":"Mirian-Hosseinabadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,1]]},"reference":[{"key":"1043_CR1","unstructured":"Fowler, M.: Microservices. martinFowler.com. 25 March 2014 [Cited: 28 June 2021]. https:\/\/martinfowler.com\/articles\/microservices.html (2014)"},{"key":"1043_CR2","volume-title":"Microservice Architecture: Aligning Principles, Practices, and Culture","author":"I Nadareishvili","year":"2016","unstructured":"Nadareishvili, I., et al.: Microservice Architecture: Aligning Principles, Practices, and Culture. O\u2019Reilly Media, Sebastopol, CA (2016)"},{"key":"1043_CR3","unstructured":"Camunda Group: Zeebe. Zeebe. 5 Feb 2018 [Cited: 28 June 2021]. https:\/\/docs.zeebe.io\/introduction\/what-is-zeebe.html (2018)"},{"key":"1043_CR4","doi-asserted-by":"crossref","unstructured":"Lamancha, B.P., et al.: Model-driven test code generation. In: International Conference on Evaluation of Novel Approaches to Software Engineering, vol. 275, pp. 155\u2013168. Springer, Heraklion (2011)","DOI":"10.1007\/978-3-642-32341-6_11"},{"key":"1043_CR5","unstructured":"Clemson, T.: Testing Strategies in a microservice architecture. martinfowler. 18 Nov 2014 [Cited: 28 June 2021]. https:\/\/martinfowler.com\/articles\/microservice-testing\/ (2014)"},{"key":"1043_CR6","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2012)"},{"key":"1043_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-662-49224-6_1","volume-title":"Software Engineering and Formal Methods","author":"K Meinke","year":"2015","unstructured":"Meinke, K., Nycander, P.: Learning-based testing of distributed microservice architectures: correctness and fault injection. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) Software Engineering and Formal Methods, vol. 9509, pp. 3\u201310. Springer, Berlin (2015)"},{"key":"1043_CR8","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/j.icte.2019.02.001","volume":"5","author":"M Peuster","year":"2019","unstructured":"Peuster, M., et al.: Joint testing and profiling of microservice-based network services using TTCN-3. ICT Express 5, 150\u2013153 (2019)","journal-title":"ICT Express"},{"key":"1043_CR9","doi-asserted-by":"crossref","unstructured":"Savchenko, D., Radchenko, G., Taipale, O.: Microservices validation: Mjolnirr platform case study. In: International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), pp. 235\u2013240. IEEE, Opatija (2015)","DOI":"10.1109\/MIPRO.2015.7160271"},{"key":"1043_CR10","unstructured":"Reeve, J., Frost, M.P.,Thorpe, P.: Automated integration testing with mock microservices. 20190155721 United States of America, 23 May 2019 (2019)"},{"key":"1043_CR11","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/s10009-011-0189-7","volume":"13","author":"KC Castillos","year":"2011","unstructured":"Castillos, K.C., Dadeau, F., Julliand, J.: Scenario-based testing from UML\/OCL behavioral models application to POSIX compliance. Int. J. Softw. Tools Technol. Transfer 13, 431\u2013448 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1043_CR12","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.entcs.2008.11.004","volume":"220","author":"Y Falcone","year":"2008","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.-C.: j-POST: a java toolchain for property oriented software testing. Electron. Notes Theor. Comput. Sci. 220, 29\u201341 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1043_CR13","doi-asserted-by":"crossref","unstructured":"Castillos, K.C., et al.: A compositional automata-based semantics for property patterns. In: 10th International Conference on Integrated Formal Methods, vol. 7940, pp. 316\u2013330. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38613-8_22"},{"key":"1043_CR14","doi-asserted-by":"crossref","unstructured":"Achour, S., Benattou, M.: Test case generation for Java Bytecode programs annotated with BML specifications. In: International Conference on Multimedia Computing and Systems (ICMCS), vol. 5, pp. 605\u2013610. IEEE, Morocco (2016)","DOI":"10.1109\/ICMCS.2016.7905597"},{"key":"1043_CR15","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-17071-3_12","volume-title":"Formal Methods for Components and Objects","author":"BK Aichernig","year":"2009","unstructured":"Aichernig, B.K., et al.: Model-based mutation testing of hybrid systems. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) Formal Methods for Components and Objects, vol. 6286, pp. 228\u2013249. Springer, Berlin (2009)"},{"key":"1043_CR16","doi-asserted-by":"crossref","unstructured":"Yamasathien, S., Vatanawood, W.: An approach to construct formal model of business process model from BPMN workflow patterns. In: IEEE, 2014. Fourth International Conference on Digital Information and Communication Technology and its Applications (DICTAP), Bangkok, pp. 211\u2013215 (2014)","DOI":"10.1109\/DICTAP.2014.6821684"},{"key":"1043_CR17","doi-asserted-by":"crossref","unstructured":"Prandi, D., Quaglia, P., Zannone, N.: Formal analysis of BPMN via a translation into COWS. In: 10th International Conference on Coordination Models and Languages, pp. 249\u2013263. Springer, Oslo (2008)","DOI":"10.1007\/978-3-540-68265-3_16"},{"key":"1043_CR18","doi-asserted-by":"publisher","first-page":"42","DOI":"10.4018\/jwsr.2008010103","volume":"5","author":"C Ouyang","year":"2008","unstructured":"Ouyang, C., et al.: Pattern-based translation of BPMN process models to BPEL web services. Int. J. Web Serv. Res. (IJWSR) 5, 42\u201362 (2008)","journal-title":"Int. J. Web Serv. Res. (IJWSR)"},{"key":"1043_CR19","doi-asserted-by":"crossref","unstructured":"Decker, G., et al.: Transforming BPMN Diagrams into YAWL Nets. In: International Conference on Business Process Management, vol. 5240, pp. 386\u2013389. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85758-7_30"},{"key":"1043_CR20","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1016\/j.jvlc.2007.07.004","volume":"18","author":"C Zhao","year":"2007","unstructured":"Zhao, C., et al.: Pattern-based design evolution using graph transformation. J. Vis. Lang. Comput. 18, 378\u2013398 (2007)","journal-title":"J. Vis. Lang. Comput."},{"key":"1043_CR21","doi-asserted-by":"crossref","unstructured":"Ye, J., et al.: Formal semantics of BPMN process models using YAWL. In: Second International Symposium on Intelligent Information Technology Application, pp. 70\u201374. IEEE, Shanghai (2008)","DOI":"10.1109\/IITA.2008.68"},{"key":"1043_CR22","doi-asserted-by":"crossref","unstructured":"Mendling, J., et al.: Errors in the SAP reference model. In: International Conference on Business Process Management, pp. 451\u2013457. Springer, Berlin (2006)","DOI":"10.1007\/11841760_38"},{"key":"1043_CR23","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1108\/14637150910931479","volume":"15","author":"MT Wynn","year":"2009","unstructured":"Wynn, M.T., et al.: Business process verification: finally a reality! Bus. Process. Manag. J. 15, 74\u201392 (2009)","journal-title":"Bus. Process. Manag. J."},{"key":"1043_CR24","volume-title":"Testing Java Microservices Using Arquillian, Hoverfly, AssertJ, JUnit, Selenium, and Mockito","author":"AS Bueno","year":"2018","unstructured":"Bueno, A.S., Gumbrecht, A., Porter, J.: Testing Java Microservices Using Arquillian, Hoverfly, AssertJ, JUnit, Selenium, and Mockito, vol. 1. Manning Publication, New York (2018)"},{"key":"1043_CR25","doi-asserted-by":"crossref","unstructured":"Yuan, E.: Architecture interoperability and repeatability with microservices: an industry perspective. In: 2nd International Workshop on Establishing a Community-Wide Infrastructure for Architecture-Based Software Engineering, pp. 26\u201333. IEEE\/ACM, Montreal (2019)","DOI":"10.1109\/ECASE.2019.00013"},{"key":"1043_CR26","first-page":"1","volume-title":"Transactions on Petri Nets and Other Models of Concurrency","author":"WMP van der Aalst","year":"2009","unstructured":"van der Aalst, W.M.P.: Process-aware information systems: lessons to be learned from process mining. In: Jensen, K., van der Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency, pp. 1\u201326. Springer, Berlin (2009)"},{"key":"1043_CR27","unstructured":"Russell, N., et al.: Workflow control-flow patterns: a revised view. BPM Center Report, vol. 0622, pp. 6\u201322. s.n., Netherland (2006)"},{"key":"1043_CR28","unstructured":"Object Management Group: BPMN. OMG [Cited: 28 June 2021]. https:\/\/www.omg.org\/spec\/BPMN\/2.0\/About-BPMN\/"},{"key":"1043_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03121-2","volume-title":"Modern Business Process Automation: YAWL and Its Support Environment","author":"A ter Hofstede","year":"2010","unstructured":"ter Hofstede, A., et al.: Modern Business Process Automation: YAWL and Its Support Environment. Springer, New York (2010)"},{"key":"1043_CR30","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1093\/comjnl\/44.4.246","volume":"44","author":"E Verbeek","year":"2001","unstructured":"Verbeek, E., Basten, T., van der Aalst, W.: diagnosing workflow processes using Woflan. Comput. J. 44, 246\u2013279 (2001)","journal-title":"Comput. J."},{"key":"1043_CR31","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2017","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, New York (2017)"},{"key":"1043_CR32","first-page":"30","volume-title":"Testing for Continuous Delivery with Visual Studio 2012","author":"L Brader","year":"2013","unstructured":"Brader, L., Hilliker, H., Wills, A.: Chapter 2. Unit testing: testing the inside. In: Brader, L., Hilliker, H., Hilliker, H.F., Wills, A.C. (eds.) Testing for Continuous Delivery with Visual Studio 2012, p. 30. Microsoft, Redmond, Washington (2013)"},{"key":"1043_CR33","volume-title":"Model-Based Testing Essentials\u2014Guide to the ISTQB Certified Model-Based Tester","author":"G Bazzana","year":"2016","unstructured":"Bazzana, G., et al.: Model-Based Testing Essentials\u2014Guide to the ISTQB Certified Model-Based Tester. John Wiley & Sons, Hoboken (2016).. (ISBN: 9781119130017)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01043-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-01043-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01043-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T04:27:04Z","timestamp":1685507224000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-01043-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,1]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["1043"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-01043-8","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,1]]},"assertion":[{"value":"28 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 August 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 November 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}