document: Simulation , verification and automated composition of web services Web services -- Web-accessible programs and devices - are a key application area for the Semantic Web . With the proliferation of Web services and the evolution towards the Semantic Web comes the opportunity to automate various Web services tasks . Our objective is to enable markup and automated reasoning technology to describe , simulate , compose , test , and verify compositions of Web services . We take as our starting point the DAML-S DAML+OIL ontology for describing the capabilities of Web services . We define the semantics for a relevant subset of DAML-S in terms of a first-order logical language . With the semantics in hand , we encode our service descriptions in a Petri Net formalism and provide decision procedures for Web service simulation , verification and composition . We also provide an analysis of the complexity of these tasks under different restrictions to the DAML-S composite services we can describe . Finally , we present an implementation of our analysis techniques . This implementation takes as input a DAML-S description of a Web service , automatically generates a Petri Net and performs the desired analysis . Such a tool has broad applicability both as a back end to existing manual Web service composition tools , and as a stand-alone tool for Web service developers .
doc_bio_tags: O O O O O O O B I B I O O O O O O O O O O O O O B I O O O O O B I O O O O O B I O O O O O O B I O O O O O O O O O B I O O O O O O O O O O O O O O B I O O O O O O O O O O O O O O O O B I O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B I I O O O O O O O O O O O O