{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T13:18:18Z","timestamp":1769001498646,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T00:00:00Z","timestamp":1697587200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,18]]},"DOI":"10.1145\/3623503.3623536","type":"proceedings-article","created":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T14:34:51Z","timestamp":1697726091000},"page":"2-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal Verification of a Mechanical Ventilator using UPPAAL"],"prefix":"10.1145","author":[{"given":"Jaime","family":"Cuartas","sequence":"first","affiliation":[{"name":"Universidad del Valle, Cali, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Cort\u00e9s","sequence":"additional","affiliation":[{"name":"Universidad del Valle, Cali, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joan S.","family":"Betancourt","sequence":"additional","affiliation":[{"name":"Universidad del Valle, Cali, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas","family":"Aranda","sequence":"additional","affiliation":[{"name":"Universidad del Valle, Cali, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 I.","family":"Garc\u00eda","sequence":"additional","affiliation":[{"name":"Universidad del Valle, Cali, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9s M.","family":"Valencia","sequence":"additional","affiliation":[{"name":"Universidad del Valle, Cali, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Ortiz","sequence":"additional","affiliation":[{"name":"University of Namur, Namur, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563822.3569923"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"e_1_3_2_1_4_1","volume-title":"An Introduction to Numerical Analysis","author":"Atkinson Kendall E.","unstructured":"Kendall E. Atkinson . 1989. An Introduction to Numerical Analysis ( second ed.). John Wiley & Sons , New York . isbn:0471500232 http:\/\/www.worldcat.org\/isbn\/0471500232 Kendall E. Atkinson. 1989. An Introduction to Numerical Analysis (second ed.). John Wiley & Sons, New York. isbn:0471500232 http:\/\/www.worldcat.org\/isbn\/0471500232"},{"key":"e_1_3_2_1_5_1","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier Christel","year":"2026","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking (Representation and Mind Series) . The MIT Press . isbn:026 2026 49X Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press. isbn:026202649X"},{"key":"e_1_3_2_1_6_1","volume-title":"ter Beek, and Vincenzo Ciancia","author":"Basile Davide","year":"2018","unstructured":"Davide Basile , Maurice H. ter Beek, and Vincenzo Ciancia . 2018 . Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC. In Leveraging Applications of Formal Methods, Verification and Validation. Verification, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing , Cham. 372\u2013391. Davide Basile, Maurice H. ter Beek, and Vincenzo Ciancia. 2018. Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC. In Leveraging Applications of Formal Methods, Verification and Validation. Verification, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham. 372\u2013391."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_3_2_1_8_1","volume-title":"A tutorial on Uppaal 4.0. Department of computer science","author":"Behrmann Gerd","unstructured":"Gerd Behrmann , Alexandre David , and Kim G Larsen . 2006. A tutorial on Uppaal 4.0. Department of computer science , Aalborg University . Gerd Behrmann, Alexandre David, and Kim G Larsen. 2006. A tutorial on Uppaal 4.0. Department of computer science, Aalborg University."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1998-36233"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Patricia Bouyer Fran\u00e7ois Laroussinie and Pierre-Alain Reynier. 2005. Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. In International Conference on Formal Modeling and Analysis of Timed Systems. https:\/\/api.semanticscholar.org\/CorpusID:14842124 \t\t\t\t  Patricia Bouyer Fran\u00e7ois Laroussinie and Pierre-Alain Reynier. 2005. Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. In International Conference on Formal Modeling and Analysis of Timed Systems. https:\/\/api.semanticscholar.org\/CorpusID:14842124","DOI":"10.1007\/11603009_10"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028779"},{"key":"e_1_3_2_1_12_1","volume-title":"V\u00edctor Hugo Ibarra Mercado, Enrique Mu\u00f1oz D\u00edaz, and Guillermo Evangelista Benites.","author":"Chapra Steven C","year":"2011","unstructured":"Steven C Chapra , Raymond P Canale , Reyna Susana Garc\u00eda Ruiz , V\u00edctor Hugo Ibarra Mercado, Enrique Mu\u00f1oz D\u00edaz, and Guillermo Evangelista Benites. 2011 . M\u00e9todos num\u00e9ricos para ingenieros. 5, McGraw-Hill New York , NY, USA. Steven C Chapra, Raymond P Canale, Reyna Susana Garc\u00eda Ruiz, V\u00edctor Hugo Ibarra Mercado, Enrique Mu\u00f1oz D\u00edaz, and Guillermo Evangelista Benites. 2011. M\u00e9todos num\u00e9ricos para ingenieros. 5, McGraw-Hill New York, NY, USA."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.engstruct.2009.06.012"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW58534.2023.00021"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_3_2_1_18_1","volume-title":"Modeling of dynamic systems with engineering applications","author":"De Silva Clarence W","unstructured":"Clarence W De Silva . 2017. Modeling of dynamic systems with engineering applications . CRC Press . Clarence W De Silva. 2017. Modeling of dynamic systems with engineering applications. CRC Press."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0140-6736(16)30176-3"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0132-7"},{"key":"e_1_3_2_1_21_1","first-page":"460","article-title":"HyTech: A Model Checker for Hybrid Systems","volume":"1","author":"Henzinger Thomas A.","year":"1997","unstructured":"Thomas A. Henzinger , Pei-Hsin Ho , and Howard Wong-toi. 1997 . HyTech: A Model Checker for Hybrid Systems . Software Tools for Technology Transfer , 1 (1997), 460 \u2013 463 . Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-toi. 1997. HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer, 1 (1997), 460\u2013463.","journal-title":"Software Tools for Technology Transfer"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225162"},{"key":"e_1_3_2_1_23_1","volume-title":"Essentials of mechanical ventilation","author":"Hess Dean R","unstructured":"Dean R Hess and Robert M Kacmarek . 2019. Essentials of mechanical ventilation .. McGraw Hill Education .. Dean R Hess and Robert M Kacmarek. 2019. Essentials of mechanical ventilation.. McGraw Hill Education.."},{"key":"e_1_3_2_1_24_1","volume-title":"Foundations of Health Information Engineering and Systems","author":"Huhn Michaela","unstructured":"Michaela Huhn and Sara Bessling . 2013. Enhancing Product Line Development by Safety Requirements and Verification . In Foundations of Health Information Engineering and Systems , Jens Weber and Isabelle Perseil (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 37\u201354. isbn:978-3-642-39088-3 Michaela Huhn and Sara Bessling. 2013. Enhancing Product Line Development by Safety Requirements and Verification. In Foundations of Health Information Engineering and Systems, Jens Weber and Isabelle Perseil (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 37\u201354. isbn:978-3-642-39088-3"},{"key":"e_1_3_2_1_25_1","volume-title":"Heat and mass transfer","author":"Incropera Frank P","unstructured":"Frank P Incropera and David P DeWitt . 2002. Heat and mass transfer . Fifth John Wiley and Sons , 533\u2013593. Frank P Incropera and David P DeWitt. 2002. Heat and mass transfer. Fifth John Wiley and Sons, 533\u2013593."},{"key":"e_1_3_2_1_26_1","unstructured":"David Ronald Kincaid and Elliott Ward Cheney. 2009. Numerical analysis: mathematics of scientific computing. 2 American Mathematical Soc.. \t\t\t\t  David Ronald Kincaid and Elliott Ward Cheney. 2009. Numerical analysis: mathematics of scientific computing. 2 American Mathematical Soc.."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/FAS-W.2016.34"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1097\/01.ccm.0000165808.30416.ef"},{"key":"e_1_3_2_1_29_1","volume-title":"2nd International Conference on Model-Driven Engineering and Software Development (MODELSWARD). IS\u201311","author":"Larsen Kim G","year":"2014","unstructured":"Kim G Larsen . 2014 . Verification and performance analysis of embedded and cyber-physical systems using UPPAAL . In 2nd International Conference on Model-Driven Engineering and Software Development (MODELSWARD). IS\u201311 . Kim G Larsen. 2014. Verification and performance analysis of embedded and cyber-physical systems using UPPAAL. In 2nd International Conference on Model-Driven Engineering and Software Development (MODELSWARD). IS\u201311."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/DagRep.4.2.17"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2012.25"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1164\/ajrccm\/147.1.5"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1136\/fn.83.1.F64"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1378\/chest.116.suppl_1.9s-a"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artmed.2005.10.006"},{"key":"e_1_3_2_1_36_1","unstructured":"Gloria Toro C\u00f3rdoba Fanny G\u00f3mez and Jos\u00e9 Melo. 2023. Art\u00edculo original producto de la investigaci\u00f3n Design and development of a virtual learning environment in mechanical ventilation with teleoperated practice -VENTYLAB. 01 https:\/\/doi.org\/110.22490\/24629448.6925 \t\t\t\t  Gloria Toro C\u00f3rdoba Fanny G\u00f3mez and Jos\u00e9 Melo. 2023. Art\u00edculo original producto de la investigaci\u00f3n Design and development of a virtual learning environment in mechanical ventilation with teleoperated practice -VENTYLAB. 01 https:\/\/doi.org\/110.22490\/24629448.6925"},{"key":"e_1_3_2_1_37_1","volume-title":"Formal Techniques for Safety-Critical Systems, Cyrille Artho and Peter Csaba \u00d6lveczky (Eds.)","author":"Ain Qurat Ul","unstructured":"Qurat Ul Ain and Osman Hasan . 2019. Formal Timing Analysis of Digital Circuits . In Formal Techniques for Safety-Critical Systems, Cyrille Artho and Peter Csaba \u00d6lveczky (Eds.) . Springer International Publishing , Cham . 84\u2013100. isbn:978-3-030-12988-0 Qurat Ul Ain and Osman Hasan. 2019. Formal Timing Analysis of Digital Circuits. In Formal Techniques for Safety-Critical Systems, Cyrille Artho and Peter Csaba \u00d6lveczky (Eds.). Springer International Publishing, Cham. 84\u2013100. isbn:978-3-030-12988-0"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.15406\/mseij.2022.06.00194"},{"key":"e_1_3_2_1_39_1","first-page":"1","article-title":"Model-based simulation at runtime for self-adaptive systems","volume":"2016","author":"Weyns Danny","year":"2016","unstructured":"Danny Weyns and Usman Iftikhar . 2016 . Model-based simulation at runtime for self-adaptive systems . Proceeding Models at Runtime, W\u00fcrzburg 2016 , 1 \u2013 9 . Danny Weyns and Usman Iftikhar. 2016. Model-based simulation at runtime for self-adaptive systems. Proceeding Models at Runtime, W\u00fcrzburg 2016, 1\u20139.","journal-title":"Proceeding Models at Runtime, W\u00fcrzburg"},{"key":"e_1_3_2_1_40_1","volume-title":"Mustafa Emrah Yildirim, and Hamza \u00dcnsal","author":"Yalcinkaya Fikret","year":"2015","unstructured":"Fikret Yalcinkaya , Mustafa Emrah Yildirim, and Hamza \u00dcnsal . 2015 . Pressure -Volume Controlled Mechanical Ventilator: Modeling and Simulation . Fikret Yalcinkaya, Mustafa Emrah Yildirim, and Hamza \u00dcnsal. 2015. Pressure -Volume Controlled Mechanical Ventilator: Modeling and Simulation."}],"event":{"name":"FTSCS '23: 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems","location":"Cascais Portugal","acronym":"FTSCS '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623503.3623536","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623503.3623536","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:51:01Z","timestamp":1750287061000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623503.3623536"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,18]]},"references-count":40,"alternative-id":["10.1145\/3623503.3623536","10.1145\/3623503"],"URL":"https:\/\/doi.org\/10.1145\/3623503.3623536","relation":{},"subject":[],"published":{"date-parts":[[2023,10,18]]},"assertion":[{"value":"2023-10-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}