| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 431477 | The Journal of Logic and Algebraic Programming | 2007 | 19 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
