We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
A graphical tool for formal verification using Event-B modeling.
- Authors
Karmakar, Rahul
- Abstract
Event-B is a formal method for describing and verifying systems at the system level. It enables a refining technique to design the system incrementally. Using Event-B notations to define system requirements can be quite abstract for complex requirements. The primary Event-B components uphold several relationships with context, machines, and events. The RODIN is the standard tool support to verify Event-B models. Using RODIN can sometimes be difficult when building the models and maintaining all the relationships. Leveraging the system's graphical depiction would be preferable. In this paper, we provide a web-based graphical assistance tool. Graphic representations are offered for the components of Event-B. The refinement relationships between the components are automatically generated by the tool's first module, G2E. It upholds the stated sequence of events. The component relationships of the Event-B model can be graphically defined in a single window, and the Event-B files are generated automatically. An executable Python class is produced by the second module (E2P) for further verification. The suggested module encourages early verification of crucial criteria while allowing for design flexibility through autonomous code generation. A district healthcare model is designed for Covid19 management using the proposed frameworks and verified.
- Subjects
DESIGN techniques; COVID-19; PYTHON programming language; PYTHONS
- Publication
Multimedia Tools & Applications, 2024, Vol 83, Issue 4, p10899
- ISSN
1380-7501
- Publication type
Article
- DOI
10.1007/s11042-023-15993-8