Modeling and verifying DML triggers using Event-B

Abstract

Database trigger is a block code that automatically executes in response to changes of table or view in the database system. The correctness of a trigger usually can be verified when it is executed. It is apparently useful if we can detect the trigger system's errors in the design phase. In this paper, we introduce an approach to model and verify data manipulation language (DML) triggers in the database system by a formal method. In the first phase, we formalize a database trigger system by an Event-B model. After that, we use the Rodin tool to verify some properties of the system such as termination, preservation of constraint rules. We also run an example to illustrate the approach in detail. © 2013 Springer-Verlag.