research-article

Open access

Runtime enforcement of timed properties using games

Authors:

Matthieu Renard,

Antoine Rollet,

Yliès FalconeAuthors Info & Claims

Formal Aspects of Computing, Volume 32, Issue 2-3

Pages 315 - 360

https://doi.org/10.1007/s00165-020-00515-2

Published: 01 July 2020 Publication History

Abstract

This paper deals with runtime enforcement of timed properties with uncontrollable events. Runtime enforcement consists in defining and using an enforcement mechanism that modifies the executions of a running system to ensure their correctness with respect to the desired property. Uncontrollable events cannot be modified by the enforcement mechanisms and thus have to be released immediately. We present a complete theoretical framework for synthesising such mechanism, modelling the runtime enforcement problem as a Büchi game. It permits to pre-compute the decisions of the enforcement mechanism, thus avoiding to explore the whole execution tree at runtime. The obtained enforcement mechanism is sound, compliant and optimal, meaning that it should output as soon as possible correct executions that are as close as possible to the input execution. This framework takes as input any timed regular property modelled by a timed automaton. We present GREP, a tool implementing this approach. We provide algorithms and implementation details of the different modules of GREP, and evaluate its performance. The results are compared with another state of the art runtime enforcement tool.

References

References

[1]

Alcalde B, Cavalli A, Chen D, Khuu D, Lee D (2004) Network protocol system passive testing for fault management: A backward checking approach. In: International conference on formal techniques for networked and distributed systems. Springer, pp 150–166

[2]

Alur R, Courcoubetis C, Halbwachs N, Dill D, Wong-Toi H (1992) Minimization of timed transition systems. In: CONCUR'92. Springer, pp 340–354

[3]

Alur R, Dill D(1992) The theory of timed automata. In: de Bakker JW, Huizing C, de Roever WP, Rozenberg G(eds)Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 45–73

[4]

Bartocci E, Falcone Y, (eds) (2018) Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science. Springer, Heidelberg

[5]

Bartocci E, Falcone Y, Francalanza A, Reger G (2018) Introduction to runtime verification. In: Bartocci and Falcone [BF18], pp 1–33

[6]

Basin D, Jugé V, Klaedtke F, Zălinescu E (2013) Enforceable security policies revisited. ACM Trans Inf Syst Secur 16(1):3:1–3:26

[7]

Bloem R, Könighofer B, Könighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: CoRR, arXiv:1501.02573

[8]

Basin D, Klaedtke F, Zalinescu E (2011) Algorithms for monitoring real-time properties. In: Khurshid S, Sen K (eds) Proceedings of the 2nd international conference on runtime verification (RV 2011), volume 7186 of lecture notes in computer science. Springer, pp 260–275

[9]

Bengtsson J and Yi W Timed automata: Semantics, aalgorithms and tools Lect Notes Comput Sci 2004 3098 87-124

[10]

Charafeddine H, El-Harake K, Falcone Y, Jaber M (2015) Runtime enforcement for component-based systems. In: Proceedings of the 30th annual ACM symposium on applied computing, 2015, pp 1789–1796

[11]

Cavalli A, Gervy C, and Prokopenko S New approaches for passive testing using an extended finite state machine specification Inf Softw Technol 2003 45 12 837-852

[12]

Chatterjee K, Henzinger TA, Piterman N (2008) Algorithms for büchi games. arXiv:0805.2620

[13]

Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: Automata, languages and programming, pp 474–486

[14]

Dolzhenko E, Ligatti J, and Reddy S Modeling runtime enforcement with mandatory results automata Int J Inf Secur 2015 14 1 47-60

Digital Library

[15]

Falcone Y (2010) You should better enforce than verify. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds), proceedings Runtime verification - first international conference, RV 2010, St. Julians, Malta, November 1-4, 2010, volume 6418 of lecture notes in computer science. Springer, pp 89–105

[16]

Falcone Y, Fernandez J-C, and Mounier L What can you verify and enforce at runtime? Int J Softw Tools Technol Transfer 2012 14 3 349-382

[17]

Falcone Y, Havelund K, Reger G (2013) A tutorial on runtime verification. In: Broy M, Peled DA, Kalus G (eds) Engineering dependable software systems, volume 34 of NATO science for peace and security series, D: information and communication security. IOS Press, pp 141–175

[18]

Falcone Y, Jéron T, Marchand H, and Pinisetty S Runtime enforcement of regular timed properties by suppressing and delaying events Syst Control Lett 2016 123 2-41

Digital Library

[19]

Falcone Y, Mounier L, Fernandez J-C, and Richier J-L Runtime enforcement monitors: composition, synthesis, and enforcement abilities Formal Methods Syst Des 2011 38 3 223-262

Digital Library

[20]

Falcone Y, Mariani L, Rollet A, Saha S (2018) Runtime failure prevention and reaction. In: Bartocci and Falcone [BF18], pp 103–134

[21]

Falcone Y, Pinisetty S (2019) On the runtime enforcement of timed properties. In: Bernd F, Leonardo M (eds), Proceedings runtime verification—19th international conference, RV 2019, Porto, Portugal, October 8-11, 2019, volume 11757 of Lecture Notes in Computer Science. Springer, pp. 48–69

[22]

Gradel E and Thomas W Automata, logics, and infinite games: a guide to current research 2002 Berlin Springer

[23]

Khoury R and Tawbi N Which security policies are enforceable by runtime monitors? A survey. Comput Sci Rev 2012 6 1 27-45

