手工分析组合服务相当困难和耗时,为此提出了一种基于uMSD的Web服务组合的模型检验方法.如何简单和直观地表示Web服务组合的时态性质是该方法的关键问题.鉴于uMSD在简单性和表达力之间找到了一个平衡点,定义了uMSD的形式语法和语义.以Web服务组合OJA为实例,使用uMSD来图形化地表示组合服务的时态性质,展示了uMSD的可行性.实验分析表明,该验证方法能够有效地检测组合服务中的逻辑错误.%In order to solve the problem that analyzing the composite services by manual is rather difficult and time-con suming; an approach was proposed to verify composite services by model checking based on uMSD. How to represent the temporal properties of the composite service easily and intuitively is a critical issue of the approach. Because uMSD finds a balance between simplicity of use and expressiveness; the paper defined the formal syntax and semantics of uMSD. In the paper; uMSD was used to graphically represent the temporal properties of a composite service On-the-Job Assistant as a case study; presenting the feasibility of uMSD. A series of experiments show the approach can effectively detect the logical errors in the composite service.
展开▼
