Behavior-Consistent Service Substitutions in Dynamic Environments

doi:10.1007/s12204-014-1472-z

Abstract

Abstract: In this paper, a novel approach for service substitutions based on the service type in terms of its interface type and behavior semantics is proposed. In order to analyze and verify behavior-consistent service substitutions in dynamic environments, we first present a formal language to describe services from control-flow perspective, then introduce a type and effect system to infer conservative approximations of all possible behaviors of these services. The service behaviors are represented by concurrent behavior expressions (CBEs). Built upon the interpretation of CBEs, behavior-consistent service substitutions are defined and analyzed by subtyping technology. The correctness of the analysis approach is guaranteed by type safety theorem, which is mechanically proved in the Coq proof assistant. Finally, applications in web services show that our method is effective and feasible.

Key words: behavior consistency| concurrent regular expressions| subtyping technology| type and effect systems|service substitutions

摘要： In this paper, a novel approach for service substitutions based on the service type in terms of its interface type and behavior semantics is proposed. In order to analyze and verify behavior-consistent service substitutions in dynamic environments, we first present a formal language to describe services from control-flow perspective, then introduce a type and effect system to infer conservative approximations of all possible behaviors of these services. The service behaviors are represented by concurrent behavior expressions (CBEs). Built upon the interpretation of CBEs, behavior-consistent service substitutions are defined and analyzed by subtyping technology. The correctness of the analysis approach is guaranteed by type safety theorem, which is mechanically proved in the Coq proof assistant. Finally, applications in web services show that our method is effective and feasible.

关键词: behavior consistency| concurrent regular expressions| subtyping technology| type and effect systems|service substitutions

CLC Number:

TP 301.2

CHEN Jun-qing* (陈俊清), HUANG Lin-peng (黄林鹏), YU Cheng-yuan (于程远). Behavior-Consistent Service Substitutions in Dynamic Environments[J]. Journal of shanghai Jiaotong University (Science), 2014, 19(1): 17-27.

References

[1] Papazoglou M P. Service-oriented computing: Concepts,characteristics and directions [C]// Proceedings of the 4th International Conference on Web Information Systems Engineering. Tilburg University, Netherlands:IEEE, 2003: 3-12.
[2] Bartoletti M, Degano P, Ferrari G L, et al.Semantics-based design for secure web services [J].IEEE Transactions on Software Engineering, 2008,34(1): 33-49.
[3] Athanasopoulos D, Zarras A, Issarny V. Service substitution revisited [C]// Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering. Auckland: IEEE, 2009: 555-559.
[4] Fredj M, Georgantas N, Issarny V, et al. Dynamic service substitution in service-oriented architectures[C]// Proceedings of the IEEE Congress on Services.Honolulu, HI: IEEE, 2008: 101-104.
[5] Bartoletti M, Degano P, Ferrari G L. Planning and verifying service composition [J]. Journal of Computer Security, 2009, 17(5): 799-837.
[6] Pianwattanaphon R, Senivongse T. Compatibility by service type model for automatic web services substitution [C]// Proceedings of the 9th International Conference on Advanced Communication Technology.Gangwon-Do: IEEE, 2007: 76-81.
[7] Santhanam G R, Basu S, Honavar V. Web service substitution based on preferences over non-functional attributes [C]//Proceedings of the 2009 IEEE International Conference on Services Computing. Bangalore:IEEE, 2009: 210-217.
[8] Ibrahim N, Frdric F, Frnot S. Semantic service substitution in pervasive environments [J]. International Journal of Services, Economics and Management(IJSEM), 2011, 8(1): 1-24.
[9] Berardi D, Calvanese D, Giacomo G D, et al. Automatic service composition based on behavioral descriptions[J]. International Journal of Cooperative Information Systems, 2005, 14(1): 333-376.
[10] Berardi D, Cheikh F, Giacomo G D, et al. Automatic service composition via simulation [J]. International Journal of Foundations of Computer Science,2008, 19(2): 429-451.
[11] Ferrara A. Web services: A process algebra approach[C]// Proceedings of the 2nd International Conference on Service Oriented Computing. NewYork, US:ACM, 2004: 242-251.
[12] Brogi A, Canal C, Pimentel E, et al. Formalizing web service choreographies [J]. Electronic Notes in Theoretical Computer Science, 2004, 10(5): 73-94.
[13] Brogi A, Corfini S. Behaviour-aware discovery of web service compositions [J]. International Journal of Web Services Research, 2007, 4(3): 1-25.
[14] Aalst W, Marlon D, Chun O, et al. Conformance checking of service behavior [J]. ACM Transactions on Internet Technology, 2008, 8(3): 1-13.
[15] Christian S. Service substitution: A behavioral approach based on petri nets [D]. Berlijn, Duitsland:Technische Universiteit Eindhoven, 2009.
[16] Bonchi F, Brogi A, Corfini S, et al. A net-based approach to web services publication and replaceability[J]. Fundamenta Informaticae, 2009, 94(3): 305-330.
[17] Skalka C, Smith S, Horn D V. Types and trace effects of higher order programs [J]. Journal of Functional Programming, 2008, 18(2): 179-249.
[18] Fabrizio M, Claudio G, Gianluigi Z. Serviceoriented programming with Jolie [M]. New York, USA:Springer, 2014: 81-107.
[19] Dalla P M, Lanese I, Mauro J, et al. Graceful interruption of request-response service interactions[C]// Proceedings of the International Conference on Service-Oriented Computing. Paphos, Cyprus:Springer, 2011: 590-600.
[20] Baldoni M, Baroglio C, Marengo E. Commiment-based protocols with behavioral rules and correctness properties of MAS [C]//Proceedings of the 8th International Workshop, Declarative Agent Languages and Technologies VIII. Toronto, Canada:Springer, 2011: 60-77.
[21] Beyer D, Chakrabarti A, Henzinger T A. Web service interfaces [C]// Proceedings of the 14th International Conference on World Wide Web. Chiba, Japan:ACM, 2005: 148-159.
[22] Pathak J, Basu S, Honavar V. On context-sensitive substitutability of web services [C]// Proceedings of the 5th IEEE International Conference on Web Services.Honolulu, USA: IEEE, 2007: 192-199.
[23] Baresi L, Ghezzi C, Guinea S. Smart monitors for composed services [C]// Proceedings of the 2nd International Conference on Service Oriented Computing.New York, USA: ACM, 2004: 193-202.
[24] Garg V K, Ragunath M T. Concurrent regular expressions and their relationship to Petri nets [J]. Theoretical Computer Science, 1992, 96(2): 285-304.
[25] Aydemir B, Chargueraud A, Pierce B C, et al.Engineering formal metatheory [C]//in Proceedings of the 35th Annual ACM Sigplan-Sigact Symposium on Principles of Programming Languages. San Francisco,USA: ACM, 2008: 3-15.