http://mlab.seas.upenn.edu Real-Time & Embedded Systems Laboratory - University of Pennsylvania Sun, 08 Jan 2017 18:05:58 +0000 en-US hourly 1 https://wordpress.org/?v=4.6.9 http://mlab.seas.upenn.edu/heart-on-a-chip-won-1st-prize-award-of-excellence-of-high-tech-medical-service-in-the-world-embedded-software-contestwesc/ Fri, 07 Dec 2012 20:37:09 +0000 http://mlab.seas.upenn.edu/?p=2962 http://mlab.seas.upenn.edu/the-vhm-team-and-the-protodrive-team-are-going-to-participate-in-wesc2012-in-seoul-korea/ Fri, 09 Nov 2012 20:15:21 +0000 http://mlab.seas.upenn.edu/?p=2810 http://mlab.seas.upenn.edu/mlab-wins-the-1st-prize-in-the-seas-senior-design-competition-congrats-to-the-pvs-team/ Tue, 21 Aug 2012 02:59:02 +0000 http://mlab.seas.upenn.edu/?p=1839 http://mlab.seas.upenn.edu/tacas-paper-nominated-for-best-paper-award/ Fri, 11 May 2012 00:08:10 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=996 http://mlab.seas.upenn.edu/rtas-model-translation-paper-won-ieee-best-student-paper-award/ Tue, 24 Apr 2012 20:40:16 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=987 http://mlab.seas.upenn.edu/vhm-simulink-model-v1-0-released/ Tue, 14 Feb 2012 18:53:48 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=891 VHM Simulink

]]> http://mlab.seas.upenn.edu/pacemaker-verification-uppaal-model-release/ Tue, 14 Feb 2012 01:42:13 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=880 Pacemaker Verification UPPAAL

]]> http://mlab.seas.upenn.edu/modeling-and-verification-of-a-dual-chamber-implantable-pacemaker-18th-international-conference-on-tools-and-algorithms-for-the-construction-and-analysis-of-systems-tacas-2012/ Mon, 13 Feb 2012 22:11:11 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=810 Continue Reading]]> The design and implementation of software for medical devices is challenging due to their rapidly increasing functionality and the tight coupling of computation, control, and communication. The safety-critical nature and the lack of existing industry standards for verification, make this an ideal domain for exploring applications of formal modeling and analysis. In this study, we use a dual chamber implantable pacemaker as a case study for modeling and verification of control algorithms for medical devices in UPPAAL. We begin with detailed models of the pacemaker, based on the specifications and algorithm descriptions from Boston Scientific. We then define the state space of the closed-loop system based on its heart rate and developed a heart model which can non-deterministically cover the whole state space. For verification, we first specify unsafe regions within the state space and verify the closed-loop system against corresponding safety requirements. As stronger assertions are attempted, the closed-loop unsafe state may result from healthy open-loop heart conditions. Such unsafe transitions are investigated with two clinical cases of Pacemaker Mediated Tachycardia and their corresponding correction algorithms in the pacemaker. Along with emerging tools for code generation from UPPAAL models, this effort enables model-driven design and certification of software for medical devices.

]]> http://mlab.seas.upenn.edu/vhm-in-distinguished-lecture-series-uiuc-march-2011/ Mon, 13 Feb 2012 17:54:14 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=805 http://mlab.seas.upenn.edu/model-based-closed-loop-testing-paper-published-in-ieee-iccps11-april-2011/ Mon, 13 Feb 2012 21:53:33 +0000 http://alliance.seas.upenn.edu/~mlabweb/dynamic/?p=799 Continue Reading]]> The increasing complexity of software in implantable medical devices such as cardiac pacemakers and defibrillators accounts for over 40% of device recalls. Testing remains the principal means of verification in the medical device certification regime. Traditional software test generation techniques, where the tests are generated independently of the operational environment, are not effective as the device must be tested within the context of the patient's condition and the current state of the heart. It is necessary for the testing system to observe the system state and conditionally generate the next input to advance the purpose of the test. To this effect, a set of general and patient condition-specific temporal requirements is specified for the closed-loop heart and pacemaker system. Based on these requirements, we describe a closed-loop testing environment between a timed automata-based heart model and a pacemaker. This allows for interactive and physiologically relevant model-based test generation for basic pacemaker device operations such as maintaining the heart rate and atrial-ventricle synchrony. We also demonstrate the flexibility and efficacy of the testing environment for more complex common timing anomalies such as reentry circuits, pacemaker mode switch operation and pacemaker-mediated tachycardia. This system is a step toward a testing approach for medical cyber-physical systems with the patient-in-the-loop.

]]>