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

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

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

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.