Guaranteeing Weak Termination in Service Discovery

• Autorzy: Wolf K. , Weinberg D. , Ott J. , Danitz R. , Stahl C.
• Języki publikacji: EN

Abstrakty

EN

A big issue in the paradigmof Service Oriented Architectures (SOA) is service discovery. Organizations publish their services via the Internet. These published services can then be automatically found and accessed by other services, meaning, the services are composed. A fundamental property of a service composition is weak termination, which guarantees the absence of deadlocks and livelocks. In principle, weak termination can be verified by inspecting the state space of the composition of (public views of) the involved services. We propose a methodology to build that state space from precomputed fragments, which are computed upon publishing a service. That way, we shift computation effort from the resource critical “find” phase to the less critical “publish” phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions. We further show the positive impact of our approach to the computational effort of service discovery.

Słowa kluczowe

EN

deadlock- and livelock freedom; service-oriented architecture (SOA); service discovery; state space reduction

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 108, nr 1/2
• Strony: 151--180
• Opis fizyczny: Bibliogr. 43 poz., tab., wykr.

Twórcy

autor

Wolf K.

autor

Weinberg D.

autor

Ott J.

autor

Danitz R.

autor

Stahl C.

• Universität Rostock 18051 Rostock, Germany,

Bibliografia

• [1] Aalst, W. M. P. v. d.: The Application of Petri Nets to Workflow Management, The Journal of Circuits, Systems and Computers, 8(1), 1998, 21-66.
• [2] Aalst, W. M. P. v. d., Lohmann, N., Massuthe, P., Stahl, C., Wolf, K.: Multiparty Contracts: Agreeing and Implementing Interorganizational Processes, Comput. J., 53(1), 2010, 90-106.
• [3] Aalst, W. M. P. v. d., Weske, M.: The P2P approach to InterorganizationalWorkflows, International Conference on Advanced Information Systems (CAiSE 2001), 2068, Springer, 2001.
• [4] Aho, A. V., Garey, M. R., Ullman, J. D.: The Transitive Reduction of a Directed Graph, SIAM J. Comput., 1(2), 1972, 131-137.
• [5] Alves, A., Arkin, A., Askary, S., Barreto, C., Bloch, B., Curbera, F., Ford,M., Goland, Y., Gu´ızar, A., Kartha, N., Liu, C. K., Khalaf, R., König, D., Marin, M., Mehta, V., Thatte, S., Rijn, D. v. d., Yendluri, P., Yiu, A.: Web Services Business Process Execution Language Version 2.0, OASIS Standard, 11 April 2007, OASIS, April 2007.
• [6] Arias-Fisteus, J., Fern´andez, L. S., Kloos, C. D.: Applying model checking to BPEL4WS business collaborations, Symposium on Applied Computing (SAC 2005) (H. Haddad, L. M. Liebrock, A. Omicini, R. L. Wainwright, Eds.), ACM, 2005.
• [7] Bravetti, M., Zavattaro, G.: Contract Based Multi-party Service Composition, Symposium on Fundamentals of Software Engineering (FSEN 2007) (F. Arbab, M. Sirjani, Eds.), 4767, Springer, 2007, ISBN 978-3-540-75697-2.
• [8] Clarke, E. M., Emerson, E. A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logics of Programs 1981, 131, Springer, 1982.
• [9] Clarke, E. M., Filkorn, T., Jha, S.: Exploiting Symmetry In Temporal Logic Model Checking, International Conference on Computer Aided Verification (CAV 1993) (C. Courcoubetis, Ed.), 697, Springer, 1993.
• [10] Clarke, E.M., Grumberg, O., Peled, D. A.: Model Checking, MIT Press, Cambridge,Massachusetts, January 2000.
• [11] Dijkman, R. M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN, Information and Software Technology, 50(12), 2008, 1281-1294.
• [12] Emerson, E. A., Sistla, A. P.: Symmetry and Model Checking, International Conference on Computer Aided Verification(CAV 1993) (C. Courcoubetis, Ed.), 697, Springer, 1993.
• [13] Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., Völzer, H.,Wolf, K.: Instantaneous Soundness Checking of Industrial Business Process Models, International Conference on Business Process Management (BPM 2009) (U. Dayal, J. Eder, J. Koehler, H. A. Reijers, Eds.), 5701, Springer, 2009.
• [14] Fernandez, J.-C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP - A Protocol Validation and Verification Toolbox, International Conference on Computer Aided Verification (CAV 1996) (R. Alur, T. A. Henzinger, Eds.), 1102, Springer, 1996.
• [15] Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods, International Workshop on Computer Aided Verification (CAV 1990) (E. M. Clarke, R. P. Kurshan, Eds.), 531, Springer, 1991.
• [16] Graf, S., Steffen, B., Lüttgen, G.: Compositional Minimisation of Finite State Systems Using Interface Specifications, Formal Asp. Comput., 8(5), 1996, 607-616.
• [17] Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency, J. ACM, 32(1), 1985, 137-161.
• [18] Juan, E. Y. T., Tsai, J. J. P., Murata, T.: Compositional Verification of Concurrent Systems Using Petri-Net-Based Condensation Rules., ACM Trans. on Programming Languages and Systems, 20(5), 1998, 917-979.
• [19] Leymann, F., Roller, D., Schmidt, M.-T.: Web services and business process management., IBM Systems Journal, 41(2), 2002, 198-211.
• [20] Lohmann, N.: A Feature-Complete Petri Net Semantics for WS-BPEL 2.0, International Workshop on Web Services and Formal Methods (WS-FM 2007) (M. Dumas, R. Heckel, Eds.), 4937, Springer, 2008.
• [21] Lohmann, N., Kopp, O., Leymann, F., Reisig, W.: Analyzing BPEL4Chor: Verification and Participant Synthesis, InternationalWorkshop on Web Services and Formal Methods (WS-FM 2007) (M. Dumas, R. Heckel, Eds.), 4937, Springer, 2008.
• [22] Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing Interacting BPEL Processes, International Conference on Business Process Management (BPM 2006) (S. Dustdar, J. L. Fiadeiro, A. Sheth, Eds.), 4102, Springer, September 2006.
• [23] Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation, Data Knowledge Engineering, 64(1), 2008, 38-54.
• [24] Lohmann, N., Massuthe, P., Wolf, K.: Operating Guidelines for Finite-State Services, International Conference on Applications and Theory of Petri Nets (ICATPN 2007) (J. Kleijn, A. Yakovlev, Eds.), 4546, Springer, 2007.
• [25] Malik, R., Streader, D., Reeves, S.: Conflicts and Fair Testing, Int. J. Found. Comput. Sci., 17(4), 2006, 797-814.
• [26] Milner, R.: Communication and Concurrency, Prentice-Hall, Inc., 1989.
• [27] Mooij, A. J., Stahl, C., Voorhoeve,M.: Relating fair testing and accordance for service replaceability, Journal of Logic and Algebraic Programming, 79(3-5), 2010, 233 - 244, ISSN 1567-8326.
• [28] Murata, T.: Petri Nets: Properties, Analysis and Applications, Proceedings of the IEEE, 77(4), April 1989, 541-580.
• [29] OMG: Business Process Model and Notation (BPMN), FTF Beta 1 for Version 2.0, Object Management Group, 2009.
• [30] Papazoglou,M. P.: Web Services: Principles and Technology, Pearson - Prentice Hall, Essex, July 2007.
• [31] Park, D.: Concurrency and Automata on Infinite Sequences, Theoretical Computer Science (P. Deussen, Ed.), 104, Springer, 1981.
• [32] Peled, D.: All from One, One for All: on Model Checking Using Representatives, International Conference on Computer Aided Verification (CAV 1993) (C. Courcoubetis, Ed.), 697, Springer, 1993.
• [33] Puhakka,A., Valmari, A.: Weakest-CongruenceResults for Livelock-Preserving Equivalences., International Conference on Concurrency Theory (CONCUR 1999) (J. C.M. Baeten, S.Mauw, Eds.), 1664, Springer, 1999.
• [34] Rensink, A., Vogler,W.: Fair testing, Inf. Comput., 205(2), 2007, 125-198.
• [35] Schmidt, K.: Stubborn Sets for Standard Properties, International Conference on Application and Theory of Petri Nets (ICATPN 1999) (S. Donatelli, H. C. M. Kleijn, Eds.), 1639, Springer, 1999.
• [36] Schmidt, K.: LoLA: A Low Level Analyser, International Conference on Application and Theory of Petri Nets (ICATPN 2000) (M. Nielsen, D. Simpson, Eds.), 1825, Springer, 2000.
• [37] Valmari, A.: A StubbornAttack On State Explosion, InternationalWorkshop on Computer Aided Verification (CAV 1990) (E. M. Clarke, R. P. Kurshan, Eds.), 531, Springer, 1991.
• [38] Valmari, A.: TheWeakest Deadlock-Preserving Congruence., Inf. Process. Lett., 53(6), 1995, 341-346.
• [39] Valmari, A.: The State Explosion Problem, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets (W. Reisig, G. Rozenberg, Eds.), 1491, Springer, 1998.
• [40] Weinberg, D.: Efficient Controllability Analysis of Open Nets, InternationalWorkshop on Web Services and Formal Methods (WS-FM 2008) (R. Bruni, K. Wolf, Eds.), 5387, Springer-Verlag, September 2008.
• [41] Wolf, K.: DoesMy Service Have Partners?, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2, 2009, 152-171.
• [42] Wolf, K., Stahl, C., Ott, J., Danitz, R.: Verifying Livelock Freedom in an SOA Scenario, International Conference on Application of Concurrency to System Design (ACSD 2009) (S. Edwards, W. Vogler, Eds.), IEEE Computer Society, July 2009.
• [43] Wombacher, A., Mahleko, B., Neuhold, E. J.: IPSI-PF - A business process matchmaking engine based on annotated finite state automata, Inf. Syst. E-Business Management, 3(2), 2005, 127-150