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

• Autorzy: Klimek R.

Identyfikatory

DOI

10.2478/amcs-2014-0069

• Języki publikacji: EN

Abstrakty

EN

The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model’s behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is based on the semantic tableaux method, which has some advantages when compared with traditional deduction strategies. The algorithm for automatic generation of logical specifications is proposed. The generation procedure is based on predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of business processes. The main idea behind the approach is to consider patterns, defined in terms of temporal logic, as a kind of (logical) primitives which enable the transformation of models to temporal logic formulas constituting a logical specification. Automation of the generation process is crucial for bridging the gap between the intuitiveness of deductive reasoning and the difficulty of its practical application when logical specifications are built manually. This approach has gone some way towards supporting, hopefully enhancing, our understanding of deduction-based formal verification of workflow-oriented models.

Słowa kluczowe

EN

formal verification; deductive reasoning; temporal logic; semantic tableaux; workflow pattern; logical primitive; generating logical specification; business model; BPMN

PL

formalna weryfikacja; wnioskowanie dedukcyjne; logika temporalna; tablica semantyczna; wzorzec przepływu pracy; generowanie specyfikacji logicznej; model biznesowy; BPMN

• Wydawca: Oficyna Wydawnicza Uniwersytetu Zielonogórskiego
• Czasopismo: International Journal of Applied Mathematics and Computer Science
• Rocznik: 2014
• Tom: Vol. 24, no. 4
• Strony: 941--956
• Opis fizyczny: Bibliogr. 51 poz., rys., tab.

Twórcy

autor

Klimek R.

• Department of Applied Computer Science, AGH University of Science and Technology, al. A. Mickiewicza 30, 30-059 Kraków, Poland

Bibliografia

• [1] Abrial, J.-R. (2007). Formal methods: Theory becoming practice, Journal of Universal Computer Science 13(5): 619–628.
• [2] Alpern, B. and Schneider, F.B. (1985). Defining liveness, Information Processing Letters 21(4): 181–185.
• [3] 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.
• [4] Booch, G., Rumbaugh, J. and Jacobson, I. (1999). The Unified Modeling Language Reference Manual, Addison Wesley, Redwood City, CA.
• [5] 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.
• [6] 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.
• [7] Chellas, B.F. (1980). Modal Logic, Cambridge University Press, Cambridge.
• [8] Clarke, E., Grumberg, O. and Peled, D. (1999). Model Checking, MIT Press, Cambridge, MA.
• [9] Clarke, E. and Wing, J. (1996). Formal methods: State of the art and future directions, ACM Computing Surveys 28(4): 626–643.
• [10] d’Agostino, M., Gabbay, D., Hähnle, R. and Posegga, J. (1999). Handbook of Tableau Methods, Kluwer Academic Publishers, Hingham, MA.
• [11] 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.
• [12] 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.
• [13] Dijkstra, E.W. (1972). Structured Programming, Academic Press, London, pp. 1–82.
• [14] 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ès (Eds.), Proceedings of the 9th International Conference on Computer Supported Cooperative Work in Design, CSCWD 2005, 24–26 May 2005, Coventry, UK, Vol. 1, IEEE Computer Society, Washington, DC, pp. 508–513.
• [15] 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.
• [16] Emerson, E. (1990). Handbook of Theoretical Computer Science, Vol. B, MIT Press, Cambridge, MA, pp. 995–1072.
• [17] Eshuis, R. and Wieringa, R. (2004). Tool support for verifying UML activity diagrams, IEEE Transactions on Software Engineering 30(7): 437–447.
• [18] 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.
• [19] Gries, D. and Schneider, F.B. (1993). A Logical Approach to Discrete Math, Springer Verlag, New York, NY.
• [20] Hähnle, R. (1998). Tableau-based theorem proving, 10th European Summer School on Logic, Language and Information, ESSLLI 1998, Saarbrücken, Germany.
• [21] 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.
• [22] Kleene, S.C. (1952). Introduction to Metamathematics, Bibliotheca Mathematica, North-Holland, Amsterdam.
• [23] 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.
• [24] 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.
• [25] 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ów, Poland, pp. 1049–1055.
• [26] 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.
• [27] 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–18 September 2010, IEEE Computer Society, Washington, DC, pp. 135–144.
• [28] 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.
• [29] 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.
• [30] 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.
• [31] 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.
• [32] Pender, T. (2003). UML Bible, John Wiley & Sons, New York, NY.
• [33] 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.
• [34] Rasmussen, R. and Brown, R. (2012). A deductive system for proving workflow models from operational procedures, Future Generation Computer Systems 28(5): 732–742.
• [35] Riehle, D. and Züllighoven, H. (1996). Understanding and using patterns in software development, Theory and Practice of Object Systems 2(1): 3–13.
• [36] Schmidt, R. (2014). Accessible theorem provers, http://www.cs.man.ac.uk/˜schmidt/tools/.
• [37] Shankar, N. (2009). Automated deduction for verification, ACM Computing Surveys 41(4): 20:1–20:56.
• [38] 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.
• [39] van Benthem, J. (1993–95). Handbook of Logic in Artificial Intelligence and Logic Programming, 4, Oxford University Press, New York, NY, pp. 241–350.
• [40] 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.
• [41] van der Aalst, W.M.P. and ter Hofstede, A.H.M. (2005). YAWL: Yet another workflow language, Information Systems 30(4): 245–275.
• [42] van der Aalst, W.M., ter Hofstede, A., Kiepusewski, B. and Barros, A. (2003). Workflow patterns, Distributed and Parallel Databases 4(1): 5–51.
• [43] Venema, Y. (2001). Blackwell Guide to Philosophical Logic, Basil Blackwell Publishers, Oxford, pp. 203–223.
• [44] 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.
• [45] 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.
• [46] Wolter, F. and Wooldridge, M. (2011). Temporal and dynamic logic, Journal of Indian Council of Philosophical Research XXVII(1): 249–276.
• [47] Wong, P.Y. and Gibbons, J. (2011). Property specifications for workflow modelling, Science of Computer Programming 76(10): 942–967.
• [48] 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.
• [49] 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.
• [50] 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.
• [51] Zha, H., van der Aalst, W.M.P., Wang, J., Wen, L. and Sun, J. (2011). Verifying workflow processes: A transformation based approach, Software & Systems Modeling 10(2): 253–264.