[1]王昌晶,陈 茜,丁希龙,等.基于模型驱动的Web服务符号执行与验证[J].江西师范大学学报(自然科学版),2022,(01):37-48.[doi:10.16357/j.cnki.issn1000-5862.2022.01.06]
　WANG Changjing,CHEN Xi,DING Xilong,et al.The Web Service Symbolic Execution and Verification Based on Model-Driven[J].Journal of Jiangxi Normal University:Natural Science Edition,2022,(01):37-48.[doi:10.16357/j.cnki.issn1000-5862.2022.01.06]
点击复制

基于模型驱动的Web服务符号执行与验证()
分享到：

《江西师范大学学报》（自然科学版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2022年01期
页码:
37-48
栏目:
高可信与智能软件
出版日期:
2022-01-25

文章信息/Info

Title:
The Web Service Symbolic Execution and Verification Based on Model-Driven
文章编号:
1000-5862(2021)06-0037-12
作者:
王昌晶1; 2; 陈 茜1; 丁希龙1; 罗海梅3; 左正康1*
1.江西师范大学计算机信息工程学院,江西 南昌 330022; 2.江西师范大学管理科学与工程研究中心,江西 南昌 330022; 3.江西师范大学物理与通信电子学院,江西 南昌 330022
Author(s):
WANG Changjing1; 2; CHEN Xi1; DING Xilong1; LUO Haimei3; ZUO Zhengkang1*
1.College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 2.Management Science and Engineering Research Center,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 3.College of Physics and Communication Electronics,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
Web服务;  Radl-WS;  Java代码;  符号执行;  验证
Keywords:
Web service;  Radl-WS;  Java;  symbolic execution;  verification
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2022.01.06
文献标志码:
A
摘要:
Web服务测试与验证是保证Web服务功能正确的关键,目前大多数Web服务的研究无法对程序路径穷举遍历,不能保证分析的完备性.针对该不足,在基于模型驱动的3阶段Web服务模型转换生成方法的基础上,该文对转换生成的Java代码进行符号执行与形式化验证.符号执行方法可对程序运行的所有路径进行分析,为程序测试提供高覆盖率的测试用例,可以触发深层的程序错误,进而在Java代码中加入JML方法契约,可对Web服务进行形式化验证.通过PayPal Web服务案例,采用模型驱动的方法将Web服务模型转换生成方法生成Java代码,使用自动化工具对Java代码进行符号执行; 将Radl-WS服务建模语言转换为JML方法契约,并对Java代码进行形式化验证.符号执行与形式化验证方法确保了生成的Java代码可靠性与正确性,提高了自动化程度.
Abstract:
Web service testing and verification are the keys to ensuring the correct function of Web services.Most current research on Web services cannot traverse the program path exhaustively,and cannot guarantee the completeness of the analysis.For this problem,the symbolic execution and formal verification are performed on the Java code generated by the conversion based on the previous model-driven three-stage Web service model conversion generation method.The symbolic execution method can analyze all paths of program running,provide test cases with high coverage for program testing and trigger deep program errors.Furthermore,the JML method contract is added to the Java code to verify the Web service.In the PayPal Web service case,the model-driven method is adopted to generate Java code from Web service model transformation generation method,and the automated tools are used to perform symbolic execution of the Java code.In addition,the Radl-WS service modeling Language is transformed into JML method contracts and the formal validation of Java code is performed.Symbolic execution and verification methods ensure the correctness and credibility of the generated Java code and improve the degree of automation.

参考文献/References:

