Abstract: Transactions are contracts that guarantee a consistent, transparent, individual system state transition and their use is widespread in many different kinds of computing systems. Some well known standards (e.g. Corba) include the specification of services that provide transactional properties. In this paper, we present a formal method for the systematic synthesis of transactional middleware based on the combination of the aforementioned services. The synthesis of transactional middleware is based on (i) the formal specification of transactional properties and (ii) stub code generation.