Formal specification of a Web services protocol

Publikationstyp
Journal Article
Date Issued
2004-12-10
Sprache
English
Author(s)
Johnson, James E.  
Langworthy, David E.  
Lamport, Leslie  
Vogt, Friedrich H.  
Institut
Telematik E-17  
TORE-DOI
10.15480/882.2602
TORE-URI
http://hdl.handle.net/11420/4621
Journal
Electronic notes in theoretical computer science  
Volume
105
Issue
1-4 SUPPL.
Start Page
147
End Page
158
Citation
Electronic Notes in Theoretical Computer Science 1-4 SUPPL. (105): 147-158 (2004-12-10)
Publisher DOI
10.1016/j.entcs.2004.02.022
Scopus ID
2-s2.0-10444259131
Publisher
Elsevier
We describe a use of formal methods to specify and check a Web Services protocol. The Web Services Atomic Transaction protocol was specified in TLA + and checked with the TLC model checker. A modest effort revealed oversights that caused unanticipated behaviors of the protocol; these were corrected by clarifications and changes to the protocol.
Subjects
Specification
Standards
Tla
Verification
DDC Class
004: Informatik
Lizenz
https://creativecommons.org/licenses/by-nc-nd/3.0/
Loading...
Thumbnail Image
Name

1-s2.0-S1571066104051655-main.pdf

Size

258.34 KB

Format

Adobe PDF