Detecting feature interactions in Web services with model checking techniques

doi:1005-8885 (2007) 03-0108-05

Acta Metallurgica Sinica(English letters) ›› 2007, Vol. 14 ›› Issue (3): 108-112.doi: 1005-8885 (2007) 03-0108-05

• Wireless • Previous Articles Next Articles

Detecting feature interactions in Web services with model checking techniques

ZHANG Jian-yin; YANG Fang-chun; SU Sen

State Key Laboratory of Networking and Switching Technology,
Beijing University of Posts and Telecommunications, Beijing 100876, China

Received:2006-09-15 Revised:1900-01-01 Online:2007-09-30

Abstract

Abstract:

As a platform-independent software system, a Web service is designed to offer interoperability among diverse and heterogeneous applications. With the introduction of service composition in the Web service creation, various message interactions among the atomic services result in a problem resembling the feature interaction problem in the telecommunication area. This article defines the problem as feature interaction in Web services and proposes a model checking-based detection method. In the method, the Web service description is translated to the Promela language – the input language of the model checker simple promela interpreter (SPIN), and the specific properties, expressed as linear temporal logic (LTL) formulas, are formulated according to our classifi- cation of feature interaction. Then, SPIN is used to check these specific properties to detect the feature interaction in Web services.

Key words:

feature interactions; web services; model checking; detection

CLC Number:

TP393.4

ZHANG Jian-yin; YANG Fang-chun; SU Sen. Detecting feature interactions in Web services with model checking techniques[J]. Acta Metallurgica Sinica(English letters), 2007, 14(3): 108-112.

References

1. Blair L, Blair G, Pang J, et al.Feature Interaction outside a Telecom domain. Proceedings of Workshop on Feature Interaction in Composed System (ECOOP’2001), Jun 18-22, 2001, Budapest, Hungary. 2001: 15-20

2. Calder M, Kolberg M, Magill E, et al. Feature interaction: a critical review and considered forecast. International Journal of Telecommunication and Computer Networks, 2003, 41 (1): 115-141

3. Keck D O, Kuehn P J. The feature and service interaction problem in telecommunications systems: a survey. IEEE Transactions on Software Engineering, 1998, 24(10): 779-796

4. Cameron E J, Griffeth N D, Lin Yow-jian, et al. A feature interaction benchmark for IN and beyond. IEEE Communications Magazine, 1993, 31(3): 64-69

5. Amyot D, Logrippo L. Guest editorial: directions in feature interaction research. Computer Networks, 2004, 45(4): 563-567

6. Weiss M, Esfandiari B. On feature Interactions among Web Services. Proceedings of International Conference on Web Services (ICWS) , Jun 6-9, 2004, San Diego, CA, USA. Los Alamitos, CA, USA: IEEE Computer Society, 2004: 88-95

7. Wohlstadter E, Tai S, Mikalsen T, et al. GlueQoS: middleware to sweeten quality of service policy interactions. Proceedings of the 26th International Conference on Software Engineering (ICSE'04), May 23-28, 2004, Scotland, UK. Los Alamitos, CA, USA: IEEE Computer Society, 2004: 189-199

8. Joost-Pieter Katoen. Concepts, algorithms and tools for model checking. Tech Rep University of Erlangen-Numberg, 1999, 32(1)

9. Nakajima S. Model-checking verification for reliable Web service. Proceedings of Workshop on Object- Oriented Web Services (OOPSLA’02), Nov 4-8, 2000, Seattle, WA, USA. New York, NY, USA: ACM, 2002: 20

10. Nakajima S. On verifying Web Service flows. Proceedings of the Symposium on Applications and the Internet Workshops, Jan 28-Feb 1, 2002, Nara, Japan. New York, NY, USA: ACM, 2002: 223-224

11. Nakajima S. Verification of Web service flows with model-checking techniques. Proceedings of the 1st International Symposium on Cyber Worlds, Nov 6-8, 2002, Tokyo, Japan. Los Alamitos, CA, USA: IEEE Computer Society, 2002: 378-385

12. Kazhamiakin R, Pistore M, Roveri R, et al. Formal verification of requirements using SPIN: a case study on Web Services. Proceedings of 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM), Sep 28-30, 2004, Beijing, China. Los Alamitos, CA, USA: IEEE Computer Society, 2004: 406-415

13. Fu Xiang, Bultan T, Su J. Analysis of interacting BPEL Web Services. Proceeding of the Thirteenth International World Wide Web Conference(WWW’04), May 17-20, New York, NY, USA. New York, NY, USA: ACM, 2004: 621-630

