典型文献
基于模型驱动的Web服务符号执行与验证
文献摘要：
Web服务测试与验证是保证Web服务功能正确的关键,目前大多数Web服务的研究无法对程序路径穷举遍历,不能保证分析的完备性.针对该不足,在基于模型驱动的3阶段Web服务模型转换生成方法的基础上,该文对转换生成的Java代码进行符号执行与形式化验证.符号执行方法可对程序运行的所有路径进行分析,为程序测试提供高覆盖率的测试用例,可以触发深层的程序错误,进而在Java代码中加入JML方法契约,可对Web服务进行形式化验证.通过PayPal Web服务案例,采用模型驱动的方法将Web服务模型转换生成方法生成Java代码,使用自动化工具对Java代码进行符号执行;将Radl-WS服务建模语言转换为JML方法契约,并对Java代码进行形式化验证.符号执行与形式化验证方法确保了生成的Java代码可靠性与正确性,提高了自动化程度.
文献关键词：
Web服务;Radl-WS;Java代码;符号执行;验证
中图分类号：
作者姓名：
王昌晶;陈茜;丁希龙;罗海梅;左正康
作者机构：
江西师范大学计算机信息工程学院,江西 南昌 330022;江西师范大学管理科学与工程研究中心,江西 南昌 330022;江西师范大学物理与通信电子学院,江西 南昌 330022
文献出处：
引用格式：
[1]王昌晶;陈茜;丁希龙;罗海梅;左正康-.基于模型驱动的Web服务符号执行与验证)[J].江西师范大学学报（自然科学版）,2022(01):37-48
A类：
JML,Radl
B类：
基于模型,模型驱动,符号执行,测试与验证,穷举,遍历,完备性,服务模型,模型转换,生成方法,Java,代码,形式化验证,程序运行,程序测试,高覆盖,测试用例,契约,PayPal,服务案例,自动化工具,WS,建模语言,语言转换,验证方法
AB值：
0.309578
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
