Abstract
Choreography analysis is a crucial problem in concurrent and distributed system development. A choreography specifies the desired ordering of message exchanges among the components of a system. The realizability of a choreography amounts to determining the existence of components whose communication behavior conforms to the given choreography. The realizability problem has been shown to be decidable. In this paper, we investigate the repairability of un-realizable choreographies, where the goal is to identify a set of changes to a given un-realizable choreography that will make it realizable. We present a technique for automatically repairing un-realizable choreographies and provide formal guarantees of correctness and termination. We demonstrate the viability of our technique by applying it to several representative unrealizable choreographies from Singularity OS channel contracts and Web services.
References
[1]
Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. In: Proceedings of 28th International Colloquium on Automata, Languages, and Programming, pp. 797---808 2001
[2]
Armstrong, J.: Getting Erlang to talk to the outside world. In: Proceedings of ACM SIGPLAN Workshop on Erlang, pp. 64---72 2002
[3]
Autili, M., Di Ruscio, D., Di Salle, A., Inverardi, P., Tivoli, M.: A model-based synthesis process for choreography realizability enforcement. In: Cortellessa, V., Varró, D. eds. FASE 2013 ETAPS 2013. LNCS, vol. 7793, pp. 37---52. Springer, Heidelberg 2013
[4]
Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2012
[5]
Bultan, T., Fu, X.: Specification of realizable service conversations using collaboration diagrams. Serv. Oriented Comput. Appl. 21, 27---39 2008
[6]
Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. ed. Programming Languages and Systems. LNCS, vol. 7211, pp. 194---213. Springer, Heidelberg 2012
[7]
Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. In: Ibarra, O.H., Dang, Z. eds. CIAA 2003. LNCS, vol. 2759, pp. 188---200. Springer, Heidelberg 2003
[8]
Güdemann, M., Salaün, G., Ouederni, M.: Counterexample guided synthesis of monitors for realizability enforcement. In: Chakraborty, S., Mukund, M. eds. ATVA 2012. LNCS, vol. 7561, pp. 238---253. Springer, Heidelberg 2012
[9]
Hallé, S., Bultan, T.: Realizability analysis for message-based interactions using shared-state projections. In: SIGSOFT Foundations of Software Engineering 2010
[10]
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of Symposium Principles of Programming Languages 2008
[11]
Hunt, G.C., Larus, J.R.: Singularity: rethinking the software stack. Operating Syst. Rev. 412, 37---49 2007
[12]
Kumaran, S., Nandi, P., Hanson, J., Heath, T., Patnaik, Y.: Conversational browser. IBM Techreport 2004
[13]
Lanese, I., Montesi, F., Zavattaro, G.: Amending choreographies. In: Automated Specification and Verification of Web Systems 2013
[14]
Lohmann, N., Wolf, K.: Realizability is controllability. In: Laneve, C., Su, J. eds. WS-FM 2009. LNCS, vol. 6194, pp. 110---127. Springer, Heidelberg 2010
[15]
Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the theoretical foundation of choreography. In: Proceedings of Conference on World Wide Web 2007
[16]
Singularity design note 5: Channel contracts. singularity rdk documentation v1.1 2004. http://www.codeplex.com/singularity
[17]
Stengel, Z., Bultan, T.: Analyzing singularity channel contracts. In: Proceedings of 18th International Symposium on Software Testing and Analysis ISSTA, pp. 13---24 2009
[18]
Web Service Choreography Description Language WS-CDL 2005. http://www.w3.org/TR/ws-cdl-10/
[19]
Yoon, Y., Ye, C., Jacobsen, H.-A.: A distributed framework for reliable and efficient service choreographies. In: Proceedings of the 20th International Conference on World wide web, WWW 2011, pp. 785---794. ACM 2011
Recommendations
Towards automated choreography of Web services using planning in large scale service repositories
Automated composition of Web services is becoming a prominent paradigm for implementing and delivering distributed applications. A composed service can be described either by orchestration or choreography. Service orchestration has a centralized ...
Service Choreography: Present and Future
SCC '14: Proceedings of the 2014 IEEE International Conference on Services ComputingService oriented architecture is widely adopted, accepted and appreciated for both horizontal and vertical integration of enterprise applications. The success is hugely aided by web service composition, which is a temporal collaboration of independent ...
Web services choreography validation
In this paper, we propose an approach to simulation and validation of Web services choreography described by WS-CDL. Simulation of Web services choreography is important to analyze and test the choreography model written by SOA designers. On the other ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 02 April 2016
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in