Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business Processes

• Autorzy: Montali M. , Torroni P. , Chesani F. , Mello P. , Alberti M. , Lamma E.
• Języki publikacji: EN

Abstrakty

EN

We discuss the static verification of declarative Business Processes. We identify four desiderata about verifiers, and propose a concrete framework which satisfies them. The framework is based on the ConDec graphical notation for modeling Business Processes, and on Abductive Logic Programming technology for verification of properties. Empirical evidence shows that our verification method seems to perform and scale better, in most cases, than other state of the art techniques (model checkers, in particular). A detailed study of our framework's theoretical properties proves that our approach is sound and complete when applied to ConDec models that do not contain loops, and it is guaranteed to terminate when applied to models that contain loops.

Słowa kluczowe

EN

static verification; business process management; declarative business process modeling; Abductive Logic Programming (ALP); model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 3/4
• Strony: 325--361
• Opis fizyczny: Bibliogr. 48 poz., tab., wykr.

Twórcy

autor

Montali M.

autor

Torroni P.

autor

Chesani F.

autor

Mello P.

autor

Alberti M.

autor

Lamma E.

• DEIS, University of Bologna – V.le Risorgimento 2, 40136 Bologna, Italy,

Bibliografia

• [1] van der Aalst, W. M. P., Pesic, M.: DecSerFlow: Towards a Truly Declarative Service Flow Language., Web Services and Formal Methods, Third International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006, Proceedings (M. Bravetti, M. N´u˜nez, G. Zavattaro, Eds.), 4184, Springer, 2006, ISBN 3-540-38862-1.
• [2] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M.: An Abductive Framework for A-Priori Verification of Web Services, Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (A. Bossi, M. J. Maher, Eds.), ACM Press, 2006.
• [3] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M., Torroni, P.: Web Service contracting: Specification and Reasoning with SCIFF, Proceedings of the 4th European Semantic Web Conference (ESWC'07) (E. Franconi, M. Kifer, W. May, Eds.), 4519, Springer Verlag, 2007.
• [4] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Verifiable Agent Interaction in Abductive Logic Programming: the SCIFF framework, ACM Transactions on Computational Logic, 9(4), 2008, 1-43.
• [5] Alur, R., Henzinger, T. A.: A really temporal logic, Proceedings of the 30th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society, Washington, DC, USA, 1989.
• [6] Alur, R., Henzinger, T. A.: Real-time logics: complexity and expressiveness, Information and Computation, 104, 1993, 35-77.
• [7] Awad, A., Decker, G., Weske, M.: Efficient Compliance Checking Using BPMN-Q and Temporal Logic, 6th International Conference on Business Process Management (BPM 2008) (M. Dumas, M. Reichert, M.-C. Shan, Eds.), 5240, Springer Verlag, 2008.
• [8] Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools, Lectures on Concurrency and Petri Nets (J. Desel, W. Reisig, G. Rozenberg, Eds.), 3098, Springer, 2003.
• [9] Bianculli, D., Morzenti, A., Pradela, M., San Pietro, P., Spoletini, P.: Trio2Promela: a Model Checker for Temporal Metric Specifications, Proceedings of the 20th International Conference on Software Engineering, IEEE Computer Society, Washington, DC, USA, 2007.
• [10] Bürckert, H.: A resolution principle for constrained logics, Artificial Intelligence, 66, 1994, 235-271.
• [11] Casella, G., Mascardi, V.: West2East: exploiting WEb Service Technologies to Engineer Agent-based SofTware, IJAOSE, 1, 2007, 396-434.
• [12] Chesani, F.: Specification, execution and verification of interaction protocols: an approach based on computational logic, Ph.D. Thesis, University of Bologna, 2007, Available at http://amsdottorato.cib. unibo.it/392/.
• [13] Christiansen, H., Dahl, V.: HYPROLOG: A New Logic Programming Language with Assumptions and Abduction., Proceedings of ICLP 2005, 2005.
• [14] Cimatti, A., Clarke, E. M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer, 2(4), 2000, 410-425.
• [15] Clarke, E., Grumberg, O., Peled, D.: Model Checking, The MIT Press, Cambridge, Massachusetts and London, UK, 1999, ISBN 0-262-03270-8.
• [16] Delzanno, G., Podelski, A.: Model Checking in CLP, Proocedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 1999), LNCS, Springer Verlag, 1999.
• [17] Demri, S., Laroussinie, F., Schnoebelen, P.: A Parametric Analysis of the State-Explosion Problem in Model Checking, Journal of Computer and System Sciences, 72(4), 2006, 547-575.
• [18] Emerson, E. A.: Temporal and Modal Logic, in: Handbook of Theoretical Computer Science, Volume B, MIT Press, 1990, 995-1072.
• [19] Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution, ACM Transactions on Computational Logic, 2(1), 2001, 12-56.
• [20] Frühwirth, T.: Theory and Practice of Constraint Handling Rules, Journal of Logic Programming, 37(1-3), October 1998, 95-138.
• [21] Ghezzi, C., Mandrioli, D., Morzenti, A.: TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, 12(2), 1990, 107-123.
• [22] Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems, Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference (ESEC/FSE 2003), ACM, 2003.
• [23] Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive Logic Programming and Its Applications, Proceedings of the 23rd International Conference on Logic Programming (ICLP'2007), LNCS, 2007.
• [24] Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems, Proceedings of RTSS 1997, IEEE Computer Society, 1997.
• [25] Halpern, J. Y., Vardi, M. Y.: Model Checking vs. Theorem Proving: A Manifesto, In Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, 1991, 151-176.
• [26] Holzmann, G. J.: The Model Checker SPIN, IEEE Transactions on Software Engineering, 23(5), 1997, 279-295.
• [27] Jaffar, J., Maher, M.: Constraint Logic Programming: a Survey, Journal of Logic Programming, 19-20, 1994, 503-582.
• [28] Kakas, A. C., Kowalski, R. A., Toni, F.: Abductive Logic Programming, J. Log. Comput., 2(6), 1992, 719-770.
• [29] Kowalski, R. A.: Algorithm = Logic + Control, Communications of the ACM, 22(7), 1979, 424-436.
• [30] Kupferman, O., Piterman, N., Vardi, M. Y.: From Liveness to Promptness, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007) (W. Damm, H. Hermanns, Eds.), 4590, Springer, 2007.
• [31] Larsen, K. G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell, STTT, 1(1-2), 1997, 134-152.
• [32] Marques-Silva, J.: Model Checking with Boolean Satisfiability, Journal of Algorithms, 63(1-3), 2008, 3-16.
• [33] McMillan, K. L.: Interpolation and SAT-Based Model Checking, Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003) (W. A. H. Jr., F. Somenzi, Eds.), 2725, 2003.
• [34] Montali, M.: Specification and Verification of Declarative Open Interaction Models: a Logic-Based Framework, Ph.D. Thesis, University of Bologna, 2009.
• [35] Montali, M., Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Verification from declarative specifications using Logic Programming, 24th International Conference on Logic Programming (ICLP) (M. G. D. L. Banda, E. Pontelli, Eds.), number 5366 in Lecture Notes in Computer Science, Springer Verlag, Udine, Italy, December 2008.
• [36] Montali, M., Pesic, M., van der Aalst, W. M. P., Chesani, F., Mello, P., Storari, S.: Declarative Specification and Verification of Service Choreographies, ACM Transactions on the Web, accepted with minor revision, 2009.
• [37] Nalepa, G.: Proposal of Business Process and Rules Modeling with the XTT Method, Proceedings of the 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2007), 2007.
• [38] Naumovich, G., Clarke, L. A.: Classifying properties: an alternative to the safety-liveness classification, Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering: 21st Century Applications, ACM, 2000.
• [39] Pesic, M.: Constraint-Based Workflow Management Systems: Shifting Controls to Users, Ph.D. Thesis, Beta Research School for Operations Management and Logistics, Eindhoven, 2008.
• [40] Pesic, M., van der Aalst, W. M. P.: A Declarative Approach for Flexible Business Processes Management, Proceedings of the BPM 2006 Workshops, 4103, Springer, 2006.
• [41] Pesic, M., Schonenberg, H., van der Aalst, W. M. P.: DECLARE: Full Support for Loosely-Structured Processes, Proceedings of EDOC 2007, IEEE Computer Society, 2007.
• [42] Pradella, M., Morzenti, A., Pietro, P. S.: Refining Real-Time System Specifications through Bounded Modeland Satisfiability-Checking, 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 15-19 September 2008, L'Aquila, Italy, IEEE, 2008.
• [43] Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Journal of Applied Logic, 5(2), 2007, 235-251.
• [44] Rozier, K. Y., Vardi, M. Y.: LTL Satisfiability Checking, Model Checking Software. Proceedings of the 14th International SPIN Workshop, 4595, Springer Verlag, 2007.
• [45] Russo, A., Miller, R., Nuseibeh, B., Kramer, J.: An abductive Approach for Analysing Event-Based Requirements Specifications, Proceedings of ICLP 2002 (P. Stuckey, Ed.), 2401, Springer Verlag, 2002, ISBN 3-540-43930-7.
• [46] Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000) (W. A. H. Jr., S. D. Johnson, Eds.), 1954, 2000.
• [47] Torroni, P., Chesani, F., Mello, P., Yolum, P., Singh, M. P., Alberti, M., Gavanelli, M., Lamma, E.: Modeling Interactions via Commitments and Expectations, Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models (V. Dignum, Ed.), Information Science Reference, 2009.
• [48] Xanthakos, I.: Semantic Integration of Information by Abduction, Ph.D. Thesis, Imperial College London, 2003, Available at http://www.doc.ic.ac.uk/~ix98/PhD.zip.