Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
LTSA-WS: A Tool for Model-Based Verification of Web Service Compositions and Choreography @INPROCEEDINGS{Foster06ICSE, title = {{LTSA-WS: A Tool for Model-Based Verification of Web Service Compositions and Choreography}}, author = {{Sebastian} {Uchitel} and {Jeff} {Kramer} and {Jeff} {Magee} and {Howard} {Foster}}, booktitle = {IEEE International Conference on Software Engineering (ICSE 2006), Shanghai, China, May 2006.}, abstract = {In this paper we describe a tool for a model-based approach to verifying compositions of web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) process algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of web service compositions can be eased through the understanding of the behavior exhibited by the composition. The approach is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process.}, year = {2006}, url = {http://www.doc.ic.ac.uk/~hf1/phd/papers/de04.pdf}, doi = {10.1145/1134285.1134408}, partner = {LSS-ICL}, status = {public}, task = {T1.2}, }
|