论文部分内容阅读
传统的基于有限状态机的组合weh服务模型检测方法不能保证带有时间约束的组合web服务的正确性。把组合web服务看成多智能体系统，将带有时间约束的web服务智能体建模为时间自动机，通过并发组合构成时间自动机网络，从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟，并验证其活性、安全性和死锁等性质。采用该方法对雇员出差安排组合Web服务进行建模和验证，结果表明，该组合Web服务存在死锁问题。最后通过分析死锁产生的路径，完善该组合Web服务的通信协议，从而消除了死锁。