Research Article
Trigger2B: A Tool Generating Event-B Models from Database Triggers
@INPROCEEDINGS{10.1007/978-3-030-67101-3_8, author={Hong Anh Le}, title={Trigger2B: A Tool Generating Event-B Models from Database Triggers}, proceedings={Context-Aware Systems and Applications, and Nature of Computation and Communication. 9th EAI International Conference, ICCASA 2020, and 6th EAI International Conference, ICTCC 2020, Thai Nguyen, Vietnam, November 26--27, 2020, Proceedings}, proceedings_a={ICCASA \& ICTCC}, year={2021}, month={1}, keywords={Trigger Event-B Formal modeling Generation}, doi={10.1007/978-3-030-67101-3_8} }- Hong Anh Le
Year: 2021
Trigger2B: A Tool Generating Event-B Models from Database Triggers
ICCASA & ICTCC
Springer
DOI: 10.1007/978-3-030-67101-3_8
Abstract
Triggers are commonly used many traditional database applications that can be checked if they are correct after execution or manual inspection. Formal methods are techniques complementing to testing that ensure the correctness of software. In practical aspect, one limitation of formal techniques is the complexity that makes software developers lazy to use in the development. This paper introduces a tool named Trigger2B which partly supports for translating DML triggers to Event-B models. From the targeted model, we can verify the data constraints and detect infinite loops of trigger execution with RODIN. Finally, we take an example for illustration purpose. The proposed tool overcomes the complexity of formal modeling and makes them practical in the development.
