Formal specification of a Web services protocol

Publikationstyp
Journal Article
Publikationsdatum
2006-07-20
Sprache
English
Author
Johnson, James E. 
Langworthy, David E. 
Lamport, Leslie 
Vogt, Friedrich H. 
Institut
Telematik E-17 
TORE-URI
http://hdl.handle.net/11420/4240
Enthalten in
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.
Schlagworte
Specification
Standards
TLA
Verification
DDC Class
004: Informatik
510: Mathematik