Article

LTSA-WS: a tool for model-based verification of web service compositions and choreography

Authors:

Howard Foster,

Sebastian Uchitel,

Jeff Magee,

Jeff KramerAuthors Info & Claims

ICSE '06: Proceedings of the 28th international conference on Software engineering

Pages 771 - 774

https://doi.org/10.1145/1134285.1134408

Published: 28 May 2006 Publication History

Get Access

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.

References

[1]

W3C-WS-A, "Web Services Architecture (WS-A)," vol. 2004: W3C Working Group Note 11 February 2004, 2002.

Google Scholar

[2]

F. Curbera, Y. Goland, J. Klein, F. Leymann, D. Roller, S. Thatte, and S. Weerawarana, "Business Process Execution Language For Web Services, Version 1.1," 2003.

Google Scholar

[3]

W3C-WSCI, "Web Service Choreography Interface (WSCI) 1.0," W3C - Web Services Choreography Working Group 2002.

Google Scholar

[4]

R. Akkiraju, D. Flaxer, H. Chang, T. Chao, L.-J. Zhang, F. Wu, and J.-J. Jeng, "A Framework for Facilitating Dynamic e-Business via Web Services," presented at OOPSLA 2001 - Workshop on Object-Oriented Web Services, Tampa, FL, 2001.

Google Scholar

[5]

C. Karamanolis, D. Giannakopoulou, J. Magee, and S. Wheater, "Modelling and Analysis of Workflow Processes," Imperial College of Science, Technology and Medicine, London 1999.

Google Scholar

[6]

H. Foster, S. Uchitel, J. Magee, and J. Kramer, "Model-based Verification of Web Service Compositions," presented at Eighteenth IEEE International Conference on Automated Software Engineering (ASE), Montreal, Canada, 2003a.

Digital Library

Google Scholar

[7]

H. Foster, S. Uchitel, J. Magee, and J. Kramer, "Compatibility for Web Service Choreography," presented at 3rd IEEE International Conference on Web Services (ICWS), San Diego, CA, 2004a.

Digital Library

Google Scholar

[8]

O. Bukhres and C. J. Crawley, "Failure Handling in Transactional Workflows Utilizing CORBA 2.0," presented at 10th ERCIM Database Research Group Workshop on Heterogeneous Information Management, Prague, 1996.

Google Scholar

[9]

R. J. Hall, "Open Modeling in Multi-stakeholder Distributed Systems: Model-based Requirements Engineering for the 21st Century," presented at Proc. First Workshop on the State of the Art in Automated Software Engineering, U.C. Irvine Institute for Software Research, 2003.

Digital Library

Google Scholar

[10]

X. Fu, T. Bultan, and J. Su, "WSAT: A tool for Formal Analysis of Web Services," presented at 16th International Conference on Computer Aided Verification (CAV), Boston, MA, 2004.

Google Scholar

[11]

S. Nakajima, "Model-Checking Verification for Reliable Web Service," presented at OOPSLA 2002 Workshop on Object-Oriented Web Services, Seattle, Washington, 2002.

Google Scholar

[12]

