Sökning: onr:"swepub:oai:gup.ub.gu.se/260949" >
Runtime Enforcement...
Runtime Enforcement of Cyber-Physical Systems
-
- Pinisetty, Srinivas (författare)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap (GU),Department of Computer Science and Engineering, Computing Science (GU)
-
Roop, P. S. (författare)
-
Smyth, S. (författare)
-
visa fler...
-
Allen, N. (författare)
-
Tripakis, S. (författare)
-
Von Hanxleden, R. (författare)
-
visa färre...
-
(creator_code:org_t)
- 2017-09-27
- 2017
- Engelska.
-
Ingår i: Acm Transactions on Embedded Computing Systems. - : Association for Computing Machinery (ACM). - 1539-9087 .- 1558-3465. ; 16
- Relaterad länk:
-
https://gup.ub.gu.se...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- 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
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas