{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:56:53Z","timestamp":1725796613212},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319091945"},{"type":"electronic","value":"9783319091952"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09195-2_6","type":"book-chapter","created":{"date-parts":[[2014,7,9]],"date-time":"2014-07-09T09:30:06Z","timestamp":1404898206000},"page":"83-100","source":"Crossref","is-referenced-by-count":2,"title":["Alloy4SPV : A Formal Framework for Software Process Verification"],"prefix":"10.1007","author":[{"given":"Yoann","family":"Laurent","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Reda","family":"Bendraou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Souheib","family":"Baarir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Marie-Pierre","family":"Gervais","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Jackson, D.: Software Abstractions: Logic, language and analysis. Mit Pr. (2011)"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1125808.1125809","volume":"15","author":"R. Eshuis","year":"2006","unstructured":"Eshuis, R.: Symbolic model checking of uml activity diagrams. TOSEM\u00a015(1), 1\u201338 (2006)","journal-title":"TOSEM"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-77351-1_5","volume-title":"Software Composition","author":"P.Y.H. Wong","year":"2007","unstructured":"Wong, P.Y.H., Gibbons, J.: A process-algebraic approach to workflow specification and refinement. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol.\u00a04829, pp. 51\u201365. Springer, Heidelberg (2007)"},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1147\/sj.462.0335","volume":"46","author":"Y. Liu","year":"2007","unstructured":"Liu, Y., Muller, S., Xu, K.: A static compliance-checking framework for business process models. IBM Systems Journal\u00a046(2), 335\u2013361 (2007)","journal-title":"IBM Systems Journal"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-02144-2_34","volume-title":"Advanced Information Systems Engineering","author":"N. Tr\u010dka","year":"2009","unstructured":"Tr\u010dka, N., van der Aalst, W.M.P., Sidorova, N.: Data-flow anti-patterns: Discovering data-flow errors in workflows. In: van Eck, P., Gordijn, J., Wieringa, R. (eds.) CAiSE 2009. LNCS, vol.\u00a05565, pp. 425\u2013439. Springer, Heidelberg (2009)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-03848-8_19","volume-title":"Business Process Management","author":"D. Fahland","year":"2009","unstructured":"Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., V\u00f6lzer, H., Wolf, K.: Instantaneous soundness checking of industrial business process models. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol.\u00a05701, pp. 278\u2013293. Springer, Heidelberg (2009)"},{"issue":"3","key":"6_CR7","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s00165-010-0161-4","volume":"23","author":"W. Aalst van der","year":"2011","unstructured":"van der Aalst, W., Van Hee, K., ter Hofstede, A., Sidorova, N., Verbeek, H., Voorhoeve, M., Wynn, M.: Soundness of workflow nets: Classification, decidability, and analysis. Formal Aspects of Computing\u00a023(3), 333\u2013363 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Guelfi, N., Mammar, A.: A formal semantics of timed activity diagrams and its promela translation. In: IEEE 12th Asia-Pacific Software Engineering Conference, APSEC 2005, p. 8 (2005)","DOI":"10.1109\/APSEC.2005.7"},{"issue":"01","key":"6_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"W.M. Aalst van der","year":"1998","unstructured":"van der Aalst, W.M.: The application of petri nets to workflow management. Journal of Circuits, Systems, and Computers\u00a08(01), 21\u201366 (1998)","journal-title":"Journal of Circuits, Systems, and Computers"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Jung, H.T., Joo, S.H.: Transformation of an activity model into a colored petri net model. In: IEEE TISC, pp. 32\u201337 (2010)","DOI":"10.1109\/TISC.2010.5714602"},{"key":"6_CR11","unstructured":"Ter Hofstede, A.: Workflow patterns: On the expressive power of (petri-net-based) workflow languages. In: of DAIMI, University of Aarhus, Citeseer (2002)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/11568322_5","volume-title":"Conceptual Modeling \u2013 ER 2005","author":"P. Wohed","year":"2005","unstructured":"Wohed, P., van der Aalst, W.M.P., Dumas, M., ter Hofstede, A.H.M., Russell, N.: Pattern-based analysis of the control-flow perspective of uml activity diagrams. In: Delcambre, L.M.L., Kop, C., Mayr, H.C., Mylopoulos, J., Pastor, \u00d3. (eds.) ER 2005. LNCS, vol.\u00a03716, pp. 63\u201378. Springer, Heidelberg (2005)"},{"key":"6_CR13","unstructured":"Cunha, A.: Bounded model checking of temporal formulas with alloy. arXiv preprint arXiv:1207.2746 (2012)"},{"key":"6_CR14","unstructured":"OMG: Semantics of a foundational subset for executable uml models (fuml) version 1.0 (2011), \n                    \n                      http:\/\/www.omg.org\/spec\/FUML\/"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11557432_3","volume-title":"Model Driven Engineering Languages and Systems","author":"R. Bendraou","year":"2005","unstructured":"Bendraou, R., Gervais, M.-P., Blanc, X.: Uml4spm: A uml2. 0-based metamodel for software process modelling. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol.\u00a03713, pp. 17\u201338. Springer, Heidelberg (2005)"},{"issue":"5","key":"6_CR16","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/TSE.2009.85","volume":"36","author":"R. Bendraou","year":"2010","unstructured":"Bendraou, R., J\u00e9z\u00e9quel, J., Gervais, M., Blanc, X.: A comparison of six uml-based languages for software process modeling. IEEE Transactions on Software Engineering\u00a036(5), 662\u2013675 (2010)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1022883727209","volume":"14","author":"W.M. Aalst van Der","year":"2003","unstructured":"van Der Aalst, W.M., Ter Hofstede, A.H., Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distributed and Parallel Databases\u00a014(1), 5\u201351 (2003)","journal-title":"Distributed and Parallel Databases"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/11841760_38","volume-title":"Business Process Management","author":"J. Mendling","year":"2006","unstructured":"Mendling, J., Moser, M., Neumann, G., Verbeek, H.M.W., van Dongen, B.F., van der Aalst, W.M.P.: Faulty epcs in the sap reference model. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol.\u00a04102, pp. 451\u2013457. Springer, Heidelberg (2006)"},{"issue":"9","key":"6_CR19","doi-asserted-by":"publisher","first-page":"897","DOI":"10.1016\/j.infsof.2007.10.015","volume":"50","author":"N. Hsueh","year":"2008","unstructured":"Hsueh, N., Shen, W., Yang, Z., Yang, D.: Applying uml and software simulation for process definition, verification, and validation. Information and Software Technology\u00a050(9), 897\u2013911 (2008)","journal-title":"Information and Software Technology"},{"key":"6_CR20","unstructured":"Trcka, N., van der Aalst, W., Sidorova, N.: Analyzing control-flow and data-flow in workflow processes in a unified way. Computer Science Report (08-31) (2008)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-07881-6_24","volume-title":"Advanced Information Systems Engineering","author":"Y. Laurent","year":"2014","unstructured":"Laurent, Y., Bendraou, R., Baarir, S., Gervais, M.-P.: Formalization of fUML: An Application to Process Verification. In: Jarke, M., Mylopoulos, J., Quix, C., Rolland, C., Manolopoulos, Y., Mouratidis, H., Horkoff, J. (eds.) CAiSE 2014. LNCS, vol.\u00a08484, pp. 347\u2013363. Springer, Heidelberg (2014)"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Coloured petri nets. Petri nets: Central models and their properties, 248\u2013299 (1987)","DOI":"10.1007\/978-3-540-47919-2_10"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Vakili, A., Day, N.: Temporal logic model checking in alloy. Abstract State Machines, Alloy, B, VDM, and Z, 150\u2013163 (2012)","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-540-75209-7_30","volume-title":"Model Driven Engineering Languages and Systems","author":"K. Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: Uml2alloy: A challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol.\u00a04735, pp. 436\u2013450. Springer, Heidelberg (2007)"},{"key":"6_CR25","unstructured":"Eclipse: Openup, \n                    \n                      http:\/\/epf.eclipse.org\/wikis\/openup\/"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Laurent, Y., Bendraou, R., Gervais, M.P.: Generation of Process using Multi-Objective Genetic Algorithm. In: Proceedings of the 2013 International Conference on Software and Systems Process. ACM (2013) (to be published)","DOI":"10.1145\/2486046.2486076"},{"issue":"3","key":"6_CR27","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1016\/j.datak.2008.05.001","volume":"66","author":"B. Weber","year":"2008","unstructured":"Weber, B., Reichert, M., Rinderle-Ma, S.: Change patterns and change support features\u2013enhancing flexibility in process-aware information systems. Data & Knowledge Engineering\u00a066(3), 438\u2013466 (2008)","journal-title":"Data & Knowledge Engineering"},{"key":"6_CR28","unstructured":"Dong, Y., ShenSheng, Z.: Using \u03c0-calculus to formalize uml activity diagram for business process modeling. In: IEEE ECBS, pp. 47\u201354 (2003)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-642-16901-4_25","volume-title":"Formal Methods and Software Engineering","author":"I. Abdelhalim","year":"2010","unstructured":"Abdelhalim, I., Sharp, J., Schneider, S., Treharne, H.: Formal verification of tokeneer behaviours modelled in fuml using csp. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 371\u2013387. Springer, Heidelberg (2010)"},{"issue":"2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0306-4379(00)00012-0","volume":"25","author":"W. Sadiq","year":"2000","unstructured":"Sadiq, W., Orlowska, M.E.: Analyzing process models using graph reduction techniques. Information Systems\u00a025(2), 117\u2013134 (2000)","journal-title":"Information Systems"},{"issue":"2","key":"6_CR31","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Modelling Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09195-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T04:22:48Z","timestamp":1558930968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09195-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319091945","9783319091952"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09195-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}