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.

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.

Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. Anitha Murugesan, Oleg Sokolsky, Sanjai Rayadurgam, Michael Whalen, Mats Heimdahl, and Insup Lee. In Proceedings of 5th International Conference on Cyber-Physical Systems (ICCPS 2014), Berlin, Germany, April 2014.

A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal. Lu Feng, Andrew L. King, Sanjian Chen, Anaheed Ayoub, Junkil Park, Nicola Bezzo, Oleg Sokolsky, and Insup Lee. In Medical Cyber Physical Systems Workshop 2014, Berlin, Germany, April 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.

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.

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.

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.

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.

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.

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.

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.

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.