S. Uchitel and J. Kramer, "A Workbench for Synthesising Behaviour Models from Scenarios," presented at the 23rd IEEE International Conference on Software Engineering (ICSE'01), Toronto, Canada, 2001.

Digital Library

Google Scholar

[13]

J. Magee and J. Kramer, Concurrency - State Models and Java Programs: John Wiley, 1999.

Digital Library

Google Scholar

[14]

H. Foster, "A Guide to Mapping BPEL4WS to FSP," Department of Computing, Imperial College London, Technical Report 2003b.

Google Scholar

Cited By

View all

Wan LWang CLuo DLiu HMa SHu W(2024)Semantic Consistency and Correctness Verification of Digital Traffic RulesEngineering10.1016/j.eng.2023.04.01633(47-62)Online publication date: Feb-2024
https://doi.org/10.1016/j.eng.2023.04.016
partabian j(2023)Checking reachability property of systems specified through graph transformation with the approach of discovery conditional dependency between the rulesSignal and Data Processing10.61186/jsdp.20.2.17520:2(175-194)Online publication date: 1-Sep-2023
https://doi.org/10.61186/jsdp.20.2.175
Sadovykh AMesse NNigmatullin IEbersold SNaumcheva MBruel J(2023)Security Requirements Formalization with RQCODECyberSecurity in a DevOps Environment10.1007/978-3-031-42212-6_3(65-92)Online publication date: 23-Aug-2023
https://doi.org/10.1007/978-3-031-42212-6_3
Show More Cited By

Index Terms

LTSA-WS: a tool for model-based verification of web service compositions and choreography
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Modeling the WorkUnit of WS-CDL Based on Process Algebra
ICRCCS '09: Proceedings of the 2009 International Conference on Research Challenges in Computer Science

The description of choreography, WS-CDL, is an interactive description from global view which lacks formal semantics. The formal syntax and semantics, Process Algebra for WS-CDL (PA4WS), are proposed to describe WS-CDL using service channel and session ...
A Comparative Study between WSCI, WS-CDL, and OWL-S
ICEBE '09: Proceedings of the 2009 IEEE International Conference on e-Business Engineering

Choreography languages allow us to describe Web Services compositions from a global viewpoint in Service Oriented Architectures (SOA). However, none of the existing languages has achieved the status of de facto standard for that purpose until now. In ...
Formal Modeling and Conformance Validation for WS-CDL using Reo and CASM

WS-CDL is a choreography language that describes peer-to-peer collaborations of participants by defining their common and complementary observable behaviors from a global viewpoint. The main use of a choreography description is to precisely define the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '06: Proceedings of the 28th international conference on Software engineering

May 2006

1110 pages

ISBN:1595933751

DOI:10.1145/1134285

General Chair:
Leon J. Osterweil
University of Massachusetts, USA
,
Program Chairs:
Dieter Rombach
TU Kaiserslautern, Germany
,
Mary Lou Soffa
University of Virginia, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 May 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE06

Sponsor:

ICSE06: International Conference on Software Engineering

May 20 - 28, 2006

Shanghai, China

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

108
Total Citations
View Citations
1,021
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 31 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Wan LWang CLuo DLiu HMa SHu W(2024)Semantic Consistency and Correctness Verification of Digital Traffic RulesEngineering10.1016/j.eng.2023.04.01633(47-62)Online publication date: Feb-2024
https://doi.org/10.1016/j.eng.2023.04.016
partabian j(2023)Checking reachability property of systems specified through graph transformation with the approach of discovery conditional dependency between the rulesSignal and Data Processing10.61186/jsdp.20.2.17520:2(175-194)Online publication date: 1-Sep-2023
https://doi.org/10.61186/jsdp.20.2.175
Sadovykh AMesse NNigmatullin IEbersold SNaumcheva MBruel J(2023)Security Requirements Formalization with RQCODECyberSecurity in a DevOps Environment10.1007/978-3-031-42212-6_3(65-92)Online publication date: 23-Aug-2023
https://doi.org/10.1007/978-3-031-42212-6_3
Abbassi IMammar AGraiet M(2022)A Correct-by-Construction Model for Verifying Transactional Composite Services ConfigurationIEEE Transactions on Services Computing10.1109/TSC.2021.307232715:5(2511-2525)Online publication date: 1-Sep-2022
https://doi.org/10.1109/TSC.2021.3072327
Dechsupa CVatanawood WThongtak A(2022)Stepwise Verification for the BPMN With Timed and Stochastic Process Using a Colored Generalized Stochastic Petri NetIEEE Access10.1109/ACCESS.2022.316800010(42983-43002)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3168000
Menghi CRizzi ABernasconi A(2020)Integrating Topological Proofs with Model Checking to Instrument Iterative DesignFundamental Approaches to Software Engineering10.1007/978-3-030-45234-6_3(53-74)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45234-6_3
Manaf NMoschoyiannis S(2019)Generating choreographies from SBVR modelsPROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON MATHEMATICAL SCIENCES AND TECHNOLOGY 2018 (MATHTECH2018): Innovative Technologies for Mathematics & Mathematics for Technological Innovation10.1063/1.5136494(060062)Online publication date: 2019
https://doi.org/10.1063/1.5136494
Rafe VDarghayedi MPira E(2019)MS-ACOSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-018-3444-y23:12(4531-4556)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s00500-018-3444-y
Moschoyiannis SMaglaras LManaf N(2018)Trace-Based Verification of Rule-Based Service Choreographies2018 IEEE 11th Conference on Service-Oriented Computing and Applications (SOCA)10.1109/SOCA.2018.00034(185-193)Online publication date: Nov-2018
https://doi.org/10.1109/SOCA.2018.00034
Regis GDegiovanni RD'Ippolito NAguirre NBodden ESchäfer WDeursen AZisman A(2017)CLTSA: labelled transition system analyser with counting fluent supportProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3122828(979-983)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3122828
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Modeling the WorkUnit of WS-CDL Based on Process Algebra

A Comparative Study between WSCI, WS-CDL, and OWL-S

Formal Modeling and Conformance Validation for WS-CDL using Reo and CASM

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations