论文部分内容阅读
Web交互模型的形式化验证是对Web事件属性进行校验的十分可信的方法。通过一系列的系统模型建立、系统行为分析以及对于模型中关心属性的相关验证，能够让交互模型在设计阶段就能使形式化模型暴露出其所存在的缺陷，而不至于让缺陷保留到编码阶段或者更后面才能被真正地暴露出来，这样使系统模型的生存能力更加强大，同时避免了因后期缺陷暴露而出现的大代价修复。通过对Web系统的交互应用服务的过程模型化的体系进行研究，通过模型本身具有的属性进行相关正确性的校验，主要通过使用数学推理实现系统逻辑上的服务交互进程，从而进行过程的推