[Home ] [Archive]   [ فارسی ]  
:: Main :: About :: Current Issue :: Archive :: Search :: Submit :: Contact ::
Main Menu
Journal Information::
Articles archive::
Publication Ethics::
Peer Review Process::
Indexing Databases::
For Authors::
For Reviewers::
Contact us::
Site Facilities::
Google Scholar Metrics

Citation Indices from GS

AllSince 2019

Search in website

Advanced Search
Receive site information
Enter your Email in the following box to receive the site news and information.
Registered in



:: Volume 23, Issue 3 (9-2015) ::
Journal of Ilam University of Medical Sciences 2015, 23(3): 84-96 Back to browse issues page
Proposing a Formal Approach for Verification of Heart-Lung Machine
Reza Rafeh * 1
1- Arak University , r-rafeh@araku.ac.ir
Abstract:   (6299 Views)

Introduction: error occurrence in computer systems, can lead to irreparable damage, especially those used in medical systems. As a result, verification of such systems is important. Model checking as a method is used to ensure the absence of errors in the model. The heart-lung machine is used in surgeries in which heart must stop working and assumes the heart and lungs duties. In this article, a formal approach is to verify the operation of the heart-lung machine.
Methods: The heart-lung machine has been modeled by using the UPPAAL tool which supports time automatic machine, since, this machine do three sets operations in parallel which has been modeled in three subsystems: system overall performance machine, heparin injection machine and cardioplegia solution delivery machine.
 Finding: After modeling by a complete search on state space of model, the most important characteristics of system were verified. Situations were identified which cause entering the system to unsecure states. The reachability of all important states of the system was investigated. Finally, we ensured about system accuracy features and the system operates correctly.
Conclusion: Modelling is a cheap way to study a system and evaluate its reaction to environmental changes before implementation of the system. Considering to importance of heart-lung machine in surgeries, in this research a formal model has been presented to verify the operation of this machine.

Keywords: Model Checking, Heart-Lung Machine, time automatic machine, UPPAAL, System Verification.
Full-Text [PDF 841 kb]   (2150 Downloads)    
Type of Study: Research | Subject: gardiologist
Received: 2014/03/28 | Accepted: 2014/07/21 | Published: 2015/09/27
Send email to the article author

Add your comments about this article
Your username or Email:


XML   Persian Abstract   Print

Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:

Rafeh R. Proposing a Formal Approach for Verification of Heart-Lung Machine. J. Ilam Uni. Med. Sci. 2015; 23 (3) :84-96
URL: http://sjimu.medilam.ac.ir/article-1-1680-en.html

Rights and permissions
Creative Commons License This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
Volume 23, Issue 3 (9-2015) Back to browse issues page
مجله دانشگاه علوم پزشکی ایلام Journal of Ilam University of Medical Sciences
Persian site map - English site map - Created in 0.16 seconds with 41 queries by YEKTAWEB 4643