Ensuring the Correctness and Reliability of CBPS System Using Event‐B

ABSTRACT During the early phases of software system development, error detection can be challenging due to the complexity of both the requirements and the operating environments. This paper advocates for the utilization of formal modelling and verification throughout the first phases of systems deve...

Full description

Saved in:
Bibliographic Details
Published in:Software testing, verification & reliability verification & reliability, 2025-01, Vol.35 (1), p.n/a
Main Authors: Hussein Toman, Sarah, Hamel, Lazhar, Lahouij, Aida, Hussein Toman, Zinah, Graiet, Mohamed
Format: Article
Language:English
Subjects:
Alarm systems
Communications systems
Complexity
Computer Science
Error correction
Error detection
event‐B
faultless system
Fire alarm systems
IoT communication systems
Modelling
Set theory
software development
Software reliability
Verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:ABSTRACT During the early phases of software system development, error detection can be challenging due to the complexity of both the requirements and the operating environments. This paper advocates for the utilization of formal modelling and verification throughout the first phases of systems development to promptly detect and correct errors. The formalism employed throughout is Event‐B, which is backed by the Rodin toolset. To conquer requirements complexity, the frameworks of set theory and first‐order logic are employed, which provide the necessary tools for formalizing and analysing the properties and behaviours associated with Event‐B. Also, we detail the way in which modelling may be used to achieve ion, as well as the way in which refinement can be used to manage complexity through layering. Furthermore, we emphasize the significance of model validation and verification in improving the precision of formal models and requirements in IoT communication systems. The model is exemplified using a Content‐Based Publish Subscribe System (CBPS), with a special emphasis on a fire alarm system as a motivating example. This paper presents a robust framework using Event‐B for IoT communication systems, emphasizing formal modeling, validation and verification. Key findings demonstrate enhanced reliability and error reduction through automated tools, improving our understanding and development of complex IoT systems.
ISSN:0960-0833
1099-1689
DOI:10.1002/stvr.1904