In the world of Service Oriented Architectures, one deals with networks of cooperating components. A component offers services; to deliver a service it possibly needs services of other components, thus forming a service tree. This tree is built dynamically and not known beforehand. It is hard to verify the behavior of a service tree by using standard verification techniques, because these techniques typically assume a static flattened model. In this paper we model a component by an open Petri net. We give a sufficient condition for proper completion (called soundness) that requires only pairwise checks of the service compositions. We also provide a correctness-by-construction approach for building services trees.
|Title of host publication||Applications and Theory of Petri Nets (30th International Conference, Petri Nets 2009, Paris, France, June 22-26, 2009, Proceedings)|
|Editors||G. Franceschinis, K. Wolf|
|Place of Publication||Berlin|
|Publication status||Published - 2009|
|Name||Lecture Notes in Computer Science|