{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:22:00Z","timestamp":1770286920837,"version":"3.49.0"},"reference-count":76,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T00:00:00Z","timestamp":1527811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"North Portugal Regional Operational Programme","award":["NORTE 2020"],"award-info":[{"award-number":["NORTE 2020"]}]},{"name":"PORTUGAL 2020 Partnership Agreement, and through the European Regional Development Fund (ERDF)","award":["NORTE-01-0145-FEDER-000016"],"award-info":[{"award-number":["NORTE-01-0145-FEDER-000016"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2018,6,1]]},"DOI":"10.1109\/tse.2017.2694423","type":"journal-article","created":{"date-parts":[[2017,4,14]],"date-time":"2017-04-14T18:31:28Z","timestamp":1492194688000},"page":"512-533","source":"Crossref","is-referenced-by-count":32,"title":["A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems"],"prefix":"10.1109","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1604-4465","authenticated-orcid":false,"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0685-2864","authenticated-orcid":false,"given":"Andrea","family":"Domenici","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0667-7763","authenticated-orcid":false,"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref73","article-title":"Using PVSio-web and SAPERE for rapid prototyping\n of user interfaces in Integrated Clinical Environments","author":"masci","year":"2015","journal-title":"Proc Workshop Verification Assurance Co-Located CAV Verisure"},{"key":"ref72","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","article-title":"Timed automata: Semantics, algorithms and tools","author":"bengtsson","year":"2004","journal-title":"Lectures on Concurrency and Petri Nets"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755967"},{"key":"ref70","doi-asserted-by":"crossref","first-page":"703","DOI":"10.1007\/s10009-012-0237-y","article-title":"Compositional verification of real-time\n systems using ECDAR","volume":"14","author":"david","year":"2012","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1145\/2667218"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2014.12.002"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054291"},{"key":"ref75","first-page":"275","article-title":"Assume-guarantee reasoning for hierarchical hybrid systems.","author":"henzinger","year":"2001","journal-title":"Proc Int Workshop Hybrid Syst Comput Control"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76650-6_7"},{"key":"ref33","first-page":"291","article-title":"Contract-based verification of simulink models","author":"bostr\u00f6m","year":"2011","journal-title":"Formal Methods and Software Engineering - Proc 4th Int Conf on Formal Engineering Methods"},{"key":"ref32","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"de moura and","year":"2008","journal-title":"Proc Theory Practice Softw 14th Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref31","article-title":"This is Boogie 2","author":"leino","year":"2008","journal-title":"Microsoft Research"},{"key":"ref30","first-page":"190","article-title":"Formal verification of discrete-time MATLAB\/simulink models using boogie","author":"reicherdt","year":"2014","journal-title":"Proc of 12th Int Conf on Formal Engineering Methods"},{"key":"ref37","first-page":"407","article-title":"Action versus state based logics for transition systems","author":"de nicola and","year":"1990","journal-title":"Proc Semantics Syst Concurrent Process LITP Spring School Theoretical Comput Sci"},{"key":"ref36","first-page":"323","article-title":"Modeling and verifying hybrid dynamic\n systems using CheckMate","author":"silva","year":"2000","journal-title":"Proc Conf Autom Mixed Process Hybrid Dynam Syst"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1987.13876"},{"key":"ref60","first-page":"1","article-title":"Evaluation of formal IDEs for human-machine\n interface design and analysis: The case of CIRCUS and PVSio-web","author":"fayollas","year":"2016","journal-title":"Proc 3rd Workshop Formal Integr Develop Environ"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.014"},{"key":"ref61","author":"smullyan","year":"1995","journal-title":"First-Order Logic"},{"key":"ref63","first-page":"216","article-title":"Efficient modeling of\n excitable cells using hybrid automata","author":"ye","year":"2005","journal-title":"Proc Conf Computational Methods in Systems Biology"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113834"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49519-3_7"},{"key":"ref65","first-page":"188","article-title":"Modeling and verification of a dual chamber implantable pacemaker","volume":"7214","author":"jiang","year":"2012","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref29","article-title":"SCADE suite® web site.","year":"0"},{"key":"ref67","first-page":"200","article-title":"A\n tutorial on UPPAAL","volume":"3185","author":"behrmann","year":"2004","journal-title":"Proc Int School Formal Methods Des Comput Commun Softw Syst"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"ref69","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"lynch","year":"1989","journal-title":"CWI Quarterly"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_6"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837461"},{"key":"ref20","first-page":"97","author":"larsen","year":"2014","journal-title":"Support for Co-modelling and Co-simulation The Crescendo Tool"},{"key":"ref22","first-page":"22","article-title":"Modelling, simulation and analysis with 20-sim","volume":"38","author":"broenink","year":"1997","journal-title":"J A"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1668862.1668864","article-title":"The Overture Initiative Integrating Tools for VDM","volume":"35","author":"larsen","year":"2010","journal-title":"SIGSOFT Softw Eng Notes"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.819898"},{"key":"ref23","first-page":"238","article-title":"Co-simulation of embedded systems in a heterogeneous MoC-based modeling framework","author":"niaki","year":"2011","journal-title":"Proc IEEE Int Symp Ind Embedded Syst"},{"key":"ref26","article-title":"Simulink Design Verifier® web site.","year":"0"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/43.736561"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2560842"},{"key":"ref51","article-title":"RTLib: A\n library of timed automata for modeling real-time systems","author":"shan","year":"2016"},{"key":"ref59","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/978-3-319-21690-4_30","article-title":"PVSio-web 2.0: Joining PVS to HCI","author":"masci","year":"2015","journal-title":"Proc Comput Aided Verification 27th Int Conf"},{"key":"ref58","article-title":"PVSio-web: A tool for rapid\n prototyping device user interfaces in PVS","volume":"69","author":"oladimeji","year":"2014","journal-title":"Electron Commun EASST"},{"key":"ref57","first-page":"55","article-title":"Integrated\n simulation of implantable cardiac pacemaker software and heart models","author":"bernardeschi","year":"2014","journal-title":"Proc 2nd Int Congress Cardiovascular Technol"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_16"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.17487\/rfc6455"},{"key":"ref54","first-page":"316","author":"castillos","year":"2013","journal-title":"A Compositional Automata-Based Semantics for Property Patterns"},{"key":"ref53","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","article-title":"Specification: The biggest bottleneck in formal methods and\n autonomy","author":"rozier","year":"2016","journal-title":"Proc Int'l Conf Verified Software Theories Tools Experiments"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"key":"ref10","first-page":"5a1-1","article-title":"DAIDALUS: Detect and avoid alerting logic for unmanned systems","author":"mu\u00f1oz","year":"2015","journal-title":"Proc 34th Digital Avionics Syst Conf"},{"key":"ref11","year":"0","journal-title":"Stateflow Reference"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1023\/A:1018913028597","article-title":"TAME: Using PVS strategies for special-purpose theorem proving","volume":"29","author":"archer","year":"2000","journal-title":"Ann Math Artif Intell"},{"key":"ref12","first-page":"105","article-title":"The Functional Mockup Interface for Tool independent\n Exchange of Simulation Models","author":"blochwitz et","year":"2011","journal-title":"Proc 8th Int Modelica Conf"},{"key":"ref13","first-page":"173","article-title":"Functional Mockup Interface 2.0: The Standard\n for Tool independent Exchange of Simulation Models","author":"blochwitz","year":"2012","journal-title":"Proc of the 9th Int Modelica Conf"},{"key":"ref14","first-page":"33","article-title":"Hybridsim: A modeling and co-simulation tool chain for cyber-physical systems","author":"wang","year":"2013","journal-title":"Proc IEEE\/ACM Int Symp Distrib Simul Real-Time Appl"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1177\/0037549714553151"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16265-7_2"},{"key":"ref17","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08766-4","author":"bj\u00f8rner","year":"1978","journal-title":"The Vienna Development Method The Meta-Language"},{"key":"ref18","author":"fitzgerald","year":"2007","journal-title":"The Vienna Development Method"},{"key":"ref19","author":"karnopp","year":"1968","journal-title":"Analysis and Simulation of Multiport Systems The Bond Graph Approach to Physical System Dynamics"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","article-title":"PVS: Combining specification, proof checking, and model checking","author":"owre","year":"1996","journal-title":"Computer-Aided Verification"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2016.02.001"},{"key":"ref6","article-title":"Simulink® web site.","year":"0"},{"key":"ref5","article-title":"Rapid prototyping in PVS","author":"mu\u00f1oz","year":"2003"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/978-3-540-24721-0_17","article-title":"An operational semantics for Stateflow","volume":"2984","author":"hamon","year":"2004","journal-title":"Proc Conf Fundamental Approaches to Software Eng"},{"key":"ref7","article-title":"Scicoslab web site.","year":"0"},{"key":"ref49","first-page":"200","article-title":"Formal verification of medical device user interfaces using PVS","author":"masci","year":"2014","journal-title":"Proc 8th Int Conf Fundam Approaches Softw Eng"},{"key":"ref9","article-title":"Co-simulation: State of the art","author":"gomes","year":"2017","journal-title":"ACM Comput Surveys"},{"key":"ref46","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","article-title":"KeYmaera: A hybrid theorem prover for hybrid systems (system description)","author":"platzer","year":"2008","journal-title":"Proc Int'l Joint Conf Automated Reasoning"},{"key":"ref45","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"PRISM 4.0:\n Verification of probabilistic real-time systems","author":"kwiatkowska","year":"2011","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2494603.2480302"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2161241"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2010.36"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.77"},{"key":"ref43","first-page":"125","article-title":"UPPAAL 4.0","author":"behrmann","year":"2006","journal-title":"Proc 3rd Int Conf Quant Eval Syst"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/8383624\/07900400.pdf?arnumber=7900400","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T03:07:56Z","timestamp":1643166476000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7900400\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,1]]},"references-count":76,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tse.2017.2694423","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6,1]]}}}