SPECIFICATION AND VERIFICATION OF COMMUNICATION CONSTRAINTS FOR INTEROPERABLE TRANSACTIONS
- 1 March 1994
- journal article
- Published by World Scientific Pub Co Pte Ltd in International Journal of Cooperative Information Systems
- Vol. 3 (1) , 47-65
- https://doi.org/10.1142/s0218215794000041
Abstract
The specification of communication behavior is fundamental in developing interoperable transactions. In particular, the temporal ordering of messages exchanged between different communicating agents must be declaratively specified and verified in order to guarantee consistency of data in the various component systems. This paper shows that by expressing communication constraints in propositional temporal logic, the tableau method can be applied to construct a dependency graph. If the specification is correct, this method guarantees that all possible execution paths satisfying the specification will be generated. The declarative specification and verification of communication constraints in interoperable transactions is demonstrated using the classic business trip. It is argued that the specification formalism provides an improvement over the Flexible Transaction Model.Keywords
This publication has 0 references indexed in Scilit: