Titlebook: Web Services and Formal Methods; 4th International Wo Marlon Dumas,Reiko Heckel Conference proceedings 2008 Springer-Verlag Berlin Heidelbe

pancreas

妨碍议事

Synthesis of Web Services Orchestrators in a Timed Setting,By using this function we are able to reduce the starting problem to a satisfiability one that we solve by exploiting a satisfiability procedure for temporal logic. In this way we automatically generate an . as a model of the request.

Allege

Towards a Theory of Web Service Choreographies,ugh interactions among the shared components that are modeled as web services. It is expected that not only the participating services are complex and have observable states, but the number of interacting services may be also large. Prior work on choreographies (conversation protocols) all focuses o

habitat

Controlling Petri Net Process Models,ontrol has the aim to force a process to behave in a desirable way. Process models that behave properly without any control are often called “sound”. For process models that behave properly when being controlled, i.e., for controllable processes, there are various related notions, such as “relaxed s

结合

Extending Model Checking to Data-Aware Temporal Properties of Web Services,nt are interdependent. The logic CTL-FO. expresses these properties by allowing temporal operators and first-order quantification over message content to be freely mixed. A “naïve” translation of CTL-FO. into CTL leads to a serious exponential blow-up of the problem that prevents existing validation