Generation of database transactions with Petri nets

In this paper we show how we can generate models for the execution of database transactions. We describe a transaction goal by a data model and we give algorithms to generate Petri nets models that specify the execution of these transactions. This is done in such a way that database constraints, in particular referential integrity constraints, are preserved. So if the database is in a consistent state before a transaction starts, it will be in a consistent state after the transaction. The class of Petri nets we use is a subclass of coloured Petri nets, where token values are vectors of identifiers. This class is powerful enough to model transaction execution and it allows for some formal analysis, like soundness.