基于模型驱动的Web服务符号执行与验证  

The Web Service Symbolic Execution and Verification Based on Model-Driven

作　　者：王昌晶[1,2] 陈茜 丁希龙 罗海梅 左正康[1] WANG Changjing;CHEN Xi;DING Xilong;LUO Haimei;ZUO Zhengkang(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;Management Science and Engineering Research Center,Jiangxi Normal University,Nanchang Jiangxi 330022,China;College of Physics and Communication Electronics,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学管理科学与工程研究中心,江西南昌330022 [3]江西师范大学物理与通信电子学院,江西南昌330022

出　　处：《江西师范大学学报（自然科学版）》2022年第1期37-48,共12页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(61762049,61862033);江西省教育厅科技重点课题(GJJ210307)资助项目.

摘　　要：Web服务测试与验证是保证Web服务功能正确的关键,目前大多数Web服务的研究无法对程序路径穷举遍历,不能保证分析的完备性.针对该不足,在基于模型驱动的3阶段Web服务模型转换生成方法的基础上,该文对转换生成的Java代码进行符号执行与形式化验证.符号执行方法可对程序运行的所有路径进行分析,为程序测试提供高覆盖率的测试用例,可以触发深层的程序错误,进而在Java代码中加入JML方法契约,可对Web服务进行形式化验证.通过PayPal Web服务案例,采用模型驱动的方法将Web服务模型转换生成方法生成Java代码,使用自动化工具对Java代码进行符号执行;将Radl-WS服务建模语言转换为JML方法契约,并对Java代码进行形式化验证.符号执行与形式化验证方法确保了生成的Java代码可靠性与正确性,提高了自动化程度.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.

关 键 词：WEB服务 Radl-WS JAVA代码 符号执行 验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]