Projects per year
Abstract
Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a “safety shield” that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model checking and reactive synthesis fail, because it only considers a small set of critical properties, as opposed to the complex design, or the complete specification in the case of reactive synthesis. The shield continuously monitors the input/output of the design and corrects its erroneous output only if necessary, and as little as possible, so other non-critical properties are likely to be retained. Although runtime enforcement has been studied in other domains such as action systems, reactive systems pose unique challenges where the shield must act without delay. We thus present the first shield synthesis solution for reactive hardware systems and report our experimental results.
Original language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems (TACAS) - 21st International Conference |
Place of Publication | Berlin Heidelberg |
Publisher | Springer |
Pages | 533-548 |
ISBN (Print) | 978-3-662-46680-3 |
DOIs | |
Publication status | Published - 2015 |
Event | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015 - London, United Kingdom Duration: 13 Apr 2015 → 17 Apr 2015 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 9035 |
Conference
Conference | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
---|---|
Abbreviated title | TACAS 2015 |
Country/Territory | United Kingdom |
City | London |
Period | 13/04/15 → 17/04/15 |
Fields of Expertise
- Information, Communication & Computing
Treatment code (Nähere Zuordnung)
- Application
- Theoretical
Fingerprint
Dive into the research topics of 'Shield Synthesis: - Runtime Enforcement for Reactive Systems'. Together they form a unique fingerprint.Projects
- 3 Finished
-
EU - STANCE - A Source code analysis Toolbox for software security AssuraNCE
Tögl, R., Könighofer, R. & Bloem, R.
1/10/12 → 30/09/15
Project: Research project
-
FWF - RiSE - Rigorous Systems Engineering
Könighofer, R., Khalimov, A., Bloem, R., Könighofer, B. & Jacobs, S.
1/03/11 → 31/08/19
Project: Research project
-
Formal Methods for Design & Verification
Jacobs, S., Bloem, R., Könighofer, R., Könighofer, B., Khalimov, A., Hofferek, G. & Braud-Santoni, N.
1/02/08 → 15/07/19
Project: Research area