Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Mobile Networks and Applications
Published in: Mobile Networks and Applications 4/2021

18-01-2020

An Efficient Bounded Model Checking Approach for Web Service Composition

Authors: Yuanzhang Li, Dongyan Ma, Chen Liu, Wencong Han, Hongwei Jiang, Jingjing Hu

Published in: Mobile Networks and Applications | Issue 4/2021

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

With the development of service-oriented architecture, Web service composition has become more important for mitigating potential security vulnerabilities. When the scale of services increases, it will lead to the problem of state explosion. Symbolic model checking is a common method used to alleviate the problem of state-space explosion. However, for a large Web service composition system, the number of services is large, and the corresponding state space may exceed the magnitude of the symbolic model checking that can verify it. As it alleviates the state-space explosion problem, bounded model checking was utilized in the present study to verify the properties of the service composition system. Bounded model checking searches for bounded counterexamples in a limited local space and reduces the state space. This study verifies the composition of semantic Web services described by OWL-S and proposes a timed service model (TSM) to formally model the service composition system. Furthermore, the auto-mapping relationship between the OWL-S service description and the model is established. For more efficient verification, this study uses SMT-based (SMT: satisfiability modulo theory) encoding in the TSM. Finally, a public emergency service composition system was built to verify the proposed model and the efficiency of the proposed algorithm.
previous article A Timestamp-Regulating VoLTE Covert Channel against Statistical Analysis
next article PRIA: a Multi-source Recognition Method Based on Partial Observation in SIR Model

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Show more products
Literature
1.
Chen X, Li J, Ma J, Weng J, Lou W (2016) Verifiable computation over large database with incremental updates. IEEE Trans Comput 65(10):3184–3195MathSciNetCrossRef
2.
3.
Wang K, Zhang D, Li Y, Zhang R, Lin L (2016) Cost-effective active learning for deep image classification. IEEE Trans Circ Syst Vid 27(12):2591–2600CrossRef
4.
Huang Y, Li W, Liang Z, Xue Y, Wang X (2017) Efficient business process consolidation: combining topic features with structure matching. Soft Comput 22(2):645–657CrossRef
5.
Liang C, Tan Y, Zhang X, Wang X, Zheng J, Zhang Q (2018) Building packet length covert channel over mobile VoIP traffics. J Netw Comput Appl 118:144–153CrossRef
6.
Tan Y, Xue Y, Liang C, Zheng J, Zhang Q, Zheng J, Li Y (2018) A root privilege management scheme with revocable authorization for android devices. J Netw Comput Appl 107(4):69–82CrossRef
7.
Xue Y, Tan Y, Liang C, Li Y, Zheng J, Zhang Q (2018) RootAgency: a digital signature-based root privilege management agency for cloud terminal devices. Inform Sci 444:36–50MathSciNetCrossRef
8.
Guan Z, Li J, Wu L, Zhang Y, Wu J, Du X (2017) Achieving efficient and secure data acquisition for cloud-supported internet of things in smart grid. IEEE Internet Things 4(6):1934–1944CrossRef
9.
Sun Z, Zhang Q, Li Y, Tan Y (2016) Dppdl: a dynamic partial-parallel data layout for green video surveillance storage. IEEE Trans Circ Syst Vid 28(1):193–205
10.
He J, Zhang Z, Li M, Zhu L, Hu J (2019) Provable data integrity of cloud service with enhanced security in the internet of things. IEEE Access 7:6226–6239CrossRef
11.
Fan L, Lei X, Yang N, Duong T, Karagiannidis G (2017) Secrecy cooperative networks with outdated relay selection over correlated fading channels. IEEE Trans Veh Technol 66(8):7599–7603CrossRef
12.
Jiang W, Wang G, Bhuiyan MZA, Wu J (2016) Understanding graph-based trust evaluation in online social networks: methodologies and challenges. ACM Comput Surv 49(1):1–35CrossRef
13.
Zhang X, Zhu L, Wang X, Zhang C, Zhu H, Tan Y (2019) A packet-reordering covert channel over VoLTE voice and video traffics. J Netw Comput Appl 126:29–38CrossRef
14.
Tan Y, Zhang X, Sharif K, Liang C, Zhang Q, Li Y (2018) Covert timing channels for IoT over mobile networks. IEEE Wirel Commun 25(6):38–44CrossRef
15.
16.
Li Y, Hu J, Wu Z, Liu C, Peng F, Zhang Y (2018) Research on QoS service composition based on coevolutionary genetic algorithm. Soft Comput 22(23):7865–7874CrossRef
17.
18.
Liang C, Wang X, Zhang X, Zhang Y, Sharif K, Tan Y (2018) A payload-dependent packet rearranging covert channel for mobile VoIP traffic. Inform Sci 465C:162–173CrossRef
19.
Guan Z, Zhang Y, Wu L, Wu J, Ma Y, Hu J (2019) APPA: an anonymous and privacy preserving data aggregation scheme for fog-enhanced IoT. J Netw Comput Appl 125:82–92CrossRef
20.
21.
Li Y, Wang G, Nie L, Wang Q, Tan W (2018) Distance metric optimization driven convolutional neural network for age invariant face recognition. Pattern Recogn 75:51–62CrossRef
22.
Elmisery A, Sertovic M, Gupta B (2017) Cognitive privacy middleware for deep learning mashup in environmental IoT. IEEE Access 6:8029–8041CrossRef
23.
24.
Fan L, Lei X, Yang N, Duong T, Karagiannidis G (2016) Secure multiple amplify-and-forward relaying with cochannel interference. IEEE J Selected Topics Signal Proc 10(8):1494–1505CrossRef
25.
Lai X, Zou W, Xie D, Li X, Fan L (2017) DF relaying networks with randomly distributed interferers. IEEE Access 5:18909–18917CrossRef
26.
Hu J, Liu L, Zhang C, He J, Hu C (2018) Hybrid recommendation algorithm based on latent factor model and PersonalRank. J Internet Technol 19(3):919–926
27.
28.
Rodriguez-Mier P, Pedrinaci C, Lama M, Mucientes M (2016) An integrated semantic web service discovery and composition framework. IEEE Trans Serv Comput 9(4):537–550CrossRef
29.
Omid M (2017) Context-aware web service composition based on AI planning. Appl Artif Intell 31(1):23–43
30.
Bourouis A, Klai K, Hadj-Alouane NB, Touati YE (2017) On the verification of opacity in web services and their composition. IEEE Trans Serv Comput 10(1):66–79CrossRef
31.
Shunhui J, Bixin L, Dong Q (2016) Incremental verification of evolving BPEL-based web composite service. Chinese J Electron 25(1):6–12CrossRef
32.
Rodriguez G, Soria A, Campo M (2016) AI-based web service composition: a review. IETE Tech Rev 33(4):378–385CrossRef
33.
Zheng H (2017) Modeling and analyzing web services combination by using an innovative timed probabilistic priced process algebra. Agro Food Ind Hi Tech 28(3):1483–1485
34.
Van Benthem J, Van Eijck J, Gattinger M, Su K (2018) Symbolic model checking for dynamic epistemic logic — s5 and beyond. J Log Comput 28(2):367–402MathSciNetCrossRef
35.
Liu W, Wang R, Fu X, Wang J, Dong W, Mao X (2013) Counterexample-preserving reduction for symbolic model checking. J Appl Math 2014(1):249–266MathSciNetMATH
36.
Luo X, Wu L, Chen Q, Li H, Zheng L, Chen Z (2018) Symbolic model checking for discrete real-time systems. Sci China Inform Sci 61(5)
37.
Kwon Y, Kim E (2015) Bounded model checking of hybrid systems for control. IEEE Trans Automat Control 60(11):2961–2976MathSciNetCrossRef
38.
Krings S, Leuschel M (2018) Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci Comput Program 158:41–63CrossRef
39.
Chen Z, Xu Z, Du J, Mei M, Guo J (2017) Efficient encoding for bounded model checking of timed automata. IEEJ Trans Electr Electr 12(5):710–720CrossRef
40.
Monteiro F, Alves E, Silva I, Ismail H, Cordeiro L, de Lima B (2018) ESBMC-GPU a context-bounded model checking tool to verify CUDA programs. Sci Comput Program 152:63–69CrossRef
41.
Hu J, Chen X, Zhang C (2016) Proactive service selection based on acquaintance model and LS-SVM. Neurocomputing 211:60–65CrossRef
42.
Deng Z, Zhang J, He T (2017) Automatic combination technology of fuzzy CPN for OWL-S Web services in supercomputing cloud platform. Int J Pattern Recogn 31(7)
43.
Jia H, Ding S, Du M, Xue Y (2016) Approximate normalized cuts without Eigen-decomposition. Inform Sci 374:135–150CrossRef
44.
Woźna-Szcześniak B (2016) SAT-based bounded model checking for weighted deontic interpreted systems. Fund Inform 143(1–2):173–205MathSciNetMATH
45.
Zhang H, Li G, Sun D, Lu Y, Hsu C (2017) Verifying cooperative software: a SMT-based bounded model checking approach for deterministic scheduler. J Syst Architect 81:7–16CrossRef
Metadata
Title
An Efficient Bounded Model Checking Approach for Web Service Composition
Authors
Yuanzhang Li
Dongyan Ma
Chen Liu
Wencong Han
Hongwei Jiang
Jingjing Hu
Publication date
18-01-2020
Publisher
Springer US
Published in
Mobile Networks and Applications / Issue 4/2021
Print ISSN: 1383-469X
Electronic ISSN: 1572-8153
DOI
https://doi.org/10.1007/s11036-019-01486-2

Other articles of this Issue 4/2021

Mobile Networks and Applications 4/2021 Go to the issue

OriginalPaper

A Confidence-Guided Evaluation for Log Parsers Inner Quality

OriginalPaper

Malware Detection Based on Multi-level and Dynamic Multi-feature Using Ensemble Learning at Hypervisor

OriginalPaper

PRIA: a Multi-source Recognition Method Based on Partial Observation in SIR Model

OriginalPaper

A Privacy-preserving Fuzzy Search Scheme Supporting Logic Query over Encrypted Cloud Data

EditorialNotes

Convergence of 5G Technologies, Artificial Intelligence and Cybersecurity of Networked Societies for the Cities of Tomorrow

OriginalPaper

Security Assessment for Interdependent Heterogeneous Cyber Physical Systems