| MD CPS: Medical Device Cyber Physical Systems |
Research Publications
OpenICE-lite: Towards a Connectivity Platform for the Internet of Medical Things. Radoslav Ivanov, Hung Nguyen, James Weimer, Oleg Sokolsky, and Insup Lee. In Proceedings of IEEE ISORC 2018, Singapore, May 2018.
Context-Aware Detection in Medical Cyber-Physical Systems. Radoslav Ivanov, James Weimer, and Insup Lee. In Proceedings of 9th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2018), Porto, Portugal, April 2018.
Data-driven Adaptive Safety Monitoring using Virtual Subjects in Medical Cyber-Physical Systems: A Glucose Control Case Study. Sanjian Chen, Oleg Sokolsky, James Weimer, and Insup Lee. In Journal of Computer Science and Engineering, Volume 10, Num.3, pp.75-84, September 2016 (Open Access).
Clinician-in-the-Loop Annotation of ICU Bedside Alarm Data. Alexander Roederer, Joseph Dimartino, Jacob Gutsche, Margaret Mullen-Fortino, Sachin Shah, C. William Hanson III, and Insup Lee. In Proceedings of First IEEE Conference on Connected Health Applications, Systems and Engineering Technologies (IEEE CHASE 2016), Washington, DC, June 2016.
Cloud-Based Secure Logger for Medical Devices. Hung Nguyen, Bipeen Acharya, Radoslav Ivanov, Andreas Haeberlen, Linh T.X. Phan, Oleg Sokolsky, Jesse Walker, James Weimer, C. William Hanson III, and Insup Lee. In Proceedings of IEEE First International Conference on Connected Health: Applications, Systems and Engineering Technologies (CHASE 2016), Washington, DC, USA, June 2016.
Estimation of Blood Oxygen Content Using Context-Aware Filtering. Radoslav Ivanov, Nikolay Atanasov, James Weimer, Miroslav Pajic, Allan Simpao, Mohamed Rehman, George Pappas and Insup Lee. In Proceedings of 7th International Conference on Cyber-Physical Systems (ICCPS 2016), Vienna, Austria, April 2016.
Protecting interoperable clinical environment with authentication. Liang Cheng, Zhangtan Li, Yi Zhang, Yang Zhang, Insup Lee. In Proceedings of Medical CPS workshop 2016, Vienna, Austria, April 2016. Also published in SIGBED Review Vol. 14, Num. 2, February 2017
Representation of Confidence in Assurance Cases using the Beta Distribution. Lian Duan, Sanjai Rayadurgam, Mats Heimdahl, Oleg Sokolsky, and Insup Lee. In Proceedings of IEEE High Assurance Systems Engineering Symposium (HASE 2016), Orlando, Florida, USA, January 2016.
Platform-Specific Code Generation from Platform-Independent Timed Models. BaekGyu Kim, Lu Feng, Oleg Sokolsky and Insup Lee. In IEEE Real-Time Systems Symposium (RTSS 2015), San Antonio, TX, USA, December 2015.
Executing Model-based Tests on Platform-specific Implementations. Dongjiang You, Sanjai Rayadurgam, Mats P.E. Heimdahl, John Komp, BaekGyu Kim and Oleg Sokolsky. In 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015), Lincoln, NE, USA, November 2015.
Parameter-Invariant Design of Medical Alarms. James Weimer, Radoslav Ivanov, Alexander Roederer, Sanjian Chen, and Insup Lee. In IEEE Design & Test, Volume 32, Issue 5, pp 9-16, October 2015.
A Data-Driven Behavior Modeling and Analysis Framework for Diabetic Patients on Insulin Pumps. Sanjian Chen, Lu Feng, Michael R. Rickels, Amy Peleckis, Oleg Sokolsky, and Insup Lee. In IEEE International Conference on Healthcare Informatics 2015 (ICHI 2015), Dallas, TX, USA, October 2015.
An Intraoperative Glucose Control Benchmark for Formal Verification. Sanjian Chen, Matthew O'Kelly, James Weimer, Oleg Sokolsky, and Insup Lee. In 5th IFAC conference on Analysis and Design of Hybrid Systems (ADHS 2015), Atlanta, GA, USA, October 2015.
A Hybrid Approach to Causality Analysis. Shaohui Wang, Yoann Geo ffroy, Gregor Gossler, Oleg Sokolsky, and Insup Lee. In 15th International Conference on Runtime Verification (RV 2015), Vienna, Austria, September 2015.
Requirement Engineering for Functional Alarm System for Interoperable Medical Devices. Krishna K. Venkatasubramanian, Eugene Y. Vasserman, Vasiliki Sfyrla, Oleg Sokolsky, and Insup Lee. In International Conference on Computer Safety, Reliability & Security (SEFECOMP 2015), Delft, the Netherlands, September 2015.
Towards Assurance for Plug & Play Medical Systems. Andrew L. King, Lu Feng, Sam Procter, Sanjian Chen, Oleg Sokolsky, John Hatcliff, and Insup Lee. In International Conference on Computer Safety, Reliability & Security (SEFECOMP 2015), Delft, the Netherlands, September 2015.
Robust Monitoring of Hypovolemia in Intensive Care Patients using Photoplethysmogram Signals. Alexander Roederer, James Weimer, Joseph DiMartino, Jacob Gutsche, Insup Lee. In 37th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC 2015), Milan, Italy, August 2015.
Towards Non-Invasive Monitoring of Hypovolemia in Intensive Care Patients. Alexander Roederer, James Weimer, Joseph Dimartino, Jacob Gutsche, and Insup Lee. In 6th Workshop on Medical Cyber-Physical Systems (MedicalCPS 2015), Seattle, WA, April 2015.
Towards a Model-Based Meal Detector for Type I Diabetics. Sanjian Chen, James Weimer, Michael Rickels, Amy Peleckis and Insup Lee. In 6th Workshop on Medical Cyber-Physical Systems (MedicalCPS 2015), Seattle, WA, April 2015.
Early Detection of Critical Pulmonary Shunts in Infants. Radoslav Ivanov, James Weimer, Allan Simpao, Mohamed Rehman, and Insup Lee. In Proceedings of 6th International Conference on Cyber-Physical Systems (ICCPS 2015), Seattle, WA, April 2015.
Prediction of Significant Vasospasm in Aneurysmal Subarachnoid Hemorrhage Using Automated Data. Alexander Roederer, John H. Holmes, Michelle J. Smith, Insup Lee, Soojin Park. In Neurocrit Care, Vol. 21, Num. 3, pp. 444-50, December 2014.
Safety-critical Medical Device Development using the UPP2SF Model Translation Tool. M. Pajic, Z. Jiang, O. Sokolsky, I. Lee and R. Mangharam. In ACM Transactions on Embedded Computing, Volume 13 Issue 4s, Article No. 127, July 2014.
From Requirements to Code: Model Based Development of A Medical Cyber Physical System. Anitha Murugesan, Michael Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, Mats Heimdahl, Baek-Gyu Kim, Oleg Sokolsky and Insup Lee. In Proceedings of Joint event of the Fourth Symposium on Foundations of Health Information Engineering and Systems (FHIES) and the Software Engineering in Healthcare (SEHC) workshop (FHIES/SEHC '14), Washington, D.C., July 2014.
The MIDdleware Assurance Substrate: Enabling Strong Real-Time Guarantees in Open Systems with OpenFlow. Andrew L. King, Sanjian Chen, and Insup Lee. In Proceedings of 17th IEEE Computer Society symposium on object/component/service-oriented realtime distributed computing (ISORC 2014), Reno, Nevada, USA, June 2014.
Functional Alarms for Systems of Interoperable Medical Devices. Krishna K. Venkatasubramanian, Eugene Y. Vasserman, Oleg Sokolsky and Insup Lee. In 15th IEEE International Symposium on High Assurance Systems Engineering (HASE 2014), Miami, Florida, USA, January 9 - 11, 2014.
Closed-loop Verification of Medical Devices with Model Abstraction and Refinement. Z. Jiang, M. Pajic, S. Moarref, R. Alur, and R. Mangharam. To appear in Journal of Software Tools for Technology Transfer, 2013.
Model-Driven Safety Analysis of Closed-Loop Medical Systems. Miroslav Pajic, Rahul Mangharam, Oleg Sokolsky, David Arney, Julian M. Goldman, and Insup Lee. In IEEE Transactions on Industrial Informatics, 10(1), 2014, pp 3-16. Published in IEEE Xplore Early Access October 2012.
Compositional Verification of a Medical Device System. Anitha Murugesan, Michael Whalen, Sanjai Rayadurgam and Mats Heimdahl. To appear in ACM SIGAda International Conference on High Integrity Language Technology, Pittsburg, PA, November 2013.
A Modal Specification Theory for Timing Variability. Andrew King, Oleg Sokolsky, and Insup Lee. In University of Pennsylvania Department of Computer and Information Science Technical Report, No. MS-CIS-13-11, November 2013.
Cyber-Physical System Requirements - A Model Driven Approach. Anitha Murugesan, Lian Duan, Sanjai Rayadurgam, and Mats Heimdahl. Poster presented at the Grace Hopper Celebration of Women in Computing, Minneapolis, Minnesota, October 2013.
Platform-Dependent Code Generation for Embedded Real-Time Software. BaekGyu Kim, Linh T.X. Phan, Oleg Sokolsky and Insup Lee. In International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2013), Montreal, Canada, September/October 2013.
Model-based development of the Generic PCA infusion pump user interface within PVS. Paolo Masci, Anaheed Ayoub, Paul Curzon, Insup Lee, Oleg Sokolsky, and Harold Thimbleby. In 32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2013), Toulouse, France, September 2013. LNCS Volume 8153, 2013, pp 228-240, doi 10.1007/978-3-642-40793-2_21.
A Causality Analysis Framework for Component-based Real-time Systems. Shaohui Wang, Anaheed Ayoub, BaekGyu Kim, Gregor G ossler, Oleg Sokolsky, and Insup Lee. In 13th International Conference on Runtime Verification (RV '13), INRIA Rennes, France, September 2013.
Evaluation and Enhancement of an Intraoperative Insulin Infusion Protocol via In-Silico Simulation. Benjamin Kohl, Sanjian Chen, Margaret Mullen-Fortino, and Insup Lee. In IEEE International Conference on Healthcare Informatics (ICHI 2013), Philadelphia, PA, September 2013.
RADA: A Tool for Reasoning about Algebraic Data Types with Abstractions. Tuan-Hung Pham and Michael W. Whalen. In Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the Symposium on Foundations of Software Engineering, St. Petersburg, Russia, August 2013.
A Modal Specification Approach for On-Demand Medical Systems. Andrew L. King, Lu Feng, Oleg Sokolsky, Insup Lee. In Third International Symposium on Foundations of Health Information Engineering and Systems (FHIES 2013), Macau, August 2013.
Assuring the Safety of On-Demand Medical Cyber-Physical Systems. Andrew L. King, Lu Feng, Oleg Sokolsky, Insup Lee. In 1st International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA 2013), Taipei, Taiwan, August 2013.
Modeling and Requirements on the Physical Side of Cyber-Physical Systems. Mats Heimdahl, Lian Duan, Anitha Murugesan and Sanjai Rayadurgam. In Second ICSE Workshop on the Twin Peaks of Requirements and Architecture, San Francisco, CA, USA, May 2013.
Modes, Features, and State-Based Modeling for Clarity and Flexibility. Anitha Murugesan, Sanjai Rayadurgam, and Mats Heimdahl. In ICSE Workshop on Modeling in Software Engineering, San Francisco, CA, USA, May 2013.
Observable Modified Condition / Decision Coverage. Michael W. Whalen, Gregory Gay, Dongjiang You, Matt Staats, and Mats P.E. Heimdahl. In 35th International Conference on Software Engineering, San Francisco, CA, USA, May 2013.
An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. Tuan-Hung Pham and Michael W. Whalen. In Verified Software: Theories, Tools, and Experiments (VSTTE 2013), Atheron, CA, USA, May 2013.
Using Models to Address Challenges in Specifying Requirements for Medical Cyber-Physical Systems. Anitha Murugesan, Sanjai Rayadurgam, and Mats Heimdahl. In Medical Cyber Physical Systems Workshop, Philadelphia, PA, USA, April 2013.
Heart-on-a-Chip: A Closed-loop Testing Platform for Implantable Pacemakers. Z. Jiang, S. Radhakrishnan, V. Sampath, S. Sarode and R. Mangharam. In Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'13) at CPSWeek, April 2013.
Your What is My How: Iteration and Hierarchy in System Design. Michael W. Whalen, Andrew Gacek, Darren Cofer, Anitha Murugesan, Sanjai Rayadurgam, and Mats Heimdahl. In IEEE Software, 30 (2), 54, March/April 2013.
Healthcare information technology’s relativity problems: a typology of how patients’ physical reality, clinicians’ mental models, and healthcare information technology differ. Sean W Smith, Ross Koppel. In J Am Med Inform Assoc (JAMIA), published online 2013.
Assessing the Overall Sufficiency of Safety Arguments. Anaheed Ayoub, Jian Chang, Oleg Sokolsky, and Insup Lee. In 21st Safety-critical Systems Symposium (SSS'13). Bristol, UK, February 2013.
Cyber-Physical Modeling of Implantable Cardiac Medical Devices. Z. Jiang, M. Pajic and R. Mangharam. In Proceeding of IEEE Special Issue on Cyber-Physical Systems, p. 122, vol. 100, (2012).
Security and Interoperable Medical Device Systems, Part 2: Failures, Consequences and Classifications. Eugene Y. Vasserman, Krishna K. Venkatasubramanian, Oleg Sokolsky, and Insup Lee. In IEEE Security & Privacy. 10(6), pp 70 - 73, November-December 2012.
Security and Interoperable Medical Device Systems: Part 1. Krishna K. Venkatasubramanian, Eugene Y. Vasserman, Oleg Sokolsky, and Insup Lee. In IEEE Security & Privacy. 10(5), pp 61 - 63, September-October 2012.
A Model-Based I/O Interface Synthesis Framework for the Cross-Platform Software Modeling. BaekGyu Kim, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. In IEEE International Symposium on Rapid System Prototyping (RSP 2012). Tampere, Finland, October 2012.
Evaluation of a Smart Alarm for Intensive Care using Clinical Data. Andrew King, Kelsea Fortino, Nicholas Stevens, Sachin Shah, Margaret Fortino-Mullen, and Insup Lee. In 34th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC'12). San Diego, California, September, 2012.
Your What is My How: Why Requirements and Architectural Design Should Be Iterative. Michael Whalen, Mats Heimdahl, and Anitha Murugesan. In First International Workshop on the Twin Peaks of Requirements and Architecture, International Requirements Engineering Conference, Chicago, Illinois, September 2012.
A Systematic Approach to Justifying Sufficient Confidence in Software Safety Arguments. Anaheed Ayoub, BaekGyu Kim, Insup Lee, and Oleg Sokolsky. In 31st International Conference on Computer Safety, Reliability and Security (SAFECOMP 2012), Magdeburg, Germany, September 2012.
Rationale and Architecture Principles for Medical Application Platforms. John Hatcliff, Andrew King, Insup Lee, Alasdair MacDonald, Anura Fernando, Michael Robkin, Eugene Vasserman, Sandy Weininger and Julian Goldman. In ACM/IEEE Third International Conference on Cyber-Physical Systems (ICCPS 2012). Beijing, China, April 2012 (Invited Paper).
From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study. Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, and Rahul Mangharam. In 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012). Beijing, China, April 2012. (Best Student Paper Award).
Optimal scheduling for constant-rate multi-mode systems. R. Alur, A. Trivedi, and D. Wojtczak. In 15th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), Beijing, China, April 2012.
A Safety Case Pattern for Model-Based Development Approach. Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky. In NASA Formal Methods Symposium (NFM). Norfolk, VA, April 2012.
Modeling and Verification of a Dual Chamber Implantable Pacemaker. Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur and Rahul Mangharam. In 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 7214, Tallinn, Estonia, March/April 2012.
Challenges and Research Directions in Medical Cyber-Physical Systems. Insup Lee, Oleg Sokolsky, Sanjian Chen, John Hatcliff, Eunkyoung Jee, BaekGyu Kim, Andrew King, Margaret Mullen-Fortino, Soojin Park, Alexander Roederer, and Krishna Venkatasubramanian. In Special Issue on Cyber-Physical Systems, Proceedings of the IEEE, Volume 100, Issue 1, pp.75-90, January 2012 (Invited Paper).
The Medical Device Dongle: An Open-Source Standards-Based Platform for Interoperable Medical Device Connectivity. Philip Asare, Danyang Cong, Santosh Vattam, Baek-Gyu Kim, Shan Lin, Oleg Sokolsky, Margaret Mullen-Fortino and Insup Lee. In Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, FL, January 2012.
Smart Alarms: Multivariate Medical Alarm Integration for post CABG surgery patients. Stevens Nicholas, Giannareas Ana, Kern Vanessa, Viesca Adrian, Fortino-Mullen Margaret, King Andrew, Lee Insup. In Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, FL, January 2012.
Clinical Decision Support for Integrated Cyber-Physical Systems: A Mixed Methods Approach. Alex Roederer, Andrew Hicks, Enny Oyeniran, Insup Lee and Soojin Park. In Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, FL, January 2012.
Limitations of Threshold-Based Brain Oxygen Monitoring for Seizure Detection. Soojin Park, Alexander Roederer, Ram Mani, Sarah Schmitt, Peter D. LeRoux, Lyle H. Ungar, Insup Lee, Scott E. Kasner. In Neurocritical Care. December 2011, Volume 15, Issue 3, pp 469-476
Challenges in the Regulatory Approval of Medical Cyber-Physical Systems. Oleg Sokolsky, Insup Lee, and Mats Heimdahl. In Proceedings of the International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011.
Safety-Assured Development of the GPCA Infusion Pump Software. BaekGyu Kim, Anaheed Ayoub, Oleg Sokolsky, Insup Lee, Paul Jones, Yi Zhang, and Raoul Jetley. In Proceedings of the International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011.
Relating Average and Discounted Rewards for Quantitative Analysis of Timed Systems. R. Alur and A. Trivedi. In Proceedings of the International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011.
Formal verification of hybrid systems. Rajeev Alur. In Proceedings of the International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011.
Runtime Verification of Traces under Recording Uncertainty. Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky, and Insup Lee. In Proceedings of the 2nd International Conference on Runtime Verification (RV 2011), San Francisco, CA, 2011.
Biomedical Devices and Systems Security. David Arney, Krishna K. Venkatasbramanian, Oleg Sokolsky, and Insup Lee. In Proceedings of 33rd Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC ’11). Boston, MA, August/September 2011.
Modeling Cardiac Pacemaker Malfunctions with the Virtual Heart Model. Z. Jiang and R. Mangharam. In 33rd International Conference IEEE Engineering in Medicine and Biology Society (EMBC ’11). Boston, MA, August/September 2011.
Polyglot: Modeling and Analysis for Multiple Statechart Formalisms. D. Balasubramanian, C. S. Pasareanu, M. W. Whalen, G. Karsai, and M. Lowry. In Proceedings of International Symposium on Software Testing and Analysis (ISSTA), Toronto, Ontario, Canada, July 2011.
On Effective Testing of Health Care Simulation Software. Christian Murphy, M.S. Raunak, Andrew King, Sanjian Chen, Christopher Imbriano, Gail Kaiser, Insup Lee, Oleg Sokolsky, Lori Clarke, Leon Osterweil. In Proceedings of the 3rd International Workshop on Software Engineering in Health Care (SEHC 2011). Honolulu, Hawaii, May 2011.
Model-based Closed-loop Testing of Implantable Pacemakers. Z. Jiang, M. Pajic, R. Mangharam. In 2nd International Conference on Cyber-Physical Systems, (IEEE ICCPS'11), April 2011.
GSA: A Framework for Rapid Prototyping of Smart Alarm Systems. Andrew King, Alex Roederer, David Arney, Sanjian Chen, Margaret Fortino-Mullen, Ana Giannareas, C. William Hanson III, Vanessa Kern, Nicholas Stevens, Jonathan Tannen, Adrian Viesca Trevino, Soojin Park, Oleg Sokolsky, and Insup Lee. In Proceedings of the 1st ACM International Health Informatics Symposium (IHI '10), Arlington, Virginia, USA, November 2010.
Assurance Cases in Model-Driven Development of the Pacemaker Software. Eunkyoung Jee, Insup Lee and Oleg Sokolsky In Proceedings of the 4th International Symposium On Leveraging Application of Formal Methods, Verification and Validation (ISoLA 2010), Part II, LNCS 6416, pp. 343-356, Amirandes, Heraclion, Crete, October 2010.