Srinivas Pinisetty
Reinhard Von Hanxleden
Abstract
Many implantable medical devices, such as pacemakers, have been recalled due to failure of their embedded software. This motivates rethinking their design and certification processes. We propose, for the first time, an additional layer of safety by formalising the problem of run-time enforcement of implantable pacemakers. While recent work has formalised run-time enforcement of reactive systems, the proposed framework generalises existing work along the following directions: (1) we develop bi-directional enforcement, where the enforced policies depend not only on the status of the pacemaker (the controller) but also of the heart (the plant), thus formalising the run-time enforcement problem for cyber-physical systems (2) we express policies using a variant of discrete timed automata (DTA), which can cover all regular properties unlike earlier frameworks limited to safety properties, (3) we are able to ensure the timing safety of implantable devices through the proposed enforcement, and (4) we show that the DTA-based approach is efficient relative to its dense time variant while ensuring that the discretisation error is relatively small and bounded. The developed approach is validated through a prototype system implemented using the open source KIELER framework. The experiments show that the framework incurs minimal runtime overhead.
- Weiwei Ai, Nitish Patel, and Partha Roop. 2016. Requirements-centric closed-loop validation of implantable cardiac devices. In Design, Automation 8 Test in Europe Conference 8 Exhibition (DATE), 2016. IEEE, 846--849 Google Scholar
Digital Library
- Homa Alemzadeh, Ravishankar K. Iyer, Zbigniew Kalbarczyk, and Jai Raman. 2013. Analysis of safety-critical computer failures in medical devices. Security 8 Privacy, IEEE 11, 4 (2013), 14--26. Google ScholarDigital Library
- Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126, 2 (1994), 183--235. Google ScholarDigital Library
- Charles Andre, Frédéric Boulanger, and Alain Girault. 2001. Software implementation of synchronous programs. In Application of Concurrency to System Design, 2001. Proceedings. 2001 International Conference on. IEEE, 133--142. Google ScholarDigital Library
- A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. 2003. The synchronous languages 12 years later. Proc. IEEE 91, 1 (Jan 2003), 64--83.Google ScholarCross Ref
- Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. 2015. Shield synthesis: Runtime enforcement for reactive systems. In TACAS (LNCS), Vol. 9035. Springer. Google ScholarDigital Library
- Marius Bozga, Oded Maler, and Stavros Tripakis. 1999. Efficient verification of timed automata using dense and discrete time semantics. In Correct Hardware Design and Verification Methods: 10th IFIP WG10.5 Advanced Research Working Conference, CHARME’99 BadHerrenalb, Germany, September 27--29, 1999 Proceedings, Laurence Pierre and Thomas Kropf (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 125--141. Google ScholarDigital Library
- Lei Bu, Qixin Wang, Xin Chen, Linzhang Wang, Tian Zhang, Jianhua Zhao, and Xuandong Li. 2011. Toward online hybrid systems model checking of cyber-physical systems’ time-bounded short-run behavior. SIGBED Rev. 8, 2 (June 2011), 7--10. Google ScholarDigital Library
- Taolue Chen, Marco Diciolla, Marta Kwiatkowska, and Alexandru Mereacre. 2013. A simulink hybrid heart model for quantitative verification of cardiac pacemakers. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. ACM, 131--136. Google ScholarDigital Library
- Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. 2015. Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Sec. 14, 1 (2015), 47--60. Google ScholarDigital Library
- Ylies Falcone, Thierry Jéron, Hervé Marchand, and Srinivas Pinisetty. 2016. Runtime enforcement of regular timed properties by suppressing and delaying events. Science of Computer Programming 123 (2016), 2--41. Google ScholarDigital Library
- Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. 2011. Runtime enforcement monitors: Composition, synthesis, and enforcement abilities. FMSD 38, 3 (2011), 223--262. Google ScholarDigital Library
- Nicolas Halbwachs, Fabienne Lagnier, and Pascal Raymond. 1994. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST’93). Springer, 83--96. Google ScholarDigital Library
- Zhihao Jiang, Miroslav Pajic, Rajeev Alur, and Rahul Mangharam. 2014. Closed-loop verification of medical devices with model abstraction and refinement. International Journal on Software Tools for Technology Transfer 16, 2 (2014), 191--213. Google ScholarDigital Library
- Z. Jiang, M. Pajic, and R. Mangharam. 2012. Cyber-physical modeling of implantable cardiac medical devices. Proc. IEEE 100, 1 (Jan 2012), 122--137.Google Scholar
- Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, and Rahul Mangharam. 2012. Modeling and verification of a dual chamber implantable pacemaker. In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12). Springer-Verlag, Berlin, Heidelberg, 188--203. Google ScholarDigital Library
- Marta Kwiatkowska, Harriet Lea-Banks, Alexandru Mereacre, and Nicola Paoletti. 2014. Formal modelling and validation of rate-adaptive pacemakers. In Healthcare Informatics (ICHI), 2014 IEEE International Conference on. IEEE, 23--32. Google ScholarDigital Library
- Jay Ligatti, Lujo Bauer, and David Walker. 2009. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12, 3, Article 19 (Jan. 2009), 19:1--19:41 pages. Google ScholarDigital Library
- Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand, Antoine Rollet, and Omer Nguena Timo. 2014. Runtime enforcement of timed properties revisited. FMSD 45, 3 (2014), 381--422. Google ScholarDigital Library
- Fred B. Schneider. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 1 (2000), 30--50. Google ScholarDigital Library
- Partha S. Roop Sidharta Andalam, Avinash Malik, and Mark Trew. 2016. Hybrid automata model of the heart for formal verification of pacemakers. In Applied Verification for Continuous and Hybrid Systems (ARCH’16). Vienna, Austria.Google Scholar
- Christian von Essen and Barbara Jobstmann. 2013. Program Repair without Regret. Springer, Berlin, Heidelberg, 896--911.Google Scholar
- F. Xu, Z. Qin, C. C. Tan, B. Wang, and Q. Li. 2011. IMDGuard: Securing implantable medical devices with the external wearable guardian. In 2011 Proceedings IEEE INFOCOM. 1862--1870.Google Scholar
- P. Ye, E. Entcheva, S. A. Smolka, and R. Grosu. 2008. Modelling excitable cells using cycle-linear hybrid automata. IET Systems Biology 2, 1 (2008), 24--32.Google ScholarCross Ref
- Eugene Yip, Sidharta Andalam, Partha S. Roop, Avinash Malik, Mark Trew, Weiwei Ai, and Nitish Patel. 2016. Towards the emulation of the cardiac conduction system for pacemaker testing. arXiv Preprint arXiv:1603.05315 (2016).Google Scholar
Index Terms
- Runtime Enforcement of Cyber-Physical Systems
Recommendations
Runtime enforcement of reactive systems using synchronous enforcers
SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of SoftwareSynchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem ...
Predictive runtime enforcement
Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ...
Runtime enforcement of timed properties revisited
Runtime enforcement is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence ...
Comments