Skip to main content
SpringerLink
Log in

Comparing Controlled System Synthesis and Suppression Enforcement

  • Conference paper
  • First Online:
Runtime Verification (RV 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11757))

Included in the following conference series:

Abstract

Runtime enforcement and control system synthesis are two verification techniques that automate the process of transforming an erroneous system into a valid one. As both techniques can modify the behaviour of a system to prevent erroneous executions, they are both ideal for ensuring safety. In this paper, we investigate the interplay between these two techniques and identify control system synthesis as being the static counterpart to suppression-based runtime enforcement, in the context of safety properties.

This work was partly supported by the projects “TheoFoMon: Theoretical Foundations for Monitorability” (nr. 163406-051) and “Developing Theoretical Foundations for Runtime Enforcement” (nr. 184776-051) of the Icelandic Research Fund, by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement nr. 778233, and by the Endeavour Scholarship Scheme (Malta), part-financed by the European Social Fund (ESF) - Operational Programme II – Cohesion Policy 2014–2020.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abramsky, S.: Observation equivalence as a testing equivalence. Theoret. Comput. Sci. 53, 225–241 (1987). https://doi.org/10.1016/0304-3975(87)90065-X

    Article  MathSciNet  MATH  Google Scholar 

  2. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: A framework for parameterized monitorability. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 203–220. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_11

    Chapter  Google Scholar 

  3. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Kjartansson, S.Ö.: Determinizing monitors for HML with recursion. arXiv preprint (2016)

    Google Scholar 

  4. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1–52:29 (2019). https://doi.org/10.1145/3290365. http://doi.acm.org/10.1145/3290365

    Article  Google Scholar 

  5. Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: On runtime enforcement via suppressions. In: 29th International Conference on Concurrency Theory, CONCUR 2018, Beijing, China, 4–7 September 2018, pp. 34:1–34:17 (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.34

  6. Aceto, L., Ingólfsdóttir, A.: Testing Hennessy-Milner logic with recursion. In: Thomas, W. (ed.) FoSSaCS 1999. LNCS, vol. 1578, pp. 41–55. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49019-1_4

    Chapter  Google Scholar 

  7. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007)

    Book  Google Scholar 

  8. 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 (2011)

    Google Scholar 

  9. Arnold, A., Walukiewicz, I.: Nondeterministic controllers of nondeterministic processes. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata. Texts in Logic and Games, vol. 2, pp. 29–52. Amsterdam University Press, Amsterdam (2008)

    Google Scholar 

  10. Basile, D., ter Beek, M.H., Pugliese, R.: Bridging the gap between supervisory control and coordination of services: synthesis of orchestrations and choreographies. In: Riis Nielson, H., Tuosto, E. (eds.) COORDINATION 2019. LNCS, vol. 11533, pp. 129–147. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22397-7_8

    Chapter  Google Scholar 

  11. Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: A survey of runtime monitoring instrumentation techniques. In: PrePost 2017, pp. 15–28 (2017)

    Article  Google Scholar 

  12. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    MATH  Google Scholar 

  13. Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 172–189. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_11

    Chapter  Google Scholar 

  14. Ehlers, R., Lafortune, S., Tripakis, S., Vardi, M.Y.: Bridging the gap between supervisory control and reactive synthesis: case of full observation and centralized control. In: WODES, pp. 222–227. International Federation of Automatic Control (2014)

    Google Scholar 

  15. Erlingsson, U., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: Proceedings of the 1999 Workshop on New Security Paradigms, NSPW 1999, pp. 87–95. ACM, New York (1999)

    Google Scholar 

  16. Falcone, Y., Marchand, H.: Runtime enforcement of k-step opacity. In: 52nd IEEE Conference on Decision and Control, pp. 7271–7278, December 2013. https://doi.org/10.1109/CDC.2013.6761043

  17. Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transfer 14(3), 349 (2012)

    Article  Google Scholar 

  18. Francalanza, A.: A theory of monitors. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 145–161. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49630-5_9

    Chapter  MATH  Google Scholar 

  19. Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 85, pp. 8:1–8:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017)

    Google Scholar 

  20. Francalanza, A., et al.: A foundation for runtime monitoring. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 8–29. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_2

    Chapter  Google Scholar 

  21. 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)

    Article  Google Scholar 

  22. Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transfer 2(4), 366–381 (2000). https://doi.org/10.1007/s100090050043

    Article  MATH  Google Scholar 

  23. Havelund, K., Roşu, G.: An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst. Des. 24(2), 189–215 (2004)

    Article  Google Scholar 

  24. 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)

    Article  MathSciNet  Google Scholar 

  25. Kejstová, K., Ročkai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 225–240. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_14

    Chapter  Google Scholar 

  26. Könighofer, B., et al.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332–361 (2017)

    Article  Google Scholar 

  27. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293–303 (2009)

    Article  Google Scholar 

  28. Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1), 2–16 (2005)

    Article  Google Scholar 

  29. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1–40 (1992)

    Article  MathSciNet  Google Scholar 

  30. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989, pp. 179–190. ACM, New York (1989). https://doi.org/10.1145/75277.75293. http://doi.acm.org/10.1145/75277.75293

  31. Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)

    Article  MathSciNet  Google Scholar 

  32. Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York (2009)

    Book  Google Scholar 

  33. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)

    Book  Google Scholar 

  34. Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3(1), 30–50 (2000)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Gran Sasso Science Institute, L’Aquila, Italy

    Luca Aceto

  2. School of Computer Science, Reykjavík University, Reykjavík, Iceland

    Luca Aceto, Ian Cassar & Anna Ingólfsdóttir

  3. Department of Computer Science, University of Malta, Msida, Malta

    Ian Cassar & Adrian Francalanza

Authors
  1. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ian Cassar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Adrian Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Anna Ingólfsdóttir
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ian Cassar .

Editor information

Editors and Affiliations

  1. Universität des Saarlandes, Saarbrücken, Germany

    Bernd Finkbeiner

  2. University of Milano Bicocca, Milan, Italy

    Leonardo Mariani

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A. (2019). Comparing Controlled System Synthesis and Suppression Enforcement. In: Finkbeiner, B., Mariani, L. (eds) Runtime Verification. RV 2019. Lecture Notes in Computer Science(), vol 11757. Springer, Cham. https://doi.org/10.1007/978-3-030-32079-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32079-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32078-2

  • Online ISBN: 978-3-030-32079-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation