{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,14]],"date-time":"2025-11-14T17:28:06Z","timestamp":1763141286777,"version":"3.37.3"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2020,1,18]],"date-time":"2020-01-18T00:00:00Z","timestamp":1579305600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,18]],"date-time":"2020-01-18T00:00:00Z","timestamp":1579305600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772070"],"award-info":[{"award-number":["61772070"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"State Key Lab of Digital ManuNational Key R&D Program of China","award":["2018YFB1004402"],"award-info":[{"award-number":["2018YFB1004402"]}]},{"name":"Beijing Municipal Natural Science Foundation","award":["4172053"],"award-info":[{"award-number":["4172053"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s11036-019-01486-2","type":"journal-article","created":{"date-parts":[[2020,1,18]],"date-time":"2020-01-18T18:02:10Z","timestamp":1579370530000},"page":"1503-1513","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An Efficient Bounded Model Checking Approach for Web Service Composition"],"prefix":"10.1007","volume":"26","author":[{"given":"Yuanzhang","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dongyan","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chen","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wencong","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongwei","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3220-621X","authenticated-orcid":false,"given":"Jingjing","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,1,18]]},"reference":[{"issue":"10","key":"1486_CR1","doi-asserted-by":"publisher","first-page":"3184","DOI":"10.1109\/TC.2015.2512870","volume":"65","author":"X Chen","year":"2016","unstructured":"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\u20133195","journal-title":"IEEE Trans Comput"},{"doi-asserted-by":"publisher","unstructured":"Meng W, Tischhauser E, Wang Q, Wang Y, Han J (2018) When intrusion detection meets blockchain technology: a review. IEEE Access. https:\/\/doi.org\/10.1109\/ACCESS.2018.2799854","key":"1486_CR2","DOI":"10.1109\/ACCESS.2018.2799854"},{"issue":"12","key":"1486_CR3","doi-asserted-by":"publisher","first-page":"2591","DOI":"10.1109\/TCSVT.2016.2589879","volume":"27","author":"K Wang","year":"2016","unstructured":"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\u20132600","journal-title":"IEEE Trans Circ Syst Vid"},{"issue":"2","key":"1486_CR4","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/s00500-016-2364-y","volume":"22","author":"Y Huang","year":"2017","unstructured":"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\u2013657","journal-title":"Soft Comput"},{"key":"1486_CR5","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jnca.2018.06.012","volume":"118","author":"C Liang","year":"2018","unstructured":"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\u2013153","journal-title":"J Netw Comput Appl"},{"issue":"4","key":"1486_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/j.jnca.2018.01.011","volume":"107","author":"Y Tan","year":"2018","unstructured":"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\u201382","journal-title":"J Netw Comput Appl"},{"key":"1486_CR7","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.ins.2018.02.069","volume":"444","author":"Y Xue","year":"2018","unstructured":"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\u201350","journal-title":"Inform Sci"},{"issue":"6","key":"1486_CR8","doi-asserted-by":"publisher","first-page":"1934","DOI":"10.1109\/JIOT.2017.2690522","volume":"4","author":"Z Guan","year":"2017","unstructured":"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\u20131944","journal-title":"IEEE Internet Things"},{"issue":"1","key":"1486_CR9","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1109\/TCSVT.2016.2605045","volume":"28","author":"Z Sun","year":"2016","unstructured":"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\u2013205","journal-title":"IEEE Trans Circ Syst Vid"},{"key":"1486_CR10","doi-asserted-by":"publisher","first-page":"6226","DOI":"10.1109\/ACCESS.2018.2889296","volume":"7","author":"J He","year":"2019","unstructured":"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\u20136239","journal-title":"IEEE Access"},{"issue":"8","key":"1486_CR11","doi-asserted-by":"publisher","first-page":"7599","DOI":"10.1109\/TVT.2017.2669240","volume":"66","author":"L Fan","year":"2017","unstructured":"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\u20137603","journal-title":"IEEE Trans Veh Technol"},{"issue":"1","key":"1486_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2906151","volume":"49","author":"W Jiang","year":"2016","unstructured":"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\u201335","journal-title":"ACM Comput Surv"},{"key":"1486_CR13","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.jnca.2018.11.001","volume":"126","author":"X Zhang","year":"2019","unstructured":"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\u201338","journal-title":"J Netw Comput Appl"},{"issue":"6","key":"1486_CR14","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MWC.2017.1800062","volume":"25","author":"Y Tan","year":"2018","unstructured":"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\u201344","journal-title":"IEEE Wirel Commun"},{"doi-asserted-by":"publisher","unstructured":"Wu J, Dong M, Ota K, Li J, Guan Z (2018) FCSS: Fog-computing-based content-aware filtering for security services in information-centric social networks. IEEE Trans Emerging Topics Comput. https:\/\/doi.org\/10.1109\/TETC.2017.2747158","key":"1486_CR15","DOI":"10.1109\/TETC.2017.2747158"},{"issue":"23","key":"1486_CR16","doi-asserted-by":"publisher","first-page":"7865","DOI":"10.1007\/s00500-018-3510-5","volume":"22","author":"Y Li","year":"2018","unstructured":"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\u20137874","journal-title":"Soft Comput"},{"key":"1486_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-018-9451-y","volume":"62","author":"Z Guan","year":"2019","unstructured":"Guan Z, Zhang Y, Zhu L, Wu L, Yu S (2019) EFFECT: an efficient flexible privacy-preserving data aggregation scheme with authentication in smart grid. Sci China Inf Sci 62:1\u201314. https:\/\/doi.org\/10.1007\/s11432-018-9451-y","journal-title":"Sci China Inf Sci"},{"key":"1486_CR18","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.ins.2018.07.011","volume":"465C","author":"C Liang","year":"2018","unstructured":"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\u2013173","journal-title":"Inform Sci"},{"key":"1486_CR19","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.jnca.2018.09.019","volume":"125","author":"Z Guan","year":"2019","unstructured":"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\u201392","journal-title":"J Netw Comput Appl"},{"doi-asserted-by":"publisher","unstructured":"Zhang Q, Gong H, Zhang X, Liang C, Tan Y (2019) A sensitive network jitter measurement for covert timing channels over interactive traffic. Multimed Tools Appl. https:\/\/doi.org\/10.1007\/s11042-018-6281-1","key":"1486_CR20","DOI":"10.1007\/s11042-018-6281-1"},{"key":"1486_CR21","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.patcog.2017.10.015","volume":"75","author":"Y Li","year":"2018","unstructured":"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\u201362","journal-title":"Pattern Recogn"},{"key":"1486_CR22","doi-asserted-by":"publisher","first-page":"8029","DOI":"10.1109\/ACCESS.2017.2787422","volume":"6","author":"A Elmisery","year":"2017","unstructured":"Elmisery A, Sertovic M, Gupta B (2017) Cognitive privacy middleware for deep learning mashup in environmental IoT. IEEE Access 6:8029\u20138041","journal-title":"IEEE Access"},{"key":"1486_CR23","doi-asserted-by":"publisher","first-page":"3023","DOI":"10.1007\/s12652-018-0928-7","volume":"10","author":"L Jiang","year":"2018","unstructured":"Jiang L, Cheng Y, Yang L, Li J, Yan H, Wang X (2018) A trust-based collaborative filtering algorithm for E-commerce recommendation system. J Amb Intell Human Comput 10:3023\u20133034. https:\/\/doi.org\/10.1007\/s12652-018-0928-7","journal-title":"J Amb Intell Human Comput"},{"issue":"8","key":"1486_CR24","doi-asserted-by":"publisher","first-page":"1494","DOI":"10.1109\/JSTSP.2016.2607692","volume":"10","author":"L Fan","year":"2016","unstructured":"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\u20131505","journal-title":"IEEE J Selected Topics Signal Proc"},{"key":"1486_CR25","doi-asserted-by":"publisher","first-page":"18909","DOI":"10.1109\/ACCESS.2017.2751105","volume":"5","author":"X Lai","year":"2017","unstructured":"Lai X, Zou W, Xie D, Li X, Fan L (2017) DF relaying networks with randomly distributed interferers. IEEE Access 5:18909\u201318917","journal-title":"IEEE Access"},{"issue":"3","key":"1486_CR26","first-page":"919","volume":"19","author":"J Hu","year":"2018","unstructured":"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\u2013926","journal-title":"J Internet Technol"},{"doi-asserted-by":"publisher","unstructured":"Tan Q, Gao Y, Shi J, Wang X, Fang B, Tian Z (2018) Towards a comprehensive insight into the eclipse attacks of Tor hidden services. IEEE Internet Things. https:\/\/doi.org\/10.1109\/JIOT.2018.2846624","key":"1486_CR27","DOI":"10.1109\/JIOT.2018.2846624"},{"issue":"4","key":"1486_CR28","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1109\/TSC.2015.2402679","volume":"9","author":"P Rodriguez-Mier","year":"2016","unstructured":"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\u2013550","journal-title":"IEEE Trans Serv Comput"},{"issue":"1","key":"1486_CR29","first-page":"23","volume":"31","author":"M Omid","year":"2017","unstructured":"Omid M (2017) Context-aware web service composition based on AI planning. Appl Artif Intell 31(1):23\u201343","journal-title":"Appl Artif Intell"},{"issue":"1","key":"1486_CR30","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/TSC.2016.2605090","volume":"10","author":"A Bourouis","year":"2017","unstructured":"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\u201379","journal-title":"IEEE Trans Serv Comput"},{"issue":"1","key":"1486_CR31","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1049\/cje.2016.01.002","volume":"25","author":"J Shunhui","year":"2016","unstructured":"Shunhui J, Bixin L, Dong Q (2016) Incremental verification of evolving BPEL-based web composite service. Chinese J Electron 25(1):6\u201312","journal-title":"Chinese J Electron"},{"issue":"4","key":"1486_CR32","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1080\/02564602.2015.1110061","volume":"33","author":"G Rodriguez","year":"2016","unstructured":"Rodriguez G, Soria A, Campo M (2016) AI-based web service composition: a review. IETE Tech Rev 33(4):378\u2013385","journal-title":"IETE Tech Rev"},{"issue":"3","key":"1486_CR33","first-page":"1483","volume":"28","author":"H Zheng","year":"2017","unstructured":"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\u20131485","journal-title":"Agro Food Ind Hi Tech"},{"issue":"2","key":"1486_CR34","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1093\/logcom\/exx038","volume":"28","author":"J Van Benthem","year":"2018","unstructured":"Van Benthem J, Van Eijck J, Gattinger M, Su K (2018) Symbolic model checking for dynamic epistemic logic \u2014 s5 and beyond. J Log Comput 28(2):367\u2013402","journal-title":"J Log Comput"},{"issue":"1","key":"1486_CR35","first-page":"249","volume":"2014","author":"W Liu","year":"2013","unstructured":"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\u2013266","journal-title":"J Appl Math"},{"doi-asserted-by":"crossref","unstructured":"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)","key":"1486_CR36","DOI":"10.1007\/s11432-017-9152-x"},{"issue":"11","key":"1486_CR37","doi-asserted-by":"publisher","first-page":"2961","DOI":"10.1109\/TAC.2015.2417839","volume":"60","author":"Y Kwon","year":"2015","unstructured":"Kwon Y, Kim E (2015) Bounded model checking of hybrid systems for control. IEEE Trans Automat Control 60(11):2961\u20132976","journal-title":"IEEE Trans Automat Control"},{"key":"1486_CR38","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2017.08.013","volume":"158","author":"S Krings","year":"2018","unstructured":"Krings S, Leuschel M (2018) Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci Comput Program 158:41\u201363","journal-title":"Sci Comput Program"},{"issue":"5","key":"1486_CR39","doi-asserted-by":"publisher","first-page":"710","DOI":"10.1002\/tee.22457","volume":"12","author":"Z Chen","year":"2017","unstructured":"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\u2013720","journal-title":"IEEJ Trans Electr Electr"},{"key":"1486_CR40","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.scico.2017.09.005","volume":"152","author":"F Monteiro","year":"2018","unstructured":"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\u201369","journal-title":"Sci Comput Program"},{"key":"1486_CR41","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.neucom.2015.11.119","volume":"211","author":"J Hu","year":"2016","unstructured":"Hu J, Chen X, Zhang C (2016) Proactive service selection based on acquaintance model and LS-SVM. Neurocomputing 211:60\u201365","journal-title":"Neurocomputing"},{"doi-asserted-by":"crossref","unstructured":"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)","key":"1486_CR42","DOI":"10.1142\/S0218001417590108"},{"key":"1486_CR43","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/j.ins.2016.09.032","volume":"374","author":"H Jia","year":"2016","unstructured":"Jia H, Ding S, Du M, Xue Y (2016) Approximate normalized cuts without Eigen-decomposition. Inform Sci 374:135\u2013150","journal-title":"Inform Sci"},{"issue":"1\u20132","key":"1486_CR44","first-page":"173","volume":"143","author":"B Wo\u017ana-Szcze\u015bniak","year":"2016","unstructured":"Wo\u017ana-Szcze\u015bniak B (2016) SAT-based bounded model checking for weighted deontic interpreted systems. Fund Inform 143(1\u20132):173\u2013205","journal-title":"Fund Inform"},{"key":"1486_CR45","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/j.sysarc.2017.09.008","volume":"81","author":"H Zhang","year":"2017","unstructured":"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\u201316","journal-title":"J Syst Architect"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-019-01486-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-019-01486-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-019-01486-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,11]],"date-time":"2022-10-11T22:40:02Z","timestamp":1665528002000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-019-01486-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,18]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["1486"],"URL":"https:\/\/doi.org\/10.1007\/s11036-019-01486-2","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"type":"print","value":"1383-469X"},{"type":"electronic","value":"1572-8153"}],"subject":[],"published":{"date-parts":[[2020,1,18]]},"assertion":[{"value":"18 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}