Publications

Export 55 results:
Author Title Type [ Year(Desc)]
2015
Comparing model checkers for timed UML activity diagrams, Daw, Zamira, and Cleaveland Rance , Sci. Comput. Program., Volume 111, p.277–299, (2015)  (2.93 MB)
An Extensible Operational Semantics for UML Activity Diagrams, Daw, Zamira, and Cleaveland Rance , Software Engineering and Formal Methods - 13th International Conference, {SEFM} 2015, York, UK, September 7-11, 2015. Proceedings, (2015)
High-Confidence Medical Device Software Development, Jiang, Z., and Mangharam R. , Foundations and Trends in Electronic Design Automation, Volume 9, (2015)  (14.77 MB)
SpaTeL: A Novel Spatial-temporal Logic and Its Applications to Networked Systems, Haghighi, Iman, Jones Austin, Kong Zhaodan, Bartocci Ezio, Grosu Radu, and Belta Calin , Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, New York, NY, USA, (2015)  (679.39 KB)
System design of stochastic models using robustness of temporal properties, Bartocci, Ezio, Bortolussi Luca, Nenzi Laura, and Sanguinetti Guido , Theoretical Computer Science, Volume 587, p.3 - 25, (2015)  (1.57 MB)
2016
Automated Closed-Loop Model Checking of Implantable Pacemakers using Abstraction Trees, Jiang, Zhihao, Abbas Houssam, Mosterman Pieter J., and Mangharam Rahul , Medical Cyber Physical Systems Workshop 2016, (2016)  (2.85 MB)
Bifurcation Analysis of Cardiac Alternans Using δ -Decidability., Islam, Md. Ariful, Byrne Greg, Kong Soonho, Clarke Edmund M., Cleaveland Rance, Fenton Flavio H., Grosu Radu, Jones Paul L., and Smolka Scott A. , CMSB, (2016)  (795.28 KB)
The Challenges of High-Confidence Medical Device Software, Jiang, Z., Abbas H., Jang K., and Mangharam R. , IEEE Computer January Outlook, (2016)  (726.87 KB)
Estimability Analysis and Optimal Design in Dynamic Multi-scale Models of Cardiac Electrophysiology, Shotwell, Matthew S., and Gray Richard A. , Journal of Agricultural, Biological, and Environmental Statistics, p.1–16, (2016)
Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus, Ganesan, D., Lindvall M., Hafsteinsson S., Cleaveland R., Strege S. L., and Moleski W. , 2016 IEEE 27th International Symposium on Software Reliability Engineering (ISSRE), Oct, (2016)  (976.61 KB)
A framework for decentralized opacity in linear systems, Ramasubramanian, B., Cleaveland R., and Marcus S. I. , 2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton), Sept, (2016)  (564.69 KB)
A framework for opacity in linear systems, Ramasubramanian, Bhaskar, Cleaveland Rance, and Marcus Steven I. , 2016 American Control Conference, {ACC} 2016, Boston, MA, USA, July 6-8, 2016, (2016)  (159.19 KB)
High-level modeling for computer-aided clinical trials of medical devices, Abbas, Houssam, Jiang Zhihao, Jang Kuk Jin, Beccani Marco, Liangy Jackson, and Mangharam Rahul , High Level Design Validation and Test Workshop (HLDVT), 2016 IEEE International, (2016)  (4.01 MB)
In-silico pre-clinical trials for implantable cardioverter defibrillators, Jiang, Zhihao, Abbas Houssam, Jang Kuk Jin, Beccani Marco, Liang Jackson, Dixit Sanjay, and Mangharam Rahul , Engineering in Medicine and Biology Society (EMBC), 2016 IEEE 38th Annual International Conference of the, (2016)  (4.99 MB)
SHARP BOUNDARY ELECTROCARDIAC SIMULATIONS, XUE, SHUAI, LIM HYUNKYUNG, GLIMM JAMES, FENTON FLAVIO H., and CHERRY ELIZABETH M. , Stony Brook, (2016)  (725.88 KB)
Towards Model Checking of Implantable Cardioverter Defibrillators, Abbas, Houssam, Jiang Kuk Jin, Jiang Zhihao, and Mangharam Rahul , Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, New York, NY, USA, (2016)  (1.87 MB)
2017
Alternans promotion in cardiac electrophysiology models by delay differential equations, Gomes, Johnny M., Santos Rodrigo Weber dos, and Cherry Elizabeth M. , Chaos: An Interdisciplinary Journal of Nonlinear Science, Volume 27, p.093915, (2017)
Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees, Ferlez, James, Cleaveland Rance, and Marcus Steven I. , Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, {EXPRESS/SOS} 2017, Berlin, Germany, 4th September 2017., (2017)  (254.08 KB)
Closed-loop quantitative verification of rate-adaptive pacemakers, Paoletti, Nicola, Patanè Andrea, and Kwiatkowska Marta , ACM Transactions on Cyber-Physical Systems, to appear, (2017)
Corrections to "A Menagerie of Timed Automata", Keiren, Jeroen J. A., Fontana Peter, and Cleaveland Rance , ACM Comput. Surv., Volume 50, p.42:1–42:8, (2017)  (221.78 KB)
Data assimilation for cardiac electrical dynamics, Cherry, E. M., Cairns D. I., Holt N., LaVigne N. S., Fenton F. H., and Hoffman M. J. , Proceedings of the 5th {International} {Conference} on {Computational} and {Mathematical} {Biomedical} {Engineering}, Pittsburgh, PA, (2017)
Data-Driven Robust Control for Type 1 Diabetes Under Meal and Exercise Uncertainties, Paoletti, Nicola, Liu Kin Sum, Smolka Scott A., and Lin Shan , Computational Methods in Systems Biology, (2017)
Distinguishing mechanisms for alternans in cardiac cells using constant-diastolic-interval pacing, Cherry, Elizabeth M. , Chaos: An Interdisciplinary Journal of Nonlinear Science, Volume 27, p.093902, (2017)
Effects of model error on cardiac electrical wave state reconstruction using data assimilation, LaVigne, Nicholas S., Holt Nathan, Hoffman Matthew J., and Cherry Elizabeth M. , Chaos: An Interdisciplinary Journal of Nonlinear Science, Volume 27, p.093911, (2017)
Efficient parameterization of cardiac action potential models using a genetic algorithm, Cairns, Darby I., Fenton Flavio H., and Cherry E. M. , Chaos: An Interdisciplinary Journal of Nonlinear Science, Volume 27, p.093922, (2017)

Pages