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 条

[31] Formal Verification of the Pastry Protocol Using TLA+
Lu, Tianxiang
DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015, 2015, 9409 : 284 - 299
[32] FORMAL VERIFICATION OF CONTRACTUAL SOFTWARE ARCHITECTURES USING SPIN
Ozkaya, Mert
MALAYSIAN JOURNAL OF COMPUTER SCIENCE, 2015, 28 (04) : 318 - 337
[33] Formal Verification of Graph Grammars using Mathematical Induction
da Costa, Simone Andre
Ribeiro, Leila
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 43 - 60
[34] Formal verification of concurrent programs using the Larch prover
Chetali, B
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (01) : 46 - 62
[35] Formal verification of simulation traces using computation slicing
Sen, Alper
Garg, Vijay K.
IEEE TRANSACTIONS ON COMPUTERS, 2007, 56 (04) : 511 - 527
[36] Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems
Boudjadar, Abdeldjalil
Vaandrager, Frits
Bodeveix, Jean-Paul
Filali, Mamoun
FUNDAMENTALS OF SOFTWARE ENGINEERING, FSEN 2013, 2013, 8161 : 111 - 132
[37] Formal Verification of a Keystore
Boender, Jaap
Badevic, Goran
THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 49 - 64
[38] Formal Verification of Websites
Flores, Sonia
Lucas, Salvador
Villanueva, Alicia
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) : 103 - 118
[39] Formal verification of μ-charts
Goldson, D
APSEC 2002: NINTH ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, 2002, : 129 - 136
[40] Formal Verification of Ptolemy Discrete Event Model
Lu Z.-H.
Wang R.
Kong H.
Guan Y.
Shi Z.-P.
Wang, Rui (rwang04@cnu.edu.cn), 1830, Chinese Academy of Sciences (32): : 1830 - 1848

← 1 2 3 4 5 →