A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems

masci, 2015, Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments, Proc Workshop Verification Assurance Co-Located CAV Verisure

bengtsson, 2004, Timed automata: Semantics, algorithms and tools, Lectures on Concurrency and Petri Nets, 87, 10.1007/978-3-540-27755-2_3

10.1145/1755952.1755967

david, 2012, Compositional verification of real-time systems using ECDAR, Int J Softw Tools Technol Transfer, 14, 703, 10.1007/s10009-012-0237-y

10.1145/2667218

10.1016/j.pmcj.2014.12.002

10.1007/BFb0054291

henzinger, 2001, Assume-guarantee reasoning for hierarchical hybrid systems., Proc Int Workshop Hybrid Syst Comput Control, 275

10.1007/978-3-540-76650-6_7

boström, 2011, Contract-based verification of simulink models, Formal Methods and Software Engineering - Proc 4th Int Conf on Formal Engineering Methods, 291

de moura and, 2008, Z3: An Efficient SMT Solver, Proc Theory Practice Softw 14th Int Conf Tools Algorithms Construction Anal Syst, 337

leino, 2008, This is Boogie 2, Microsoft Research

reicherdt, 2014, Formal verification of discrete-time MATLAB/simulink models using boogie, Proc of 12th Int Conf on Formal Engineering Methods, 190

de nicola and, 1990, Action versus state based logics for transition systems, Proc Semantics Syst Concurrent Process LITP Spring School Theoretical Comput Sci, 407

silva, 2000, Modeling and verifying hybrid dynamic systems using CheckMate, Proc Conf Autom Mixed Process Hybrid Dynam Syst, 323

10.1007/978-1-4612-1674-2

10.1109/PROC.1987.13876

fayollas, 2016, Evaluation of formal IDEs for human-machine interface design and analysis: The case of CIRCUS and PVSio-web, Proc 3rd Workshop Formal Integr Develop Environ, 1

10.1016/j.ic.2014.01.014

smullyan, 1995, First-Order Logic

ye, 2005, Efficient modeling of excitable cells using hybrid automata, Proc Conf Computational Methods in Systems Biology, 216

10.1145/1113830.1113834

10.1109/LICS.1996.561342

10.1007/3-540-49519-3_7

jiang, 2012, Modeling and verification of a dual chamber implantable pacemaker, Proc Int Conf Tools Algorithms Construction Anal Syst, 7214, 188

10.1016/0304-3975(94)90010-8

0, SCADE suite® web site.

behrmann, 2004, A tutorial on UPPAAL, Proc Int School Formal Methods Des Comput Commun Softw Syst, 3185, 200

10.1006/inco.1994.1045

lynch, 1989, An introduction to input/output automata, CWI Quarterly, 2, 219

10.1007/3-540-44659-1_6

10.1145/1837274.1837461

larsen, 2014, Support for Co-modelling and Co-simulation The Crescendo Tool, 97

broenink, 1997, Modelling, simulation and analysis with 20-sim, J A, 38, 22

larsen, 2010, The Overture Initiative Integrating Tools for VDM, SIGSOFT Softw Eng Notes, 35, 1, 10.1145/1668862.1668864

10.1109/TCAD.2003.819898

niaki, 2011, Co-simulation of embedded systems in a heterogeneous MoC-based modeling framework, Proc IEEE Int Symp Ind Embedded Syst, 238

0, Simulink Design Verifier® web site.

10.1109/43.736561

10.1109/TSE.2016.2560842

shan, 2016, RTLib: A library of timed automata for modeling real-time systems

masci, 2015, PVSio-web 2.0: Joining PVS to HCI, Proc Comput Aided Verification 27th Int Conf, 470, 10.1007/978-3-319-21690-4_30

oladimeji, 2014, PVSio-web: A tool for rapid prototyping device user interfaces in PVS, Electron Commun EASST, 69

bernardeschi, 2014, Integrated simulation of implantable cardiac pacemaker software and heart models, Proc 2nd Int Congress Cardiovascular Technol, 55

10.1007/978-3-319-06200-6_16

10.17487/rfc6455

castillos, 2013, A Compositional Automata-Based Semantics for Property Patterns, 316

rozier, 2016, Specification: The biggest bottleneck in formal methods and autonomy, Proc Int'l Conf Verified Software Theories Tools Experiments, 8, 10.1007/978-3-319-48869-1_2

10.1145/298595.298598

muñoz, 2015, DAIDALUS: Detect and avoid alerting logic for unmanned systems, Proc 34th Digital Avionics Syst Conf, 5a1-1

0, Stateflow Reference

archer, 2000, TAME: Using PVS strategies for special-purpose theorem proving, Ann Math Artif Intell, 29, 139, 10.1023/A:1018913028597

blochwitz et, 2011, The Functional Mockup Interface for Tool independent Exchange of Simulation Models, Proc 8th Int Modelica Conf, 105

blochwitz, 2012, Functional Mockup Interface 2.0: The Standard for Tool independent Exchange of Simulation Models, Proc of the 9th Int Modelica Conf, 173

wang, 2013, Hybridsim: A modeling and co-simulation tool chain for cyber-physical systems, Proc IEEE/ACM Int Symp Distrib Simul Real-Time Appl, 33

10.1177/0037549714553151

10.1007/978-3-642-16265-7_2

bjørner, 1978, The Vienna Development Method The Meta-Language, 10.1007/3-540-08766-4

fitzgerald, 2007, The Vienna Development Method

karnopp, 1968, Analysis and Simulation of Multiport Systems The Bond Graph Approach to Physical System Dynamics

owre, 1996, PVS: Combining specification, proof checking, and model checking, Computer-Aided Verification, 411, 10.1007/3-540-61474-5_91

10.1016/j.ipl.2016.02.001

0, Simulink® web site.

muñoz, 2003, Rapid prototyping in PVS

hamon, 2004, An operational semantics for Stateflow, Proc Conf Fundamental Approaches to Software Eng, 2984, 229, 10.1007/978-3-540-24721-0_17

0, Scicoslab web site.

masci, 2014, Formal verification of medical device user interfaces using PVS, Proc 8th Int Conf Fundam Approaches Softw Eng, 200

gomes, 2017, Co-simulation: State of the art, ACM Comput Surveys

platzer, 2008, KeYmaera: A hybrid theorem prover for hybrid systems (system description), Proc Int'l Joint Conf Automated Reasoning, 171, 10.1007/978-3-540-71070-7_15

kwiatkowska, 2011, PRISM 4.0: Verification of probabilistic real-time systems, Proc Int Conf Comput Aided Verification, 585, 10.1007/978-3-642-22110-1_47

10.1145/2494603.2480302

10.1007/978-3-319-21401-6_36

10.1109/JPROC.2011.2161241

10.1109/ECRTS.2010.36

10.1109/RTSS.2012.77

behrmann, 2006, UPPAAL 4.0, Proc 3rd Int Conf Quant Eval Syst, 125