Abstract
In this paper, we present a characterization of workflows as labeled transition systems, focusing on an encoding of workflow specifications based on workflow patterns. This encoding models tasks in a convenient way, enabling us to exploit fluent linear time temporal logic formulas for capturing typical constraints on workflows. Fluents enable us to flexibly characterize the activities associated with workflow tasks, and also to easily express a wide range of constraints on workflows. Moreover, our characterization of workflows as labeled transition systems, and the use of fluent linear time temporal logic as a language to express workflow properties, allows us to employ model checking for automatically guaranteeing that a property is satisfied by a workflow, or generating violating workflow executions when such property does not hold.
We use YAWL as a language for expressing workflows. Our characterization of workflows as labeled transition systems is implemented in a tool that translates YAWL models into FSP, and then employs the LTSA tool to automatically verify properties of workflows, expressed as fluent linear time temporal logic properties, on the resulting FSP models.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Model Check
- Temporal Logic
- Linear Temporal Logic
- Label Transition System
- Business Process Execution Language
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
van der Aalst, W.M.P., ter Hofstede, A.H.M., Kiepuszewski, B., Barros, A.P.: Workflow Patterns. Distributed and Parallel Databases 14, 5–51 (2003)
van der Aalst, W.M.P., ter Hofstede, A.H.M.: YAWL: yet another workflow language. Inf. Syst. 30, 245–275 (2005)
van der Aalst, W.M.P., et al.: Soundness of workflow nets: classification, decidability, and analysis. Formal Asp. Comput. 23(3), 333–363 (2011)
van Breugel, F., Koshkina, M.: Models and Verification of BPEL (2006), http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)
Rabbi, F., Wang, H., MacCaull, W.: YAWL2DVE: An Automated Translator for Workflow Verification. In: SSIRI, pp. 53–59 (2010)
Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: ESEC / SIGSOFT FSE, pp. 257–266 (2003)
Girault, C., Valk, R.: Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Springer (2002)
ter Hofstede, A.H.M., van der Aalst, W.M.P., Adams, M., Russell, N.: Modern Bussiness Process Automation. Springer (2010)
Karamanolis, C.T., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model Checking of Workflow Schemas. In: EDOC, pp. 170–181 (2000)
Kindler, E.: On the semantics of EPCs: Resolving the vicious circle. Data Knowl. Eng. 56(1), 23–40 (2006)
Leyla, N., Mashiyat, A.S., Wang, H., MacCaull, W.: Towards workflow verification. In: CASCON, pp. 253–267 (2010)
Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. John Wiley & Sons (1999)
Maggi, F.M., Montali, M., Westergaard, M., van der Aalst, W.M.P.: Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 132–147. Springer, Heidelberg (2011)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer (1991)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems -Safety. Springer (1995)
Miller, R., Shanahan, M.: The Event Calculus in Classical Logic - Alternative Axiomatisations. Linkoping Electronic Articles in Computer and Information Science 4(16), 1–27 (1999)
Morimoto, S.: A Survey of Formal Verification for Business Process Modeling. In: ICCS 2008, pp. 514–522 (2008)
Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: Declarative Workflow. In: Modern Business Process Automation, pp. 175–201 (2010)
Regis, G., Aguirre, N., Maibaum, T.: Specifying and Verifying Business Processes Using PPML. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 737–756. Springer, Heidelberg (2009)
Wong, P.Y.H., Gibbons, J.: Property specifications for workflow modelling. Sci. Comput. Program 76(10), 942–967 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Regis, G., Ricci, N., Aguirre, N.M., Maibaum, T. (2012). Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows. In: Gheyi, R., Naumann, D. (eds) Formal Methods: Foundations and Applications. SBMF 2012. Lecture Notes in Computer Science, vol 7498. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33296-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-33296-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33295-1
Online ISBN: 978-3-642-33296-8
eBook Packages: Computer ScienceComputer Science (R0)