[24]

Ligatti J, Bauer L, Walker D (2009) Run-time enforcement of nonsafety policies. ACM Trans Inf Syst Secur 12(3):19:1–19:41

[25]

Leucker M and Schallhart C A brief account of runtime verification J Log Algebr Program 2009 78 5 293-303

[26]

Manna Z, Pnueli A (1990) A hierarchy of temporal properties (invited paper, 1989). In: Proceedings of the ninth annual ACM symposium on Principles of distributed computing. ACM, pp 377–410

[27]

Pinisetty S, Falcone Y, Jéron T, Marchand H, Rollet A, Nguena Timo O (2013) Runtime enforcement of timed properties. In: Shaz Q, Serdar T (eds) Runtime verification, volume 7687 of lecture notes in computer science. Springer, pp. 229–244

[28]

Pinisetty S, Falcone Y, Jéron T, Marchand H, Rollet A, and Nguena-Timo OL Runtime enforcement of timed properties revisited Formal Methods Syst Des 2014 45 3 381-422

Digital Library

[29]

Pinisetty S, Falcone Y, Jéron T, Marchand H (2014) Runtime enforcement of parametric timed properties with practical applications. In: 12th international workshop on discrete event systems, WODES 2014, Cachan, France, May 14-16, 2014, pp 420–427

[30]

Pinisetty S, Falcone Y, Jéron T, Marchand H (2014) Runtime enforcement of regular timed properties. In: Cho Y, Shin SY, Kim SW, Hung CC, Hong J (eds) Symposium on applied computing, SAC 2014, Gyeongju, Republic of Korea—March 24-28, 2014. ACM, pp 1279–1286

[31]

Pinisetty S, Falcone Y, Jéron T, Marchand H (2015) TiPEX: a tool chain for timed property enforcement during execution. In: Bartocci E, Majumdar R, (eds) RV’2015, 6th international conference on runtime verification, volume 9333 of lecture notes in computer science, Vienne, Austria, Springer, pp 12

[32]

Renard M, Falcone Y, Rollet A, Jéron T, and Marchand H Optimal enforcement of (timed) properties with uncontrollable events Math Struct Comput Sci 2017 29 1 169-214

[33]

Renard M, Rollet A, Falcone Y (2017) Grep: games for the runtime enforcement of properties. In: Nina Y, Ana Rosa C, Hüsnü Y (eds) Testing Software and Systems—ICTSS 2017. Springer, Berlin, pp 259–275

[34]

Renard M, Rollet A, Falcone Y (2017) Runtime enforcement using Büchi games. In: Proceedings of model checking software—24th international symposium, SPIN 2017, Co-located with ISSTA 2017, Santa Barbara, USA. ACM Press, pp 70–79

[35]

Schneider FB Enforceable security policies ACM Trans Inf Syst Secur 2000 3 1 30-50

Digital Library

[36]

UDBM (2011) Uppaal DBM Library. http://people.cs.aau.dk/~adavid/UDBM/. Accessed: 2017-04-27

[37]

Wu M, Zeng H, Wang C (2016) Synthesizing runtime enforcer of safety properties under burst error. In: 8th NASA Formal methods symposium NFM16, Minneapolis, USA

Cited By

Shankar SPradhan APinisetty SRollet AFalcone Y(2024)Bounded-memory runtime enforcement with probabilistic and performance analysisFormal Methods in System Design10.1007/s10703-024-00446-162:1-3(141-180)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10703-024-00446-1
Shankar SPinisetty S(2023)Serial Compositional Runtime Enforcement of Safety Timed PropertiesProceedings of the 16th Innovations in Software Engineering Conference10.1145/3578527.3578529(1-11)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3578527.3578529
Bonfanti SRiccobene EScandurra P(2023)A component framework for the runtime enforcement of safety propertiesJournal of Systems and Software10.1016/j.jss.2022.111605198:COnline publication date: 1-Apr-2023
https://dl.acm.org/doi/10.1016/j.jss.2022.111605
Show More Cited By

Recommendations

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 ...
Runtime enforcement using Büchi games
SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We ...
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 ...

Comments

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 32, Issue 2-3

Jul 2020

203 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2020.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 2020

Accepted: 05 June 2020

Revision received: 09 April 2020

Received: 28 March 2018

Published in FAC Volume 32, Issue 2-3

Author Tags

Qualifiers

Research-article

Funding Sources

Bordeaux INP
Région Nouvelle Aquitaine (France)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
65
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)7

Reflects downloads up to 22 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shankar SPradhan APinisetty SRollet AFalcone Y(2024)Bounded-memory runtime enforcement with probabilistic and performance analysisFormal Methods in System Design10.1007/s10703-024-00446-162:1-3(141-180)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10703-024-00446-1
Shankar SPinisetty S(2023)Serial Compositional Runtime Enforcement of Safety Timed PropertiesProceedings of the 16th Innovations in Software Engineering Conference10.1145/3578527.3578529(1-11)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3578527.3578529
Bonfanti SRiccobene EScandurra P(2023)A component framework for the runtime enforcement of safety propertiesJournal of Systems and Software10.1016/j.jss.2022.111605198:COnline publication date: 1-Apr-2023
https://dl.acm.org/doi/10.1016/j.jss.2022.111605
Shankar SRollet APinisetty SFalcone Y(2022)Bounded-Memory Runtime EnforcementModel Checking Software10.1007/978-3-031-15077-7_7(114-133)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1007/978-3-031-15077-7_7

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents