Verification and validation of systems is greatly influenced by the choices made at modeling stage. Both expressible system features and verifiable properties strongly depend on the used description language. This work uses a modular Petri Net derived formalism -Timed Net Condition/Event Systems (TNCES) - to model service orchestrators. Coverage of all representative orchestration characteristics is ensured by selecting OWL-S as provider for the main set of flow descriptors. This paper discusses the considered alternatives for each modeling decision, and gives grounds for the final choices made. In particular, timed automata, process algebras and Petri Nets are compared to support the selection of TNCES as formalism for the representation of service orchestration. The second main modeling decision is sustained by an analysis of four web composition languages: BPEL, WS-CDL, OWL-S and WSMO. The paper concludes with a presentation of the industrial demonstrator of this research and a discussion of the applicable verification techniques.
展开▼
