Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 4/2023

03-08-2023 | Original Article

On first-order runtime enforcement of branching-time properties

Authors: Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir

Published in: Acta Informatica | Issue 4/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime for a specified operational model of enforcing monitors. We study the enforceability of branching-time, first-order properties expressed in the Hennessy–Milner Logic with Recursion (\(\mu \) HML) with respect to monitors that can enforce behaviour involving events that carry data. To this end, we develop an operational framework for first-order enforcement via suppressions, insertions and replacements. We then use this model to formalise the meaning of enforcing a branching-time property. We also show that a safety syntactic fragment of the logic is enforceable within this framework by providing an automated synthesis function that generates correct suppression monitors from any formula taken from this logical fragment.
previous article Testing membership for timed automata
next article The second step in characterizing a three-word code

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
Literature
1.
2.
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3(1), 30–50 (2000)CrossRef
3.
Francalanza, A., Aceto, L., Achilleos, A., Attard, D.P., Cassar, I., Della Monica, D., Ingólfsdóttir, A.: A foundation for runtime monitoring. In: Lahiri, S., Reger, G. (eds.) Runtime Verification, pp. 8–29. Springer, Cham (2017)CrossRef
4.
Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1), 2–16 (2005)CrossRef
5.
Ligatti, J., Reddy, S.: A theory of runtime enforcement, with results. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) CESORICS, pp. 87–100. Springer, Berlin (2010)
6.
Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223–262 (2011)MATHCrossRef
7.
Berstel, J., Boasson, L.: Transductions and context-free languages. Ed. Teubner, pp. 1–278 (1979)
8.
9.
Alur, R., Černý, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 599–610. ACM, ISBN 978-1-4503-0490-0 (2011)
10.
Könighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., Könighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332–361 (2017)MATHCrossRef
11.
Francalanza, A., Aceto, L., Ingólfsdóttir, A.: Monitorability for the Hennessy–Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87–116 (2017)MATHCrossRef
12.
Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: Monitoring for silent actions. In: Lokam, S., Ramanujam, R. (eds.) FSTTCS 2017: Foundations of Software Technology and Theoretical Computer Science, volume 93 of LIPIcs, p. 7:1-7:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl (2018)
13.
Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: A framework for parameterized monitorability. In: Baier, C., Dal Lago, U. (eds.) Foundations of Software Science and Computation Structures, pp. 203–220. Springer, Cham (2018)CrossRef
14.
Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: On bidirectional runtime enforcement. In: Peters, K., Willemse, T.A.C. (eds.) FORTE, volume 12719 of Lecture Notes in Computer Science, pp. 3–21. Springer, Cham (2021)
15.
Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: Comparing controlled system synthesis and suppression enforcement. Int. J. Softw. Tools Technol. Transf. 23(4), 601–614 (2021)MATHCrossRef
16.
Burlò, C.B., Francalanza, A., Scalas, A.: On the monitorability of session types, in theory and practice. In: Møller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11–17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, p. 20:1-20:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl (2021)
17.
Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theoret. Comput. Sci. 336(2–3), 209–234 (2005)MathSciNetMATHCrossRef
18.
Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) Runtime Verification (RV), LNCS, pp. 172–189. Springer, Cham (2017)CrossRef
19.
Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33–58 (2017)MathSciNetMATHCrossRef
20.
Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York, pp. 582–594 (2016)
21.
Ferrando, A., Dennis, L.A., Ancona, D., Fisher, M., Mascardi, V.: Verifying and validating autonomous systems: towards an integrated approach. In: Colombo, C., Leucker, M. (eds.) Runtime Verification—18th International Conference, RV 2018, volume 11237 of Lecture Notes in Computer Science, pp. 263–281. Springer, Cham (2018). https://​doi.​org/​10.​1007/​978-3-030-03769-7_​15CrossRef
22.
Kejstová, K., Ročkai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) Runtime Verification RV 2017. Springer, Cham (2017)
23.
24.
Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. In: Bauer, F.L., et al. (eds.) Logic and Algebra of Specification, pp. 143–202. Springer, Berlin (1993)CrossRef
25.
Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) International Symposium on Formal Methods, pp. 573–586. Springer, Berlin (2006)
26.
27.
Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: The best a monitor can do. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25–28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, p. 7:1-7:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstu (2021). https://​doi.​org/​10.​4230/​LIPIcs.​CSL.​2021.​7CrossRef
28.
Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 14(3), 349 (2012)CrossRef
29.
30.
Larsen, K.G.: Proof systems for satisfiability in Hennessy–Milner logic with recursion. Theor. Comput. Sci. 72(2), 265–288 (1990)MathSciNetMATHCrossRef
31.
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) 25 Years of Model Checking, pp. 196–215. Springer, Berlin (2008)CrossRef
32.
33.
Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Tasiran, S. (eds.) International Workshop on Runtime Verification, pp. 126–138. Springer, Berlin (2007)CrossRef
34.
Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2–3), 209–234 (2005)MathSciNetMATHCrossRef
35.
Leucker, M.: Sliding between model checking and runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV, volume 7687 of Lecture Notes in Computer Science, pp. 82–87. Springer, Berlin (2012)
36.
Decker, N., Leucker, M., Thoma, D.: junit\({}^{\text{ rv }}\)-adding runtime verification to junit. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, volume 7871 of Lecture Notes in Computer Science, pp. 459–464. Springer, Berlin (2013)
37.
Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV, volume 10548 of Lecture Notes in Computer Science, pp. 172–189. Springer, Cham (2017)
38.
Kejstová, K., Rockai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) RV, volume 10548 of Lecture Notes in Computer Science, pp. 225–240. Springer, Cham (2017)
39.
Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Testing equivalence vs. runtime monitoring. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming, volume 11665 of Lecture Notes in Computer Science, pp. 28–44. Springer, Berlin (2019)CrossRef
40.
Monica, D.D, Francalanza, A.L.: Pushing runtime verification to the limit: may process semantics be with us. In: OVERLAY@AI*IA, volume 2509 of CEUR Workshop Proceedings, pp. 47–52. CEUR-WS.org (2019)
41.
Havelund, K., Peled, D.: Bdds for representing data in runtime verification. In: Deshmukh, J., Nickovic, D. (eds.) RV, volume 12399 of Lecture Notes in Computer Science, pp. 107–128. Springer, Cham (2020)
42.
Guzmán, M., Riganelli, O., Micucci, D., Mariani, L.: Test4enforcers: test case generation for software enforcers. In: Deshmukh, J., Nickovic, D. (eds.) RV, volume 12399 of Lecture Notes in Computer Science, pp. 279–297. Springer, Cham (2020)
43.
Burlò, C.B., Francalanza, A., Scalas, A.: Towards a hybrid verification methodology for communication protocols (short paper). In: Gotsman, A., Sokolova, A. (eds.) FORTE, volume 12136 of Lecture Notes in Computer Science, pp. 227–235. Springer, Cham (2020)
44.
Shijubo, J., Waga, M., Suenaga, K.: Efficient black-box checking via model checking with strengthened specifications. In: Feng, L., Fisman, D. (eds.) RV, volume 12974 of Lecture Notes in Computer Science, pp. 100–120. Springer, Cham (2021)
45.
Martinelli, F., Matteucci, I.: Partial model checking, process algebra operators and satisfiability procedures for (automatically) enforcing security properties. In: Foundations of Computer Security. Citeseer, pp. 133–144 (2005)
46.
Andersen, H.R.: Partial model checking. In: Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science. IEEE, pp. 398–407 (1995)
47.
Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and Boolean equation systems. In: Flanagan, C., König, B. (eds.) TACAS, pp. 141–156. Springer, Berlin (2012)
48.
Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sanchez, C. (eds.) Runtime Verification, pp. 473–481. Springer, Cham (2016)CrossRef
49.
Attard, D.P., Cassar, I., Francalanza, A., Aceto, L., Ingolfsdottir, A.: A Runtime Monitoring Tool for Actor-Based Systems, pp. 49–74. River Publishers, Aalborg (2017)
50.
Francalanza, A., Xuereb, J.: On implementing symbolic controllability. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION, volume 12134 of Lecture Notes in Computer Science, pp. 350–369. Springer, Cham (2020)
51.
Attard, D.P., Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Better late than never or: verifying asynchronous components at runtime. In: Peters, K., Willemse, T.A.C. (eds.) Formal Techniques for Distributed Objects, Components, and Systems—41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pp. 207–225. Springer, Cham (2021). https://​doi.​org/​10.​1007/​978-3-030-78089-0_​14
52.
Achilleos, A., Exibard, L., Francalanza, A., Lehtinen, K., Xuereb, J.: A synthesis tool for optimal monitors in a branching-time setting. In: ter Beek, M.H., Sirjani, M. (eds.) COORDINATION, volume 13271 of Lecture Notes in Computer Science, pp. 181–199. Springer, Cham (2022)
53.
Aceto, L., Achilleos, A., Attard, D.P., Exibard, L., Francalanza, A., Ingólfsdóttir, A.: A monitoring tool for linear-time \(\mu \)hml. In: ter Beek, M.H., Sirjani, M. (eds.) COORDINATION, volume 13271 of Lecture Notes in Computer Science, pp. 200–219. Springer, Cham (2022)
54.
55.
56.
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)MATHCrossRef
57.
Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007)MATHCrossRef
58.
59.
Stirling, C.: Handbook of logic in computer science, vol. 2. Modal and Temporal Logics, pp. 477–563. Oxford University Press, Inc., New York (1992)
60.
Stirling, C.: Model checking and other games. In: Notes for Mathfit Workshop on Finite Model Theory. University of Wales, Swansea (1996)
61.
Francalanza, A.: A Theory of Monitors (extended abstract). In: International Conference on Foundations of Software Science and Computation Structures. Springer, pp. 145–161 (2016)
62.
Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, pp. 8:1–8:19 (2017)
63.
d’Amorim, M., Roşu, G.: Efficient monitoring of \(\omega \)-languages. In: CAV, pp. 364–378 (2005)
64.
65.
66.
Debois, S., Hildebrandt, T., Slaats, T.: Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes. In: Bjørner, N., de Boer, F. (eds.) FM 2015: Formal Methods, pp. 143–160. Springer, Cham (2015)CrossRef
67.
68.
van Hulst, A.C., Reniers, M.A., Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic. Discrete Event Dyn. Syst. 27(1), 109–142 (2017)MathSciNetMATHCrossRef
69.
Milner, R.: Communication and Concurrency. PHI Series in Computer Science, Prentice Hall, Upper Saddle River (1989)MATH
70.
Bielova, N., Massacci, F.: Predictability of enforcement. In: Erlingsson, U., Wieringa, R., Zannone, N. (eds.) International Symposium on Engineering Secure Software and Systems, pp. 73–86. Springer, Berlin (2011)CrossRef
71.
Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: Cimatti, A., Sirjani, M. (eds.) Software Engineering and Formal Methods—15th International Conference, SEFM 2017, Trento, Italy, September 4–8, 2017, Proceedings, volume 10469 of Lecture Notes in Computer Science, pp. 219–235. Springer, Cham (2017). https://​doi.​org/​10.​1007/​978-3-319-66197-1_​14
72.
Aceto, L., Attard, D.P., Francalanza, A., Ingólfsdóttir, A.: On benchmarking for concurrent runtime verification. In: Guerra, E., Stoelinga, M. (eds.) Fundamental Approaches to Software Engineering—24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27–April 1 (2021), Proceedings, volume 12649 of Lecture Notes in Computer Science, pp. 3–23. Springer, Cham (2021). https://​doi.​org/​10.​1007/​978-3-030-71500-7_​1
73.
Aceto, L., Ingólfsdóttir, A.: Testing Hennessy–Milner logic with recursion. In: Thomas, W. (ed.) Foundations of Software Science and Computation Structures, pp. 41–55. Springer, Berlin (1999)CrossRef
74.
Rabinovich, A.M.: A complete axiomatisation for trace congruence of finite state behaviors. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pp. 530–543. Springer, London (1994)CrossRef
75.
Bielova, N.: A theory of constructive and predictable runtime enforcement mechanisms. Ph.D. Thesis, University of Trento (2011)
76.
Pnueli, Z.M.A.: A hierarchy of temporal properties. In: Proceedings of the 2nd Symposium. ACM of Principle Of Distributed Computer (1990)
77.
Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H.: Runtime enforcement of parametric timed properties with practical applications. In: IEEE International Workshop on Discrete Event Systems, Cachan, France, May, pp. 46–53 (2014)
78.
Pinisetty, S., Roop, P.S., Smyth, S., Tripakis, S., von Hanxleden, R.: Runtime enforcement of reactive systems using synchronous enforcers. CoRR, arxiv:​1612.​05030 (2016)
79.
Pinisetty, S., Roop, P.S., Smyth, S., Allen, N., Tripakis, S., Hanxleden, R.V.: Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 16(5), 178:1-178:25 (2017)
80.
81.
Martinelli, F., Matteucci, I.: Through modeling to synthesis of security automata. Electron. Not. Theor. Comput. Sci. 179, 31–46 (2006)CrossRef
82.
Martinelli, F., Matteucci, I.: An approach for the specification, verification and synthesis of secure systems. Electron. Not. Theor. Comput. Sci. 168, 29–43 (2007)CrossRef
83.
Castellani, I., Dezani-Ciancaglini, M., Pérez, J.A.: Self-adaptation and secure information flow in multiparty communications. Formal Asp. Comput. 28 (4): 669-696 (2016)
84.
Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: Abraham, E., Huisman, M. (eds.) International Conference on Integrated Formal Methods, pp. 176–192. Springer, Cham (2016)CrossRef
85.
Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors (extended abstract). In: Legay, A., Bensalem, S. (eds.) RV, volume 8174 of Lecture Notes in Computer Science, vol. 8174, pp. 112–129. Springer, Cham (2013)
Metadata
Title
On first-order runtime enforcement of branching-time properties
Authors
Luca Aceto
Ian Cassar
Adrian Francalanza
Anna Ingólfsdóttir
Publication date
03-08-2023
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 4/2023
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-023-00441-9

Other articles of this Issue 4/2023

Acta Informatica 4/2023 Go to the issue

Original Article

The second step in characterizing a three-word code

Review

Dot to dot, simple or sophisticated: a survey on shape reconstruction algorithms

Original Article

Testing membership for timed automata

Editorial

Editorial 2023: changes and invariants

Premium Partner

    Image Credits