Search
 
loader loading subjects...
cover
Compensable transactions
Tony Hoare
116 - 134
NATO Security through Science Series - D: Information and Communication Security
Volume 9: Software System Reliability and Security
Abstract

The concept of a compensable transaction has been embodied in modern business workflow languages like BPEL. This article uses the concept of a box-structured Petri net to formalise the definition of a compensable transaction. The standard definitions of structured program connectives are extended to construct longer-running transactions out of shorter fine-grain ones. Floyd-type assertions on the arcs of the net specify the intended properties of the transaction and of its component programs. The correctness of the whole transaction can therefore be proved by simple local reasoning.

$35.00 / €27.50 / £22.00
Add PDF to cart