Pascal Poizat
ABSTRACT
Choreographies allow business and service architects to specify with a global perspective the requirements of applications built over distributed and interacting software entities. While being a standard for the abstract specification of business workflows and collaboration between services, the Business Process Modeling Notation (BPMN) has only been recently extended into BPMN 2.0 to support an interaction model of choreography, which, as opposed to interconnected interface models, is better suited to top-down development processes. An important issue with choreographies is real-izability, i.e., whether peers obtained via projection from a choreography interact as prescribed in the choreography requirements. In this work, we propose a realizability checking approach for BPMN 2.0 choreographies. Our approach is formally grounded on a model transformation into the LOTOS NT process algebra and the use of equivalence checking. It is also completely tool-supported through interaction with the Eclipse BPMN 2.0 editor and the CADP process algebraic toolbox.
- R. Alur, K. Etessami, and M. Yannakakis. Inference of Message Sequence Charts. IEEE Transactions on Software Engineering, 29(7): 623--633, 2003. Google Scholar
Digital Library
- R. Alur, K. Etessami, and M. Yannakakis. Realizability and Verification of MSC Graphs. Theoretical Computer Science, 331(1): 97--114, 2005. Google ScholarDigital Library
- S. Basu and T. Bultan. Choreography Conformance via Synchronizability. In Proc. of WWW'11, pages 795--804. ACM Press, 2011. Google ScholarDigital Library
- M. Bozkurt, M. Harman, and Y. Hassoun. Testing Web Services: A Survey. Technical report, King's College London, 2010.Google Scholar
- D. Brand and P. Zafiropulo. On Communicating Finite-State Machines. J. ACM, 30(2): 323--342, 1983. Google ScholarDigital Library
- M. Bravetti and G. Zavattaro. Contract Compliance and Choreography Conformance in the Presence of Message Queues. In Proc. of WS-FM'08, volume 5387 of LNCS, pages 37--54. Springer, 2009. Google ScholarDigital Library
- T. Bultan and X. Fu. Specification of Realizable Service Conversations using Collaboration Diagrams. Service Oriented Computing and Applications, 2(1): 27--39, 2008.Google ScholarCross Ref
- N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro. Choreography and Orchestration Conformance for System Design. In Proc. of Coordination'06, volume 4038 of LNCS, pages 63--81. Springer, 2006. Google ScholarDigital Library
- M. Carbone, K. Honda, and N. Yoshida. Structured Communication-Centred Programming for Web Services. In Proc. of ESOP'07, volume 4421 of LNCS, pages 2--17. Springer, 2007. Google ScholarDigital Library
- D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, V. Powazny, F. Lang, W. Serwe, and G. Smeding. Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4). INRIA/VASY, 149 pages, 2011.Google Scholar
- P. Crouzen and F. Lang. Smart Reduction. In Proc. of FASE'11, volume 6603 of LNCS, pages 111--126. Springer, 2011. Google ScholarDigital Library
- G. Decker, O. Kopp, and A. Barros. An Introduction to Service Choreographies. Information Technology, 50(2): 122--127, 2008.Google Scholar
- G. Decker and M. Weske. Local Enforceability in Interaction Petri Nets. In Proc. of BPM'07, volume 4714 of LNCS, pages 305--319. Springer, 2007. Google ScholarDigital Library
- G. Decker and M. Weske. Interaction-centric Modeling of Process Choreographies. Information Systems, 36(2): 292--312, 2011. Google ScholarDigital Library
- X. Fu, T. Bultan, and J. Su. Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services. Theoretical Computer Science, 328(1--2): 19--37, 2004. Google ScholarDigital Library
- H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In Proc. of TACAS'11, volume 6605 of LNCS, pages 372--387. Springer, 2011. Google ScholarDigital Library
- ISO. LOTOS --- A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Technical Report 8807, ISO, 1989.Google Scholar
- R. Kazhamiakin and M. Pistore. Analysis of Realizability Conditions for Web Service Choreographies. In Proc. of FORTE'06, volume 4229 of LNCS, pages 61--76. Springer, 2006. Google ScholarDigital Library
- J. Li, H. Zhu, and G. Pu. Conformance Validation between Choreography and Orchestration. In Proc. of TASE'07, pages 473--482. IEEE Computer Society, 2007. Google ScholarDigital Library
- N. Lohmann and K. Wolf. Realizability Is Controllability. In Proc. of WS-FM'09, volume 6194 of LNCS, pages 110--127. Springer, 2010. Google ScholarDigital Library
- A. Marconi and M. Pistore. Synthesis and Composition of Web Services. In Proc. of SFM'09, volume 5569 of LNCS, pages 89--157. Springer, 2009. Google ScholarDigital Library
- R. Mateescu, P. Poizat, and G. Salaün. Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques. In Proc. of ICSOC'08, volume 5364 of LNCS, pages 84--99. Springer, 2008. Google ScholarDigital Library
- R. Mateescu and M. Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Sci. Comput. Programming, 46(3): 255--281, 2003. Google ScholarDigital Library
- R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. Google ScholarDigital Library
- OMG. Business Process Model and Notation (BPMN) - Version 2.0. January 2011.Google Scholar
- Z. Qiu, X. Zhao, C. Cai, and H. Yang. Towards the Theoretical Foundation of Choreography. In Proc. of WWW'07, pages 973--982. ACM Press, 2007. Google ScholarDigital Library
- G. Salaün and T. Bultan. Realizability of Choreographies using Process Algebra Encodings. In Proc. of IFM'09, volume 5423 of LNCS, pages 167--182. Springer, 2009. Google ScholarDigital Library
- S. Uchitel, J. Kramer, and J. Magee. Incremental Elaboration of Scenario-based Specifications and Behavior Models using Implied Scenarios. ACM Transactions on Software Engineering and Methodology, 13(1): 37--85, 2004. Google ScholarDigital Library
Recommendations
Evaluating the appropriateness of the BPMN 2.0 standard for modeling service choreographies: using an extended quality framework
The concept of choreography has emerged over the past years as a foundational concept for capturing and managing collaborative business processes. The latest version of the Business Process Modeling Notation (BPMN 2.0) adopts choreography as a first-...
Realizability of Choreographies Using Process Algebra Encodings
Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and ...
Comments