Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Runtime Enforcement of Cy… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Runtime Enforcement of Cyber-Physical Systems

Artikel i vetenskaplig tidskrift
Författare Srinivas Pinisetty
P. S. Roop
S. Smyth
N. Allen
S. Tripakis
R. Von Hanxleden
Publicerad i Acm Transactions on Embedded Computing Systems
Volym 16
ISSN 1539-9087
Publiceringsår 2017
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap (GU)
Språk en
Länkar dx.doi.org/10.1145/3126500
Ämnesord 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
Ämneskategorier Datavetenskap (datalogi)

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?