About | Contact Us | Register | Login
ProceedingsSeriesJournalsSearchEAI
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

Research Article

Trigger2B: A Tool Generating Event-B Models from Database Triggers

Download(Requires a free EAI acccount)
2 downloads
Cite
BibTeX Plain Text
  • @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
Hong Anh Le1,*
  • 1: Hanoi University of Mining and Geology, 18 Pho Vien
*Contact email: lehonganh@humg.edu.vn

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.

Keywords
Trigger Event-B Formal modeling Generation
Published
2021-01-13
Appears in
SpringerLink
http://dx.doi.org/10.1007/978-3-030-67101-3_8
Copyright © 2020–2025 ICST
EBSCOProQuestDBLPDOAJPortico
EAI Logo

About EAI

  • Who We Are
  • Leadership
  • Research Areas
  • Partners
  • Media Center

Community

  • Membership
  • Conference
  • Recognition
  • Sponsor Us

Publish with EAI

  • Publishing
  • Journals
  • Proceedings
  • Books
  • EUDL