Formal Verification of a Mechanical Ventilator using UPPAAL

被引:3
|
作者
Cuartas, Jaime [1 ]
Cortes, David [1 ]
Betancourt, Joan S. [1 ]
Aranda, Jesus [1 ]
Garcia, Jose I. [1 ]
Valencia, Andres M. [1 ]
Ortiz, James [2 ]
机构
[1] Univ Valle, Cali, Colombia
[2] Univ Namur, Namur, Belgium
来源
PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2023 | 2023年
关键词
Timed Automata; Formal Verification; Mechanical Ventilator; TOOL; ART;
D O I
10.1145/3623503.3623536
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Mechanical ventilators are increasingly used for life support of critically ill patients. In this sense, despite recent technological advances, the accurate specification of their properties remains challenging, and the use of formal tools is limited. This work focuses on verifying the properties of the architecture of a mechanical ventilator using UPPAAL as a modeling tool. As a result, the system requirements and specification of a functional prototype were verified and improved using the formal model of a mechanical ventilator. This approach provides a valuable means of ensuring the correctness and reliability of mechanical ventilator systems.
引用
收藏
页码:2 / 13
页数:12
相关论文
共 50 条
  • [41] Formal Verification of a Fuzzy Rule-Based Classifier Using the Prototype Verification System
    Gebreyohannes, Solomon
    Karimoddini, Ali
    Homaifar, Abdollah
    Esterline, Albert
    FUZZY INFORMATION PROCESSING, NAFIPS 2018, 2018, 831 : 1 - 12
  • [42] Formal Sequence: Extending UML Sequence Diagram for Behavior Description and Formal Verification
    Han, Deshuai
    Xing, Jianchun
    Yang, Qiliang
    Wang, Hongda
    Zhang, Xuewei
    PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2, 2016, : 474 - 481
  • [43] Formal Verification of ECCs for Memories Using ACL2
    Mahum Naseer
    Waqar Ahmad
    Osman Hasan
    Journal of Electronic Testing, 2020, 36 : 643 - 663
  • [44] Formal verification of hybrid systems using CheckMate:: A case study
    Silva, BI
    Krogh, BH
    PROCEEDINGS OF THE 2000 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 2000, : 1679 - 1683
  • [45] Methodology for Formal Verification of Hardware Safety Strategies Using SMT
    Faure-Gignoux, Anthony
    Delmas, Kevin
    Gauffriau, Adrien
    Pagetti, Claire
    IEEE EMBEDDED SYSTEMS LETTERS, 2024, 16 (04) : 381 - 384
  • [46] Formal verification of digital circuits using symbolic model checking
    Casar, A
    Brezocnik, Z
    Kapus, T
    INFORMACIJE MIDEM-JOURNAL OF MICROELECTRONICS ELECTRONIC COMPONENTS AND MATERIALS, 2000, 30 (03): : 153 - 160
  • [47] Semantic Web Service Composition Using Formal Verification Techniques
    Kil, Hyunyoung
    Nam, Wonhong
    COMPUTER APPLICATIONS FOR DATABASE, EDUCATION, AND UBIQUITOUS COMPUTING, 2012, 352 : 72 - +
  • [48] Towards Formal Verification of Adaptive Cruise Controller using SpaceEx
    Mishra, Ambuj
    Roy, Subir K.
    2016 INTERNATIONAL CONFERENCE ON VLSI SYSTEMS, ARCHITECTURES, TECHNOLOGY AND APPLICATIONS (VLSI-SATA), 2016,
  • [49] Formal Verification of a Java']Java Component Using the RESOLVE Framework
    Rumreich, Laine
    Sivilotti, Paolo A. G.
    FRONTIERS OF COMBINING SYSTEMS (FROCOS 2021), 2021, 12941 : 287 - 305
  • [50] Towards Formal Verification of Business Process using a Graphical Specification
    El Hichami, Outman
    El Mohajir, Badr Eddine
    Al Achhab, Mohammed
    Berrada, Ismail
    Oucheikh, Rachid
    2014 THIRD IEEE INTERNATIONAL COLLOQUIUM IN INFORMATION SCIENCE AND TECHNOLOGY (CIST'14), 2014, : 12 - 17