Abstract
Workflows have proven to be a useful conceptualization for the automation of business processes. While formal verification methods (e.g., model checking) can help ensure the reliability of workflow systems, the industrial uptake of such methods has been slow largely due to the effort involved in modeling and the memory required to verify complex systems. Incorporation of time constraints in such systems exacerbates the latter problem. We present an automated translator, YAWL2DVE-t, which takes as input a time constrained workflow model built with the graphical modeling tool YAWL, and outputs the model in DVE, the system specification language for the distributed LTL model checker DiVinE. The automated translator, together with the graphical editor and the distributed model checker, provides a method for rapid design, verification and refactoring of time constrained workflow systems. We present a realistic case study developed through collaboration with the local health authority.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Miller, K., MacCaull, W.: Toward web-based careflow management systems. Journal of Emerging Technologies in Web Intelligence (JETWI) Special Issue: E-health Interoperability 1(2), 137–145 (2009)
Wang, F.: Formal verification of timed systems: A survey and perspective. Proceedings of the IEEE 92, 1283–1305 (2004)
Marjanovic, O.: Dynamic verification of temporal constraints in production workflows. In: ADC ’00: Proceedings of the Australasian Database Conference, Washington, DC, USA, pp. 74–81. IEEE Computer Society, Los Alamitos (2000)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California, Irvine, CA (1974)
Gruhn, V., Laue, R.: Using timed model checking for verifying workflows. In: Cordeiro, J., Filipe, J. (eds.) Computer Supported Activity Coordination, pp. 75–88. INSTICC Press (2005)
Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J. P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Heidelberg (2002)
Krcál, P., Yi, W.: Decidable and undecidable problems in schedulability analysis using timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 236–250. Springer, Heidelberg (2004)
Foyo, P.M.G.D., Silva, J.R.: Using time petri nets for modeling and verification of timed constrained workflow systems. In: ABCM Symposium Series in Mechatronics, vol. 3, pp. 471–478 (2008)
Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Roméo: A tool for analyzing time petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)
Berthomieu, B., Vernadat, F.: Time petri nets analysis with tina. In: 3rd International Conference on The Quantitative Evaluation of Systems (QEST 2006), pp. 123–124. IEEE Computer Society Press, Los Alamitos (2006)
Barnat, J., Brim, L., Ročkai, P.: Scalable multi-core ltl model-checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 187–203. Springer, Heidelberg (2007)
Barnat, J., Brim, L., Ročkai, P.: DiVinE 2.0: High-Performance model checking. In: International Workshop on High Performance Computational Systems Biology (HiBi 09), pp. 31–32. IEEE Computer Society, Los Alamitos (2009)
Leyla, N., Mashiyat, A., Wang, H., MacCaull, W.: Workflow verification with divine. In: 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC ’09) (2009) Work in progress report
Russell, N., Hofstede, A.T., Aalst, W.M.P.V.D., Mulyar, N.: Workflow control-flow patterns: A revised view. Technical report, BPMcenter.org (2006)
Rabbi, F., Wang, H., MacCaull, W.: YAWL2DVE: An automated translator for workflow verification. In: 4th IEEE International Conference on Secure Software Integration and Reliability Improvement, pp. 53–59. IEEE Computer Society, Los Alamitos (2010)
Aalst, W.M.P.V.D., Hofstede, A.T.: Yawl: yet another workflow language. Information Systems 30(4), 245–275 (2005)
DiVinE Project, http://divine.fi.muni.cz/ (last accessed June 2010)
Li, W., Fan, Y.: A time management method in workflow management system. In: Workshops at the Grid and Pervasive Computing Conference, pp. 3–10. IEEE Computer Society, Los Alamitos (2009)
WfMC: Workflow management coalition terminology and glossary. Technical Report (wfmc-tc-1011) v3.0. Technical report, Winchester, UK (1999)
Combi, C., Posenato, R.: Controllability in temporal conceptual workflow schemata. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 64–79. Springer, Heidelberg (2009)
Combi, C., Gozzi, M., Juárez, J.M., Oliboni, B., Pozzi, G.: Conceptual modeling of temporal clinical workflows. In: TIME, pp. 70–81. IEEE Computer Society, Los Alamitos (2007)
Li, H., Yang, Y.: Verification of temporal constraints for concurrent workflows. In: Yu, J.X., Lin, X., Lu, H., Zhang, Y. (eds.) APWeb 2004. LNCS, vol. 3007, pp. 804–813. Springer, Heidelberg (2004)
Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)
Wang, H., MacCaull, W.: An efficient explicit-time description method for timed model checking. In: 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 09), Eindhoven, The Netherlands, EPTCS, vol. 14, pp. 77–91 (2009)
Berg, L.V.D., Strooper, P.A., Winter, K.: Introducing time in an industrial application of model-checking. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 56–67. Springer, Heidelberg (2008)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Ferris, F.D., Balfour, H.M., Bowen, K., Farley, J., Hardwick, M., Lamontagne, C., Lundy, M., Syme, A., West, P.: A model to guide hospice palliative care: Based on national principles and norms of practice. Canadian Hospice Palliative Care Association, Ottawa (2002)
Atlantic Computational Excellence Network (ACEnet), http://www.ace-net.ca/ (last accessed, June 2010)
Centre for Logic and Information. St. Francis Xavier University, http://logic.stfx.ca/ (last accessed, June 2010)
Miller, K., MacCaull, W.: Verification of careflow management systems with timed BDI CTL logic. In: 3rd International Workshop on Process-oriented Information Systems in Healthcare (ProHealth’09), in Conjunction with BPM’09. LNBIP, vol. 43, pp. 623–634. Springer, Heidelberg (2010)
Wang, H., MacCaull, W.: Verifying real-time systems using explicit-time description methods. In: Workshop on Quantitative Formal Methods: Theory and Applications, Eindhoven, The Netherlands, EPTCS, vol. 13, pp. 67–79 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mashiyat, A.S., Rabbi, F., Wang, H., MacCaull, W. (2010). An Automated Translator for Model Checking Time Constrained Workflow Systems. In: Kowalewski, S., Roveri, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2010. Lecture Notes in Computer Science, vol 6371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15898-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-15898-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15897-1
Online ISBN: 978-3-642-15898-8
eBook Packages: Computer ScienceComputer Science (R0)