LTL Model Checking for Verification of Electronic Medical Record (EMR) Design

This paper presents an in-depth investigation into the verification of a software design model, focusing on the context of Electronic Medical Record (EMR) systems. Verification plays a critical role in ensuring the correctness and reliability of such systems, making it a topic of paramount importance. In this study, we undertake the task of remodeling the EMR requirements using a finite transition system to facilitate rigorous analysis and verification. Additionally, we express the formal specification through Linear Temporal Logic (LTL), leveraging its expressive power and ability to capture temporal properties accurately. To assess the validity of the design model, we employ the widely recognized SPIN model checker, a tool known for its effectiveness in detecting errors and inconsistencies in software systems. Our analysis reveals several critical findings. Specifically, the model checker successfully identifies paths within the design model that fail to satisfy the specified LTL formula, shedding light on potential areas of concern. Moreover, the generation of a comprehensive counterexample provides valuable insights for further analysis and improvement of the software design. Overall, this research highlights the significance of verification techniques in software design and emphasizes the applicability of the finite transition system and LTL in this context. The findings underscore the importance of thorough verification and the potential benefits of employing tools like SPIN to enhance the reliability and robustness of EMR systems.