基于模型驱动的Web服务符号执行与验证
Journal of Jiangxi Normal University（Natural Sciences Edition）（2022）
摘要
Web服务测试与验证是保证Web服务功能正确的关键,目前大多数Web服务的研究无法对程序路径穷举遍历,不能保证分析的完备性.针对该不足,在基于模型驱动的3阶段Web服务模型转换生成方法的基础上,该文对转换生成的Java代码进行符号执行与形式化验证.符号执行方法可对程序运行的所有路径进行分析,为程序测试提供高覆盖率的测试用例,可以触发深层的程序错误,进而在Java代码中加入JML方法契约,可对Web服务进行形式化验证.通过PayPal Web服务案例,采用模型驱动的方法将Web服务模型转换生成方法生成Java代码,使用自动化工具对Java代码进行符号执行;将Radl-WS服务建模语言转换为JML方法契约,并对Java代码进行形式化验证.符号执行与形式化验证方法确保了生成的Java代码可靠性与正确性,提高了自动化程度.
更多AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要