Formal Analysis of Database Trigger Systems Using Event-B

View Sample PDF

Author(s): Anh Hong Le (Hanoi University of Mining and Geology, Hanoi, Vietnam), To Van Khanh (VNU University of Engineering and Technology, Hanoi, Vietnam)and Truong Ninh Thuan (VNU University of Engineering and Technology, Hanoi, Vietnam)
Copyright: 2021
Volume: 9
Issue: 4
Pages: 16
Source title: International Journal of Software Innovation (IJSI)
Editor(s)-in-Chief: Roger Y. Lee (Central Michigan University, USA)and Lawrence Chung (The University of Texas at Dallas, USA)
DOI: 10.4018/IJSI.20211001.oa1

Keywords: Computer Science & IT / Information Science Reference / Systems & Software Design / Systems and Software Engineering

Purchase

View Formal Analysis of Database Trigger Systems Using Event-B on the publisher's website for pricing and purchasing information.

Abstract

Most modern relational database systems use triggers to implement automatic tasks in response to specific events happening inside or outside a system. A database trigger is a human readable block code without any formal semantics. Frequently, people can check if a trigger is designed correctly after it is executed or by manual checking. In this article, the authors introduce a new method to model and verify database trigger systems using Event-B formal method at design phase. First, the authors make use of similar mechanism between triggers and Event-B events to propose a set of rules translating a database trigger system into Event-B constructs. Then, the authors show how to verify data constraint preservation properties and detect infinite loops of trigger execution with RODIN/Event-B. The authors also illustrate the proposed method with a case study. Finally, a tool named Trigger2B which partly supports the automatic modeling process is presented.

The IRMA Community

Research IRM

Formal Analysis of Database Trigger Systems Using Event-B

Purchase

Abstract

Related Content

IRMA Sponsors