Web Service protocol standards should be unambiguous and provide a complete description of the allowed behavior of the protocols’ participants. Implementation of such protocols is an error-prone process, firstly because of the lack of precision and completeness of the standards, and secondly because of erroneous transformation of semantics from the specification to the final implementation. Applying the TLA+ paradigm we first consider the protocol on act level. Safety properties taken from real world scenarios are compared to the facilities of the protocol. As result, we identified some limitation of applicability of the otocol to abstract application use cases, modelled from the real world scenarios. These limitations are an omission of possible activities seen in the real world. Further, WS-C and WS-BA make assumptions about the internal structures of the participants, violating SOA paradigm. The former error could be detected by the use of formal methods. The latter can be c...
Friedrich H. Vogt, Simon Zambrovski, Boris Gruschk