[1] SOURI A,RAHMANI A M,NAVIMIPOUR N J,et al.A symbolic model checking approach in formal verification of distributed systems [J].Human Centric Computing and Information Sciences,2019,9(1):1-27.
[2] 彭焕峰,黄纬,范大娟,等.Web 服务演化综述 [J].科学技术与工程,2015,15(30):63-70.
[3] 丁志军,周泽霞.Web 服务组合测试综述 [J].Journal of Software,2018,29(2):299-319.
[4] 廖军,谭浩,刘锦德.基于 Pi-演算的Web服务组合的描述和验证 [J].计算机学报,2005,28(4):635-643.
[5] 罗异.基于模型驱动架构的Web代码生成方法研究与应用 [D].重庆:重庆邮电大学,2018.
[6] DO KIM H.BPMN-based modeling of B2B business processes from the neutral perspective of UMM/BPSS [EB/OL].[2021-03-16].https://ieeexplore.ieee.org/document/4590645.
[7] SADOVYKH A,DESFRAY P,ELVESAETER B,et al.Enterprise architecture modeling with soaML using BMM and BPMN-MDA approach in practice [EB/OL].[2021-03-16].https://ieeexplore.ieee.org/document/5783155.
[8] 徐华珍,薛锦云,朱小征.Apla→Java 程序生成系统中泛型机制实现方法研究 [J].江西师范大学学报(自然科学版),2017,41(1):52-55.
[9] 石海鹤,薛锦云.基于PAR的算法形式化开发 [J].计算机学报,2009,32(5):982-991.
[10] 谢武平.Radl→Apla 程序生成系统及其可靠性研究 [D].南昌:江西师范大学,2009.
[11] 石海鹤.支持泛型程序设计的Apla-Java自动程序转换系统 [D].南昌:江西师范大学,2004:1-74.
[12] 左正康,薛锦云.Apla中泛型约束机制研究 [J].软件学报,2015,26(6):1340-1355.
[13] 叶志斌,严波.符号执行研究综述 [J].计算机科学,2018,45(6A):28-35.
[14] CADAR C,SEN K.Symbolic execution for software testing:three decades later [J].Communications of the ACM,2013,56(2):82-90.
[15] HENTSCHEL M,BUBEL R,HÄHNLE R.The symbolic execution debugger(SED):a platform for interactive symbolic execution,debugging,verification and more [J].International Journal on Software Tools for Technology Transfer, 2019,21(5):485-513.
[16] AHRENDT W,BECKERT B,HÄHNLE R,et al.Verifying object-oriented programs with KeY:a tutorial [EB/OL].[2021-03-19].https://dl.acm.org/doi/10.5555/1777707.1777713.
[17] 王昌晶,薛锦云.Radl形式规格说明相对正确性研究 [J].软件学报,2013,24(4):715-729.
[18] 王昌晶.基于扩展逻辑变换系统μTS证明循环变换正确性 [J].计算机研究与发展,2012,49(9):1863-1873.
[19] 张广泉.形式化方法导论 [M].北京:清华大学出版社,2015:1-256.
[20] 张琦,王昌晶,罗海梅,等.WSDL→Radl-WS 生成方法及自动转换系统 [J].江西师范大学学报(自然科学版),2018,42(3):298-303.
[21] SALEH I,KULCZYKI G,BLAKE M B,et al.Formal methods for data-centric Web services:from model to implementation [EB/OL].[2021-03-20].https://ieeexplore.ieee.org/document/6649596.

相似文献/References:

[1]谢承旺.面向服务的电力行业信息系统应用集成研究[J].江西师范大学学报(自然科学版),2012,(06):631.
　LI Juan,DING Shu-liang*,LUO Fen.The Research on Application Integration Scheme for Power Industry Enterprises[J].Journal of Jiangxi Normal University:Natural Science Edition,2012,(01):631.

备注/Memo

备注/Memo:
收稿日期:2021-09-12
基金项目:国家自然科学基金(61762049,61862033)和江西省教育厅科技重点课题(GJJ210307)资助项目.
作者简介:王昌晶(1977—),男,江西南昌人,教授,博士,博士生导师,主要从事软件形式化方法、形式规格说明方法和Web服务方面的研究.E-mail:wcj771006@126.com
通信作者:左正康(1980—),男,江西抚州人,教授,博士,主要从事泛型程序设计和可信软件的研究.E-mail:kerrykaren@126.com
更新日期/Last Update: 2022-01-25