A system for deduction-based formal verification of workflow-oriented software models

Abrial, J.-R. (2007). Formal methods: Theory becoming practice, Journal of Universal Computer Science 13(5): 619-628.Search in Google Scholar

Alpern, B. and Schneider, F.B. (1985). Defining liveness, Information Processing Letters 21(4): 181-185.10.1016/0020-0190(85)90056-0Search in Google Scholar

Barker, A. and Van Hemert, J. (2008). Scientific workflow: A survey and research directions, in R. Wyrzykowski, J. Dongarra, K. Karczewski and J.Wasniewski (Eds.), Proceedings of the 7th International Conference Parallel Processing and Applied Mathematics, PPAM 2008, Gdańsk, Poland, 9-12 September 2007, Lecture Notes in Computer Science, Vol. 4967, Springer Verlag, Berlin, pp. 746-753.10.1007/978-3-540-68111-3_78Search in Google Scholar

Booch, G., Rumbaugh, J. and Jacobson, I. (1999). The Unified Modeling Language Reference Manual, Addison Wesley, Redwood City, CA.Search in Google Scholar

Brambilla, M., Deutsch, A., Sui, L. and Vianu, V. (2005). The role of visual tools in a web application design and verification framework: A visual notation for LTL formulae, in D. Lowe and M. Gaedke (Eds.), Proceedings of the 5th International Conference on Web Engineering ICWE 2005, July 27-29, 2005, Sydney, Australia, Lecture Notes in Computer Science, Vol. 3579, Springer Verlag, Berlin, pp. 557-568.10.1007/11531371_70Search in Google Scholar

Bryans, J.W. and Wei, W. (2010). Formal analysis of BPMN models using Event-B, in S. Kowalewski and M. Roveri (Eds), 15th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2010, 20-21 September 2010, Antwerp, Belgium, Lecture Notes in Computer Science, Vol. 6371, Springer Verlag, Berlin, pp. 33-49.10.1007/978-3-642-15898-8_3Search in Google Scholar

Chellas, B.F. (1980). Modal Logic, Cambridge University Press, Cambridge.10.1017/CBO9780511621192Search in Google Scholar

Clarke, E., Grumberg, O. and Peled, D. (1999). Model Checking, MIT Press, Cambridge, MA.Search in Google Scholar

Clarke, E. and Wing, J. (1996). Formal methods: State of the art and future directions, ACM Computing Surveys 28(4): 626-643. d’Agostino, M., Gabbay, D., Hähnle, R. and Posegga, J. (1999).Search in Google Scholar

Handbook of Tableau Methods, Kluwer Academic Publishers, Hingham, MA.Search in Google Scholar

Dehnert, J. and van der Aalst, W.M.P. (2004). Bridging the gap between business models and workflow specifications, International Journal of Cooperative Information Systems 13(03): 289-332.10.1142/S0218843004000973Search in Google Scholar

Dijkman, R.M., Dumas, M. and Ouyang, C. (2008). Semantics and analysis of business process models in BPMN, Information and Software Technology 50(12): 1281-1294.10.1016/j.infsof.2008.02.006Search in Google Scholar

Dijkstra, E.W. (1972). Structured Programming, Academic Press, London, pp. 1-82.Search in Google Scholar

