{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:12:58Z","timestamp":1748664778268,"version":"3.41.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319255781"},{"type":"electronic","value":"9783319255798"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-25579-8_21","type":"book-chapter","created":{"date-parts":[[2015,10,19]],"date-time":"2015-10-19T00:49:03Z","timestamp":1445215743000},"page":"365-383","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Timed Semantics of Workflows"],"prefix":"10.1007","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salvatore","family":"Distefano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Ferrucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Mazzara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"21_CR1","unstructured":"Bersani, M.M., Rossi, M., Pietro, P.S.: A tool for deciding the satisfiability of continuous-time metric temporal logic. In: 2013 20th International Symposium on Temporal Representation and Reasoning, 26\u201328 September, 2013, Pensacola, FL, USA, pp. 99\u2013106 (2013)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Proceedings of Logics of Programs","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Proceedings of Logics of Programs. LNCS, vol. 193, pp. 196\u2013218. Springer, Heidelberg (1985)"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: Refining real-time system specifications through bounded model- and satisfiability-checking. In: ASE, pp. 119\u2013127 (2008)","DOI":"10.1109\/ASE.2008.22"},{"key":"21_CR4","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.jlap.2006.05.007","volume":"70","author":"R Lucchi","year":"2007","unstructured":"Lucchi, R., Mazzara, M.: A pi-calculus based semantics for ws-bpel. J. Logic Algebraic Program. 70, 96\u2013118 (2007)","journal-title":"J. Logic Algebraic Program."},{"key":"21_CR5","unstructured":"Mazzara, M.: Deriving specifications of dependable systems: toward a method. In: 12th European Workshop on Dependable Computing (EWDC) (2009)"},{"key":"21_CR6","unstructured":"Mazzara, M.: On methods for the formal specification of fault tolerant systems. In: Proceedings of the 4th International Conference on Dependability (DEPEND 2011) (2011)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Gmehlich, R., Grau, K., Iliasov, A., Jackson, M., Loesch, F., Mazzara, M.: Towards a formalism-based toolkit for automotive applications. In: Formal Methods in Software Engineering (FormaliSE) (2013)","DOI":"10.1109\/FormaliSE.2013.6612275"},{"key":"21_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"21_CR9","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/174634.174636","volume":"3","author":"A Morzenti","year":"1994","unstructured":"Morzenti, A., San Pietro, P.: Object-oriented logical specification of time-critical systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 3, 56\u201398 (1994)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Ferrucci, L., Mandrioli, D., Morzenti, A., Rossi, M.: A metric temporal logic for dealing with zero-time transitions. In: Proceedings of 19th International Symposium on Temporal Representation and Reasoning, pp. 81\u201388. IEEE Computer Society (2012)","DOI":"10.1109\/TIME.2012.22"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. on Soft. Eng. Meth. (TOSEM) (2013)","DOI":"10.1145\/2491509.2491514"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1016\/j.jlap.2012.04.002","volume":"81","author":"C Vaz","year":"2012","unstructured":"Vaz, C., Ferreira, C.: On the analysis of compensation correctness. J. Log. Algebr. Program. 81, 585\u2013605 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-89287-8_4","volume-title":"Transactions on Petri Nets and Other Models of Concurrency I","author":"F Calzolai","year":"2008","unstructured":"Calzolai, F., De Nicola, R., Loreti, M., Tiezzi, F.: TAPAs: a tool for the analysis of process algebras. In: van der Aalst, W.M.P., Billington, J., Jensen, K. (eds.) Transactions on Petri Nets and Other Models of Concurrency I. LNCS, vol. 5100, pp. 54\u201370. Springer, Heidelberg (2008)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Mazzara, M., Bhattacharyya, A.: On modelling and analysis of dynamic reconfiguration of dependable real-time systems. In: DEPEND, International Conference on Dependability (2010)","DOI":"10.1109\/DEPEND.2010.33"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Montesi, F., Guidi, C., Zavattaro, G.: Service-oriented programming with jolie. In: Web Services Foundations, pp. 81\u2013107 (2014)","DOI":"10.1007\/978-1-4614-7518-7_4"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-63139-9_48","volume-title":"Application and Theory of Petri Nets 1997","author":"WMP van der Aalst","year":"1997","unstructured":"van der Aalst, W.M.P.: Verification of workflow nets. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407\u2013426. Springer, Heidelberg (1997)"},{"issue":"A","key":"21_CR17","doi-asserted-by":"publisher","first-page":"2723","DOI":"10.1587\/transfun.E92.A.2723","volume":"92","author":"M Yamaguchi","year":"2009","unstructured":"Yamaguchi, M., Yamaguchi, S., Tanaka, M.: A model checking method of soundness for workflow nets. IEICE Trans. 92(A), 2723\u20132731 (2009)","journal-title":"IEICE Trans."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Augusto, J.C., Howard, Y., Gravell, A.M., Ferreira, C., Gruner, S., Leuschel, M.: Model-based approaches for validating business critical systems. In: STEP, pp. 225\u2013233 (2003)","DOI":"10.1109\/STEP.2003.19"},{"key":"21_CR19","unstructured":"Attie, P.C., Singh, M.P.: Specifying and enforcing intertask dependencies. In: Proceedings of the 19th VLDB Conference, pp. 134\u2013145 (1993)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Eshuis, R., Wieringa, R.: Verification support for workflow design with uml activity graphs (2002)","DOI":"10.1145\/581339.581362"},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2237796.2237811","volume":"37","author":"L Baresi","year":"2012","unstructured":"Baresi, L., Morzenti, A., Motta, A., Rossi, M.: A logic-based semantics for the verification of multi-diagram uml models. ACM SIGSOFT Softw. Eng. Notes 37, 1\u20138 (2012)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"21_CR22","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0164-1212(90)90074-V","volume":"12","author":"C Ghezzi","year":"1990","unstructured":"Ghezzi, C., Mandrioli, D., Morzenti, A.: Trio: A logic language for executable specifications of real-time systems. J. Syst. Softw. 12, 107\u2013123 (1990)","journal-title":"J. Syst. Softw."},{"key":"21_CR23","unstructured":"Ferrucci, L., Bersani, M.M., Mazzara, M.: An LTL semantics of businessworkflows with recovery. In: ICSOFT-PT 2014 - Proceedings of the 9th International Conference on Software Paradigm Trends, Vienna, Austria, 29\u201331 August, 2014, pp. 29\u201340 (2014)"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-24634-3_9","volume-title":"Coordination Models and Languages","author":"MJ Butler","year":"2004","unstructured":"Butler, M.J., Ferreira, C.: An operational semantics for stac, a language for modelling longrunning business transactions. In: Meredith, G., Ferrari, G.-L., De Nicola, R. (eds.) COORDINATION 2004. LNCS, vol. 2949, pp. 87\u2013104. Springer, Heidelberg (2004)"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-14458-5_6","volume-title":"Web Services and Formal Methods","author":"N Dragoni","year":"2010","unstructured":"Dragoni, N., Mazzara, M.: A formal semantics for the ws-bpel recovery framework. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 92\u2013109. Springer, Heidelberg (2010)"},{"key":"21_CR26","volume-title":"Web services and formal methods","author":"C Eisentraut","year":"2009","unstructured":"Eisentraut, C., Spieler, D.: Web services and formal methods. Springer, Heidelberg (2009)"},{"key":"21_CR27","unstructured":"D\u00edaz, M., Valero, V., Mac\u00eda, H., Mateo, J., D\u00edaz, G.: Bpel-rf tool: An automatic translation from ws-bpel\/wsrf specifications to petri nets. In: ICSEA 2012 : The Seventh International Conference on Software Engineering Advances (2012)"},{"key":"21_CR28","unstructured":"Foster, I., Frey, J., Graham, S., Tuecke, S., Czajkowski, K., Ferguson, D., Leymann, F., Nally, M., Storey, T., Weerawaranna, S.: Modeling stateful resources with web services (2004)"},{"key":"21_CR29","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. Theor. Comp. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comp. Sci."},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Romanovsky, A., Thomas, M. (eds.): Industrial Deployment of System Engineering Methods. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-33170-1"},{"key":"21_CR31","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"21_CR32","unstructured":"OMG: Unified modeling language 2.0 (2005). http:\/\/www.omg.org\/spec\/UML\/2.0\/"},{"key":"21_CR33","unstructured":"OASIS: Web services business process execution language version 2.0 (2007). http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/wsbpel-v2.0.pdf"},{"key":"21_CR34","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205, 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"key":"21_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-24288-5_7","volume-title":"Reachability Problems","author":"MM Bersani","year":"2011","unstructured":"Bersani, M.M., Frigeri, A., Rossi, M., San Pietro, P.: Completeness of the bounded satisfiability problem for constraint LTL. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 58\u201371. Springer, Heidelberg (2011)"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Ellis, C., Keddara, K., Rozenberg, G.: Dynamic change within workflow systems. In: Proceedings of Conference on Organizational Computing Systems. COCS 1995, pp. 10\u201321. ACM, New York (1995)","DOI":"10.1145\/224019.224021"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: A tool for deciding the satisfiability of continuous-time metric temporal logic. In: Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME), pp. 99\u2013106 (2013)","DOI":"10.1109\/TIME.2013.20"},{"key":"21_CR38","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1022883727209","volume":"14","author":"W Aalst van der","year":"2003","unstructured":"van der Aalst, W., ter Hofstede, A., Kiepuszewski, B., Barros, A.: Workflow patterns. Distrib. Parallel Databases 14, 5\u201351 (2003)","journal-title":"Distrib. Parallel Databases"},{"key":"21_CR39","unstructured":"OMG: Business process model and notation (bpmn) (2011). http:\/\/www.bpmn.org\/"},{"key":"21_CR40","first-page":"73","volume":"2","author":"M Mazzara","year":"2012","unstructured":"Mazzara, M., Dragoni, N., Zhou, M.: Implementing workflow reconfiguration in ws-bpel. Security 2, 73\u201392 (2012)","journal-title":"Security"},{"key":"21_CR41","doi-asserted-by":"crossref","DOI":"10.1515\/9781400884223","volume-title":"Non-standard analysis","author":"A Robinson","year":"1996","unstructured":"Robinson, A.: Non-standard analysis. Princeton University Press, Princeton (1996)"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Baresi, L., Guinea, S., Manna, V.P.L.: Consistent runtime evolution of service-based business processes. In: Liu, A., John Klein, A.T. (ed.) Working IEEE\/IFIP Conference on Software Architecture (WICSA) (2014)","DOI":"10.1109\/WICSA.2014.24"}],"container-title":["Communications in Computer and Information Science","Software Technologies"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25579-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T02:13:02Z","timestamp":1748657582000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25579-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319255781","9783319255798"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25579-8_21","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 October 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}