论文部分内容阅读
为了提高组合web服务的设计和实现质量,使用形式化方法对其进行建模并对其关键性质进行验证.使用web服务接口控制流自动机(WCFA)对web服务进行建模,主要描述其控制流及与其他web服务的交互关系.组合web服务由一组交互的WCFA组成.使用嵌套字自动机(NWA)对组合web服务的整体行为进行建模.将一组WCFA转换为嵌套字自动机(NWA)的算法是深度优先搜索算法的变种,算法中使用路径相关的可达性分析计算NWA的每个节点的状态公式和调用栈.安全性相关性质、调用栈相关性质及服务调用的前置和后置条件都可以用断言来描述,然后使用一个自动的可满足性(SAT)求解工具对这些断言进行验证.
To improve the design and implementation quality of a composite web service, formalize it and validate its key properties using a web-service interface control flow automata (WCFA) to model web services that describe their control Flow, and interaction with other web services Composed web services consist of a set of interacting WCFA models The overall behavior of a composite web service is modeled using a nested word automata (NWA) A set of WCFA is converted to a nested word The algorithm of the automata (NWA) is a variant of a depth-first search algorithm that uses path-related reachability analysis to compute the state formula and call stack for each node of the NWA. Security-related properties, the nature of the call stack, and the service invocation Both the preconditions and postconditions can be described in assertions and then validated using an automatic Satisfaction (SAT) solver.