@conference {, title = {Safe CPS from Unsafe Controllers}, booktitle = {Proceedings of CAADSPC 2001, the 2021 CPS-IoT Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems}, year = {2021}, month = {06/2021}, author = {U. Mehmood and S. Bak and S. A. Smolka and S. D. Stoller} } @article {, title = {Single-variable delay-differential equation approximations of the Fitzhugh-Nagumo and Hodgkin-Huxley models}, journal = {Communications in Nonlinear Science and Numerical Simulation}, volume = {82}, year = {2020}, pages = {105066}, doi = {10.1016/j.cnsns.2019.105066}, url = {https://doi.org/10.1016/j.cnsns.2019.105066}, author = {Raffael Bechara Rameh and ELIZABETH M. CHERRY and Rodrigo Weber dos Santos} } @article {, title = {Swarm Model Checking on the GPU}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2020}, author = {R. DeFrancisco and S. Cho and M. Ferdman and S. A. Smolka} } @inbook {, title = {Scott Smolka and Me}, booktitle = {From Reactive Systems to Cyber-Physical Systems}, year = {2019}, pages = {1{\textendash}6}, publisher = {Springer, Cham}, organization = {Springer, Cham}, author = {Cleaveland, Rance} } @article {, title = {Simulating waves, chaos and synchronization with a microcontroller}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {29}, year = {2019}, month = {12/2019}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&cstart=20\&pagesize=80\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:BUYA1_V_uYcC}, author = {Andrea J Welsh and Cristian Delgado and Casey Lee-Trimble and Abouzar Kaboudian and Flavio H Fenton} } @article {, title = {Spatiotemporal correlation uncovers characteristic lengths in cardiac tissue}, journal = {Physical Review E}, volume = {100}, year = {2019}, doi = {10.1103/physreve.100.020201}, url = {https://doi.org/10.1103/physreve.100.020201}, author = {Alessandro Loppini and Alessio Gizzi and Christian Cherubini and ELIZABETH M. CHERRY and FLAVIO H. FENTON and Simonetta Filippi} } @article {, title = {Simultaneous Quantification of Spatially Discordant Alternans in Voltage and Intracellular Calcium in Langendorff-Perfused Rabbit Hearts and Inconsistencies with Models of Cardiac Action Potentials and Ca Transients}, journal = {Frontiers in Physiology}, volume = {8}, year = {2017}, doi = {10.3389/fphys.2017.00819}, url = {https://doi.org/10.3389/fphys.2017.00819}, author = {Ilija Uzelac and Yanyan C. Ji and Daniel Hornung and Johannes Schr{\"o}der-Scheteling and Stefan Luther and Richard A. Gray and ELIZABETH M. CHERRY and FLAVIO H. FENTON} } @conference {, title = {{SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems}}, booktitle = {Haifa Verification Conference, to appear}, year = {2017}, abstract = {

Abstract. We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitzcontinuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.

}, author = {Fedor Shmarov and Nicola Paoletti and Ezio Bartocci and Shan Lin and Scott Smolka and Paolo Zuliani} } @article {, title = {SHARP BOUNDARY ELECTROCARDIAC SIMULATIONS}, year = {2016}, address = {Stony Brook}, abstract = {

We present a sharp boundary electrocardiac simulation model based on the finite volume embedded boundary method for the solution of voltage dynamics in irregular domains with anisotropy and a high degree of anatomical detail. This method is second order accurate uniformly up to boundaries and is able to resolve small features without the use of fine meshes. This capability is necessary to enable the repeated simulations required for future verification and validation and uncertainty quantification studies of defibrillation, where fine-scale heterogeneities, such as those formed by small blood vessels, play an important role and require resolution.

}, keywords = {cardiac electrophysiology, embedded boundary method, tensor diffusion}, doi = {10.1137/15M1019283}, author = {SHUAI XUE and HYUNKYUNG LIM and JAMES GLIMM and FLAVIO H. FENTON and ELIZABETH M. CHERRY} } @article {, title = {Security assurance cases for medical cyber{\textendash}physical systems}, journal = {IEEE Design \& Test}, volume = {32}, year = {2015}, pages = {56{\textendash}65}, author = {Ray, Arnab and Cleaveland, Rance} } @conference {21, title = {SpaTeL: A Novel Spatial-temporal Logic and Its Applications to Networked Systems}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, year = {2015}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, keywords = {networked dynamical systems, parameter synthesis, spatial temporal logic, statistical model checking}, isbn = {978-1-4503-3433-4}, doi = {10.1145/2728606.2728633}, url = {http://doi.acm.org/10.1145/2728606.2728633}, author = {Haghighi, Iman and Jones, Austin and Kong, Zhaodan and Bartocci, Ezio and Grosu, Radu and Belta, Calin} } @article {, title = {System design of stochastic models using robustness of temporal properties}, journal = {Theoretical Computer Science}, volume = {587}, year = {2015}, pages = {3 - 25}, abstract = {

Abstract Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem, i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to maintain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness degrees. By discussing three examples, we show how to approximate the distribution of the robustness degree and the average robustness. Secondly, we show how to exploit this notion to address the system design problem, where the goal is to optimise some control parameters of a stochastic model in order to maximise robustness of the desired specifications.

}, keywords = {Temporal logic}, issn = {0304-3975}, doi = {http://dx.doi.org/10.1016/j.tcs.2015.02.046}, url = {http://www.sciencedirect.com/science/article/pii/S0304397515002224}, author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi and Guido Sanguinetti} }