Abstract
We formalize timed workflow with abnormal behavior management (i.e. recovery) and demonstrate how temporal logics and model checking are methodologies to iteratively revise the design correct-by construction system. We define a formal semantics by compiling generic workflow patterns into an extension of LTL with dense time clocks (CLTLoc). CLTLoc allows us to define the first logical formalization of workflows that can be practically employed in verification tools and to avoid the use of well-known automata based formalisms dealing with real-time. We use an ad-hoc bound model checker to prove requirements validity on a business process. The working assumption is that lightweight approaches easily fit into processes that are already in place so that radical change of procedures, tools and people’s attitudes are not needed. The complexity of formalisms and invasiveness of methods have been demonstrated to be one of the major drawback and obstacle for deployment of formal engineering techniques into mundane projects.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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–28 September, 2013, Pensacola, FL, USA, pp. 99–106 (2013)
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–218. Springer, Heidelberg (1985)
Pradella, M., Morzenti, A., San Pietro, P.: Refining real-time system specifications through bounded model- and satisfiability-checking. In: ASE, pp. 119–127 (2008)
Lucchi, R., Mazzara, M.: A pi-calculus based semantics for ws-bpel. J. Logic Algebraic Program. 70, 96–118 (2007)
Mazzara, M.: Deriving specifications of dependable systems: toward a method. In: 12th European Workshop on Dependable Computing (EWDC) (2009)
Mazzara, M.: On methods for the formal specification of fault tolerant systems. In: Proceedings of the 4th International Conference on Dependability (DEPEND 2011) (2011)
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)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Morzenti, A., San Pietro, P.: Object-oriented logical specification of time-critical systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 3, 56–98 (1994)
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–88. IEEE Computer Society (2012)
Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. on Soft. Eng. Meth. (TOSEM) (2013)
Vaz, C., Ferreira, C.: On the analysis of compensation correctness. J. Log. Algebr. Program. 81, 585–605 (2012)
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–70. Springer, Heidelberg (2008)
Mazzara, M., Bhattacharyya, A.: On modelling and analysis of dynamic reconfiguration of dependable real-time systems. In: DEPEND, International Conference on Dependability (2010)
Montesi, F., Guidi, C., Zavattaro, G.: Service-oriented programming with jolie. In: Web Services Foundations, pp. 81–107 (2014)
van der Aalst, W.M.P.: Verification of workflow nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407–426. Springer, Heidelberg (1997)
Yamaguchi, M., Yamaguchi, S., Tanaka, M.: A model checking method of soundness for workflow nets. IEICE Trans. 92(A), 2723–2731 (2009)
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–233 (2003)
Attie, P.C., Singh, M.P.: Specifying and enforcing intertask dependencies. In: Proceedings of the 19th VLDB Conference, pp. 134–145 (1993)
Eshuis, R., Wieringa, R.: Verification support for workflow design with uml activity graphs (2002)
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–8 (2012)
Ghezzi, C., Mandrioli, D., Morzenti, A.: Trio: A logic language for executable specifications of real-time systems. J. Syst. Softw. 12, 107–123 (1990)
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–31 August, 2014, pp. 29–40 (2014)
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–104. Springer, Heidelberg (2004)
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–109. Springer, Heidelberg (2010)
Eisentraut, C., Spieler, D.: Web services and formal methods. Springer, Heidelberg (2009)
Díaz, M., Valero, V., Macía, H., Mateo, J., Díaz, 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)
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)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comp. Sci. 126, 183–235 (1994)
Romanovsky, A., Thomas, M. (eds.): Industrial Deployment of System Engineering Methods. Springer, Heidelberg (2013)
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231–274 (1987)
OMG: Unified modeling language 2.0 (2005). http://www.omg.org/spec/UML/2.0/
OASIS: Web services business process execution language version 2.0 (2007). http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf
Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205, 380–415 (2007)
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–71. Springer, Heidelberg (2011)
Ellis, C., Keddara, K., Rozenberg, G.: Dynamic change within workflow systems. In: Proceedings of Conference on Organizational Computing Systems. COCS 1995, pp. 10–21. ACM, New York (1995)
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–106 (2013)
van der Aalst, W., ter Hofstede, A., Kiepuszewski, B., Barros, A.: Workflow patterns. Distrib. Parallel Databases 14, 5–51 (2003)
OMG: Business process model and notation (bpmn) (2011). http://www.bpmn.org/
Mazzara, M., Dragoni, N., Zhou, M.: Implementing workflow reconfiguration in ws-bpel. Security 2, 73–92 (2012)
Robinson, A.: Non-standard analysis. Princeton University Press, Princeton (1996)
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)
Acknowledgements
The authors acknowledge the support and advice given by Marina Carvalho, Miticus Flamejante, Vínicius Pereira, Diego Pérez, Michele Ciavotta, Marco Miglierina and all the other Friends at Politecnico di Milano, which represent a moving force, an actual égrégore capable of always moving ideas forward to the next level.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bersani, M.M., Distefano, S., Ferrucci, L., Mazzara, M. (2015). A Timed Semantics of Workflows. In: Holzinger, A., Cardoso, J., Cordeiro, J., Libourel, T., Maciaszek, L., van Sinderen, M. (eds) Software Technologies. ICSOFT 2014. Communications in Computer and Information Science, vol 555. Springer, Cham. https://doi.org/10.1007/978-3-319-25579-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-25579-8_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25578-1
Online ISBN: 978-3-319-25579-8
eBook Packages: Computer ScienceComputer Science (R0)