Duan, Y. and Ma, H. (2005). Modeling flexible workflow based on temporal logic, in W. Shen, A.E. James, K.-M. Chao, M. Younas, Z. Lin and J.-P.A. Barth`es (Eds.), Proceedings of the 9th International Conference on Computer Supported Cooperative Work in Design, CSCWD 2005, 24-26Search in Google Scholar

May 2005, Coventry, UK, Vol. 1, IEEE Computer Society, Washington, DC, pp. 508-513.Search in Google Scholar

Dury, A., Boroday, S., Petrenko, A. and Lotz, V. (2007). Formal verification of business workflows and role based access control systems, in L. Peñalver, O.A. Dini, J. Mulholland and O. Nieto-Taladriz (Eds.), Proceedings of the 1st International Conference on Emerging Security Information, Systems and Technologies, SecurWare 2007, October 14-20, 2007, Valencia, Spain, IEEE Computer Society, Washington, DC, pp. 201-210.10.1109/SECUREWARE.2007.4385334Search in Google Scholar

Emerson, E. (1990). Handbook of Theoretical Computer Science, Vol. B, MIT Press, Cambridge, MA, pp. 995-1072.Search in Google Scholar

Eshuis, R. and Wieringa, R. (2004). Tool support for verifying UML activity diagrams, IEEE Transactions on Software Engineering 30(7): 437-447.10.1109/TSE.2004.33Search in Google Scholar

Frece, A. and Juric, M.B. (2012). Modeling functional requirements for configurable content- and context-aware dynamic service selection in business process models, Journal of Visual Languages & Computing 23(4): 223-247.10.1016/j.jvlc.2012.02.003Search in Google Scholar

Gries, D. and Schneider, F.B. (1993). A Logical Approach to Discrete Math, Springer Verlag, New York, NY.10.1007/978-1-4757-3837-7Search in Google Scholar

Hähnle, R. (1998). Tableau-based theorem proving, 10th European Summer School on Logic, Language and Information, ESSLLI 1998, Saarbrücken, Germany.Search in Google Scholar

Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A.J.H., Vilkomir, S., Woodward, M.R. and Zedan, H. (2009). Using formal specifications to support testing, ACM Computing Survey 41(2): 9:1-9:76.10.1145/1459352.1459354Search in Google Scholar

Kleene, S.C. (1952). Introduction to Metamathematics, Bibliotheca Mathematica, North-Holland, Amsterdam.Search in Google Scholar

Klimek, R. (2012). Towards formal and deduction-based analysis of business models for SOA processes, in J. Filipe and A. Fred (Eds.), Proceedings of the 4th International Conference on Agents and Artificial Intelligence, ICAART 2012, 6-8 February 2012, Vilamoura, Algarve, Portugal, Vol. 2, SciTePress, Lisboa, pp. 325-330.Search in Google Scholar

Klimek, R. (2013). From extraction of logical specifications to deduction-based formal verification of requirements models, in R.M. Hierons, M.G. Merayo and M. Bravetti (Eds.), Proceedings of the 11th International Conference on Software Engineering and Formal Methods, SEFM 2013, 25-27 September 2013, Madrid, Spain, Lecture Notes in Computer Science, Vol. 8137, Springer Verlag, Berlin, pp. 61-75.10.1007/978-3-642-40561-7_5Search in Google Scholar

Klimek, R., Faber, Ł. and Kisiel-Dorohinicki, M. (2013). Verifying data integration agents with deduction-based models, Proceedings of the Federated Conference on Computer Science and Information Systems, FedCSIS 2013, Krak´ow, Poland, pp. 1049-1055.Search in Google Scholar

Ko, R.K., Lee, S.S. and Lee, E.W. (2009). Business process management (BPM) standards: A survey, Business Process Management Journal 15(5): 744-791.10.1108/14637150910987937Search in Google Scholar

Leuxner, C., Sitou, W. and Spanfelner, B. (2010). A formal model for work flows, in J.L. Fiadeiro, S. Gnesi and A. Maggiolo-Schettini (Eds.), Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, 13-1810.1109/SEFM.2010.27Search in Google Scholar

September 2010, IEEE Computer Society, Washington, DC, pp. 135-144.Search in Google Scholar

Ma, S., Zhang, L. and He, J. (2008). Towards formalization and verification of unified business process model based on pi calculus, Proceedings of the 6th ACIS International Conference on Software Engineering Research, Management and Applications, SERA 2008, 20-22 August 2008, Prague, Czech Republic, IEEE Computer Society, Washington, DC, pp. 93-101.Search in Google Scholar

Maggi, F.M., Montali, M., Westergaard, M. and van der Aalst, W.M.P. (2011). Monitoring business constraints with linear temporal logic: An approach based on colored automata, Proceedings of the 9th International Conference on Business Process Management, BPM 2011, 30 August-2 September 2011, Clermont-Ferrand, France, Lecture Notes in Computer Science, Vol. 6896, Springer Verlag, Berlin, pp. 132-147.Search in Google Scholar

Morimoto, S. (2008). A survey of formal verification for business process modeling, in M. Bubak, G.D. van Albada, J. Dongarra and P.M.A. Sloot (Eds.), Proceedings of the 8th International Conference on Computational Science, ICCS 2008, June 23-25, 2008, Kraków, Poland, Part II, Lecture Notes in Computer Science, Vol. 5102, Springer Verlag, Berlin, pp. 514-522.10.1007/978-3-540-69387-1_58Search in Google Scholar

OMG (2011). Business process model and notation (BPMN) version 2.0, Technical report, Object Management Group, Needham, MA, http://www.omg.org/spec/bpmn/2.0.Search in Google Scholar

Pender, T. (2003). UML Bible, John Wiley & Sons, New York, NY.Search in Google Scholar

Rao, M.R., Hildebrandt, T.T. and Tth, J.B. (2008). The resultmaker online consultant: From declarative workflow management in practice to LTL, in M. van Sinderen, J.P.A. Almeida, L.F. Pires and M. Steen (Eds.), 12th Enterprise Distributed Object Computing Conference Workshops, EDOCW 2008, 16 September 2008, Munich, Germany, IEEE Computer Society, Washington, DC, pp. 135-142.10.1109/EDOCW.2008.57Search in Google Scholar

Rasmussen, R. and Brown, R. (2012). A deductive system for proving workflow models from operational procedures, Future Generation Computer Systems 28(5): 732-742.10.1016/j.future.2012.01.001Search in Google Scholar

Riehle, D. and Züllighoven, H. (1996). Understanding and using patterns in software development, Theory and Practice of Object Systems 2(1): 3-13.10.1002/(SICI)1096-9942(1996)2:1<3::AID-TAPO1>3.0.CO;2-#Search in Google Scholar

Schmidt, R. (2014). Accessible theorem provers, http://www.cs.man.ac.uk/˜schmidt/tools/.Search in Google Scholar

Shankar, N. (2009). Automated deduction for verification, ACM Computing Surveys 41(4): 20:1-20:56.10.1145/1592434.1592437Search in Google Scholar

Taibi, T. and Ngo, D.C.L. (2003). Modeling of distributed objects computing design pattern combinations using a formal specification language, International Journal of Applied Mathematics and Computer Science 13(2): 239-253. van Benthem, J. (1993-95). Handbook of Logic in Artificial Intelligence and Logic Programming, 4, Oxford University Press, New York, NY, pp. 241-350. van der Aalst, W.M.P. (2002). Making work flow: On the application of Petri nets to business process management, Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets, ICATPN 2002, 24-30 June 2002, Adelaide, Australia, Lecture Notes in Computer Science, Vol. 2360, Springer Verlag, Berlin, pp. 1-12. van der Aalst, W.M.P. and ter Hofstede, A.H.M. (2005).Search in Google Scholar

YAWL: Yet another workflow language, Information Systems 30(4): 245-275. van der Aalst, W.M., ter Hofstede, A., Kiepusewski, B. and Barros, A. (2003). Workflow patterns, Distributed and Parallel Databases 4(1): 5-51.10.1016/j.is.2004.02.002Search in Google Scholar

Venema, Y. (2001). Blackwell Guide to Philosophical Logic, Basil Blackwell Publishers, Oxford, pp. 203-223. Westergaard, M. (2011). Better algorithms for analyzing and enacting declarative workflow languages using LTL, Proceedings of the 9th International Conference Business Process Management, BPM 2011, 30 August-2 September 2011, Clermont-Ferrand, France, Lecture Notes in Computer Science, Vol. 6896, Springer Verlag, Berlin, pp. 83-98.Search in Google Scholar

White, S.A. (2004). Process modeling notations and workflow patterns, BPTrends, pp. 1-25, http://www.omg.org/ bpmn/Documents/Notations_and_Workflow _Patterns.pdf.Search in Google Scholar

Wolter, F. and Wooldridge, M. (2011). Temporal and dynamic logic, Journal of Indian Council of Philosophical Research XXVII(1): 249-276.Search in Google Scholar

Wong, P.Y. and Gibbons, J. (2011). Property specifications for workflow modelling, Science of Computer Programming 76(10): 942-967.10.1016/j.scico.2010.09.007Search in Google Scholar

Woodcock, J., Larsen, P.G., Bicarregui, J. and Fitzgerald, J. (2009). Formal methods: Practice and experience, ACM Computing Survey 41(4): 19:1-19:36.10.1145/1592434.1592436Search in Google Scholar

Xu, L.D., Viriyasitavat, W., Ruchikachorn, P. and Martin, A. (2012). Using propositional logic for requirements verification of service workflow, IEEE Transactions on Industrial Informatics 8(3): 639-646.10.1109/TII.2012.2187908Search in Google Scholar

Yu, Y. and Li, X. (2007). A workflow model with temporal logic constraints and its automated verification, Proceedings of the 6th International Conference on Grid and Cooperative Computing, GCC 2007, August 16-18, 2007, Urumchi, Xinjiang, China, IEEE Computer Society,Washington, DC, pp. 681-684.Search in Google Scholar

Zha, H., van der Aalst, W.M.P., Wang, J., Wen, L. and Sun, J. (2011). Verifying workflow processes: A transformationbased approach, Software & Systems Modeling 10(2): 253-264. 10.1007/s10270-010-0149-9Search in Google Scholar