14. Fu Xiang, Bultan T, Su J. WSAT: a tool for formal analysis of web services. Proceedings of the 16th International Conference on Computer Aided Verification, Jul 13-17, 2004, Boston, MA, USA. Berlin, Germany: Springer-Venlag, 2004: 510-514

15. G J Holzmann. The Model checker spin. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295

16. Andrews T, Curbera F, Dholakia H, et al., Business process execution language for Web Services. Version 1. 1, 2003, http://www-106.ibm.com/ developerworks/ library/ ws-bpel/

17. Leymann F. Web services flow language(WSFL 1.0). IBM Software Group. 2001. http://www-4.ibm.com/software/ solutions/ webservices/pdf/WSFL.pdf

Metrics

Comments

Copyright © 2020 The Journal of China Universities of Posts and Telecommunications
　 Adress: P.O. Box 231,Beijing University of Posts and Telecommunications,10 Xi Tucheng Road,Beijing 100876,P.R.China　Post Code: 100081
Tel：86-010-62282493　Fax： 86-010-62283461　E-mail: jchupt@bupt.edu.cn
Support by: Beijing Magtech Co.Ltd

[1]	Wang Wenhao , Zhao Haiying. 3D reconstruction algorithm for movable cultural relics based on salient region optimization [J]. The Journal of China Universities of Posts and Telecommunications, 2023, 30(5): 11-31.
[2]	Xu Ming, Dong Chen, Li Hanlu, Luo Qiming, Wang Lizi, Zhang Wanru, Liu Huixin. Design and implementation of unmanned aerial vehicle localization and light tracking system [J]. The Journal of China Universities of Posts and Telecommunications, 2023, 30(4): 67-74.
[3]	Li Na, Wu Yangyang, Liu Ying, Li Daxiang, Gao Jiale. Saliency guided self-attention network for pedestrian attribute recognition in surveillance scenarios [J]. The Journal of China Universities of Posts and Telecommunications, 2022, 29(5): 21-29.
[4]	Jia Wei, Gong Chao. Precise and efficient Chinese license plate recognition in the real monitoring scene of intelligent transportation system [J]. The Journal of China Universities of Posts and Telecommunications, 2022, 29(3): 1-14.
[5]	. Exploring the usefulness of light field super-resolution for object detection [J]. The Journal of China Universities of Posts and Telecommunications, 2021, 28(5): 68-81.
[6]	. Research on flame classification and recognition based on object detection and similarity fusion [J]. The Journal of China Universities of Posts and Telecommunications, 2021, 28(5): 59-67.
[7]	. Covert communication based on transmission antenna selection in the downlink communication link [J]. The Journal of China Universities of Posts and Telecommunications, 2021, 28(3): 20-27.
[8]	Cai Xingwei, Ji Wei, Qiu Ling, Liang Xiaowen. Channel puncturing based low-complexity belief propagation detection for multi-user MIMO systems [J]. The Journal of China Universities of Posts and Telecommunications, 2020, 27(6): 8-16.
[9]	Zhou You, Duan Ruifeng, Jiang Bofeng. Reduced-state noncoherent MLSD method for CPM in aeronautical telemetry [J]. The Journal of China Universities of Posts and Telecommunications, 2020, 27(4): 43-53.
[10]	Lin Jie, Liu Chuanyi, Fang Binxing. VMScan: an out-of-VM malware scanner [J]. The Journal of China Universities of Posts and Telecommunications, 2020, 27(4): 59-68.
[11]	. Polarization-based optimal detection scheme for digital self-interference cancellation in full-duplex system [J]. The Journal of China Universities of Posts and Telecommunications, 2020, 27(3): 73-82.
[12]	. LDDoS attack detection method based on wavelet decomposition and sliding windows [J]. The Journal of China Universities of Posts and Telecommunications, 2020, 27(1): 51-61.
[13]	Peng Hong, Ding Guangtai, Zhang Huiran, Hu Dongli, . Competition system for automatically evaluating edge detection algorithms based on the evolutionary game theory [J]. The Journal of China Universities of Posts and Telecommunications, 2019, 26(5): 49-59.
[14]	Pang Hao, Bu Yunyun, Wang Cong, Xiao Hui. Automatic detection of breast nodule in the ultrasound images using CNN [J]. The Journal of China Universities of Posts and Telecommunications, 2019, 26(2): 9-16.
[15]	. Segmentation of overlapping cervical nuclei based on the identification [J]. JOURNAL OF CHINA UNIVERSITIES OF POSTS AND TELECOM, 2018, 25(5): 83-92.

Detecting feature interactions in Web services with model checking techniques

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments