Affiliations: Department of Mathematics and Computer Science,
Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The
Netherlands. k.m.v.hee@tue.nl, n.sidorova@tue.nl, m.voorhoeve@tue.nl,
j.m.e.m.v.d.werf@tue.nl
Note: [] Address for correspondence: Department of Mathematics and
Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB
Eindhoven, The Netherlands
Abstract: Deleting a record from a database table without modifying other
records or tables can easily lead to a violation of the database constraints.
The same holds for other database operations. In this paper we generate
descriptions of transactions triggered by a given operation, guaranteeing that
if the database is in a consistent state before a transaction starts, it will
be in a consistent state after it is finished. We describe transactions as
models of a special 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.
