Formal Modeling and Verification of Healthcare Systems Requirements Based on Simulation and Hoare Logic

Authors

  • Naima Beladam University of RELIZANE
  • Abdelghani Ghomari University Oran1 Ahmed Ben Bella

DOI:

https://doi.org/10.13053/cys-29-1-5140

Keywords:

Healthcare systems, formal specification, formal verification, Hoare logic, dental department

Abstract

This paper proposes a new approach to formal modeling and verification of healthcare systems based on simulation and using Hoare Logic, with a focus on the dental department of an Algerian hospital. We have proposed inference rules inspired by Hoare Logic, adapted for the formal specification and verification of healthcare systems. The methodology includes the creation of a conceptual model incorporating these rules, followed by the simulation of this model to analyze and improve healthcare system performance. The obtained results of our case study show that the proposed approach allows healthcare professionals to identify inefficiencies, optimize resource utilization, reduce patient waiting times, and ensure the reliability of healthcare systems. This research paper demonstrates the effectiveness of integrating Hoare Logic inference rules into simulation processes to improve healthcare systems performance and support healthcare professionals' decision-making. 

Downloads

Published

2025-03-27

Issue

Vol. 29 No. 1 (2025): 29(1) 2025

Section

Articles

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.