To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Runtime Enforcement of Cy… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Runtime Enforcement of Cyber-Physical Systems

Journal article
Authors Srinivas Pinisetty
P. S. Roop
S. Smyth
N. Allen
S. Tripakis
R. Von Hanxleden
Published in Acm Transactions on Embedded Computing Systems
Volume 16
ISSN 1539-9087
Publication year 2017
Published at Department of Computer Science and Engineering, Computing Science (GU)
Language en
Keywords Runtime Monitoring, Runtime Enforcement, Automata, Timed Properties, Cyber-Physical Systems, medical devices, timed properties, automata, Computer Science, CAS 201218th International Conference on Tools and Algorithms for the Construction and Analysis of
Subject categories Computer Science


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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?