Welcome to the InfoSci Platform
Formal Analysis of Database Trigger Systems Using Event-B

Formal Analysis of Database Trigger Systems Using Event-B

Anh Hong Le, To Van Khanh, Truong Ninh Thuan
Copyright: © 2021 |Volume: 9 |Issue: 4 |Pages: 16
ISSN: 2166-7160|EISSN: 2166-7179|EISBN13: 9781799862796|DOI: 10.4018/IJSI.20211001.oa1
Cite Article Cite Article

MLA

Le, Anh Hong, et al. "Formal Analysis of Database Trigger Systems Using Event-B." IJSI vol.9, no.4 2021: pp.158-173. http://doi.org/10.4018/IJSI.20211001.oa1

APA

Le, A. H., Van Khanh, T., & Thuan, T. N. (2021). Formal Analysis of Database Trigger Systems Using Event-B. International Journal of Software Innovation (IJSI), 9(4), 158-173. http://doi.org/10.4018/IJSI.20211001.oa1

Chicago

Le, Anh Hong, To Van Khanh, and Truong Ninh Thuan. "Formal Analysis of Database Trigger Systems Using Event-B," International Journal of Software Innovation (IJSI) 9, no.4: 158-173. http://doi.org/10.4018/IJSI.20211001.oa1

Export Reference

Mendeley
Favorite Full-Issue Download

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.