Formal specification of a Web services protocol

Publikationstyp
Journal Article
Date Issued
2006-07-20
Sprache
English
Author(s)
Johnson, James E.  
Langworthy, David E.  
Lamport, Leslie  
Vogt, Friedrich H.  
Institut
Telematik E-17  
TORE-URI
http://hdl.handle.net/11420/4240
Journal
The journal of logic and algebraic programming  
Volume
70
Issue
1
Start Page
34
End Page
52
Citation
Journal of Logic and Algebraic Programming 1 (70): 34-52 (2007)
Publisher DOI
10.1016/j.jlap.2006.05.004
Scopus ID
2-s2.0-33750483241
Publisher
Elsevier Science
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
510: Mathematik