论文部分内容阅读
随着Internet的迅速发展和应用,WEB应用已经渗透到国计民生的各个领域。相比一般传统软件,WEB应用具有更高的质量需求。WEB应用本身的高复杂性使的对其验证、测试都相当困难,基于模型检查的Web应用验证方法是保证WEB应用质量的方法之一。
目前已有众多的模型检查方法和多种模型结构,Petri网是其中一种重要的模型描述工具,Petri网能够自然地描述并发、同步、资源竞争等系统特性,易于描述Web服务的动态行为。故基于Petri网的Web服务模型适于验证Web应用的运行过程。
本文对Web服务应用的验证模型构建进行研究,通过分析WEB应用描述语言SCXML,基于Petri网模型形式对系统模型进行模型检查。
本文主要工作如下:
1.分析了WEB应用建模语言SCXML,根据WEB应用的特征和SCXML语言具有的并发性、控制等性质,分析了WEB应用的行为、性质等。
2.通过对SCXML中元素属性的分析,实现了将现有的Web服务应用描述语言SCXML转化为模型检测器可以接受的模型------基于对扩展的Petri网的形式描述,达到SCXML到扩展Petri网的转化,使SCXML描述的并发、同步、资源竞争等WEB系统特性能够在扩展Petri网结构模型上得以体现,为Web服务转换性质的分析与验证提供有力的支持。
3.详细探讨了基于Petri网的模型检查算法,并引入on-the-fly技术进行Petri网的模型检查,同时对on-the-fly算法进行优化,以此来减缓状态空间爆炸的问题,使存储规范Petri网模型和待验证Petri网模型的交Petri网模型所占用的空间减少,从而很好地缓解内存不足的问题。
4.在提出了基于on-the-fly的Petri网的模型检查算法的基础上,用JAVA语言对算法进行了实现,并通过实例测试基于on-the-fly算法的Petri网模型检查算法的正确性。