Johnson, James E.James E.JohnsonLangworthy, David E.David E.LangworthyLamport, LeslieLeslieLamportVogt, Friedrich H.Friedrich H.Vogt2019-12-202019-12-202006-07-20Journal of Logic and Algebraic Programming 1 (70): 34-52 (2007)http://hdl.handle.net/11420/4240We 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. © 2006 Elsevier Inc. All rights reserved.en200613452Elsevier ScienceSpecificationStandardsTLAVerificationInformatikMathematikJournal Article10.1016/j.jlap.2006.05.004Other