Transaction Routing and its Verification by Correct Model Transformations

This paper presents model transformations that are encountered in refining an abstract point-to-point transaction between two processes into a complex transaction, routed over the communication architecture, consisting of multiple busses and bridges. These transformations form part of synthesizing an abstract specification model into a detailed model representing the implementation of that specification onto a platform. We present these transformations in the context of a modeling formalism that has well defined execution semantics and a notion of functional equivalence. The transformations are proven correct using our notion of equivalence. We also present methods for deriving the proof of equivalence between the abstract model and the refined model. Based on these methods, we have implemented a tool that automatically proves whether or not the model generated after transaction routing is indeed equivalent to the input model. Experimental results for large industrial examples demonstrate the feasibility, utility and efficiency of our tool and the underlying methods