Document Open Access Logo

Consistently-Detecting Monitors

Author Adrian Francalanza

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2017.8.pdf
  • Filesize: 0.71 MB
  • 19 pages

Document Identifiers

Subject Classification

Keywords
  • Runtime Monitoring
  • Deterministic Behaviour
  • Controllability
  • Compositional Reasoning
  • Symbolic Analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We study a contextual definition for deterministic monitoring based on consistent detections. It is defined in terms of the observed behaviour of the monitor when instrumented over arbitrary systems. We give an alternative, coinductive definition based on controllability which does not rely on system quantifications, and show that it is fully-abstract with respect to the former definition. We then develop a symbolic counterpart to the controllability definition to facilitate an automated analysis for controllable monitors involving data.

Cite As Get BibTex

Adrian Francalanza. Consistently-Detecting Monitors. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.8

Author Details

Adrian Francalanza

References

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Sævar Örn Kjartansson. On the Complexity of Determinizing Monitors. In CIAA, pages 1-13, 2017. URL: http://dx.doi.org/10.1007/978-3-319-60134-2_1.
  2. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge Univ. Press, 2007. Google Scholar
  3. Luca Aceto, Anna Ingolfsdottir, and Jiri Srba. Advanced Topics in Bisimulation and Coinduction, chapter The Algorithmics of Bisimilarity. Cambridge Univ. Press, 2011. Google Scholar
  4. Cyril Allauzen, Mehryar Mohri, and Ashish Rastogi. General algorithms for testing the ambiguity of finite automata. In DTL, pages 108-120, 2008. URL: http://dx.doi.org/10.1007/978-3-540-85780-8_8.
  5. Howard Barringer, Yliès Falcone, Klaus Havelund, Giles Reger, and David E. Rydeheard. Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. In FM, pages 68-84, 2012. URL: http://dx.doi.org/10.1007/978-3-642-32759-9_9.
  6. David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu. Monitoring compliance policies over incomplete and disagreeing logs. In RV, pages 151-167, 2013. URL: http://dx.doi.org/10.1007/978-3-642-35632-2_17.
  7. Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. TOSEM, 20(4):14, 2011. Google Scholar
  8. Shay Berkovich, Borzoo Bonakdarpour, and Sebastian Fischmeister. Runtime verification with minimal intrusion through parallelism. Formal Methods in System Design, 46(3):317-348, 2015. URL: http://dx.doi.org/10.1007/s10703-015-0226-3.
  9. Giovanni Bernardi and Adrian Francalanza. Full-abstraction for must testing preorders. In COORDINATION, pages 237-255, 2017. URL: http://dx.doi.org/10.1007/978-3-319-59746-1_13.
  10. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. TCS, 669:33-58, 2017. URL: http://dx.doi.org/10.1016/j.tcs.2017.02.009.
  11. Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers. Decentralized asynchronous crash-resilient runtime verification. In CONCUR, pages 16:1-16:15, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.16.
  12. Ian Cassar and Adrian Francalanza. Runtime Adaptation for Actor Systems. In RV, volume 9333, pages 38-54. Springer, 2015. Google Scholar
  13. Ian Cassar and Adrian Francalanza. On Implementing a Monitor-Oriented Programming Framework for Actor Systems. In iFM, pages 176-192, 2016. Google Scholar
  14. Feng Chen and Grigore Roşu. MOP: An Efficient and Generic Runtime Verification Framework. In OOPSLA, pages 569-588, 2007. URL: http://dx.doi.org/10.1145/1297027.1297069.
  15. Rance Cleaveland and Matthew Hennessy. Testing equivalence as a bisimulation equivalence. FACS, 5(1):1-20, 1993. Google Scholar
  16. Christian Colombo, Adrian Francalanza, Ruth Mizzi, and Gordon J. Pace. polylarva: Runtime verification with configurable resource-aware monitoring boundaries. In SEFM, pages 218-232, 2012. Google Scholar
  17. Marcelo d'Amorim and Grigore Roşu. Efficient monitoring of ω-languages. In CAV, pages 364 - 378, 2005. Google Scholar
  18. Søren Debois, Thomas Hildebrandt, and Tijs Slaats. Safety, liveness and run-time refinement for modular process-aware systems with dynamic sub processes. In FM, pages 143-160, 2015. URL: http://dx.doi.org/10.1007/978-3-319-19249-9_10.
  19. Normann Decker and Daniel Thoma. On freeze LTL with ordered attributes. In FOSSACS, pages 269-284, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_16.
  20. John Dorsey. Continuous and Discrete Control Systems: Modeling, Identification, Design, and Implementation. McGraw-Hill, 2001. Google Scholar
  21. Pierre Fraigniaud, Sergio Rajsbaum, and Corentin Travers. On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems. In RV, pages 92-107, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11164-3_9.
  22. Adrian Francalanza. A Theory of Monitors. In FoSSaCS, pages 145-161, 2016. Google Scholar
  23. Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. Monitorability for the Hennessy-Milner logic with recursion. FMSD, pages 1-30, 2017. URL: http://dx.doi.org/10.1007/s10703-017-0273-z.
  24. Adrian Francalanza and Aldrin Seychell. Synthesising Correct concurrent Runtime Monitors. FMSD, 46(3):226-261, 2015. URL: http://dx.doi.org/10.1007/s10703-014-0217-9.
  25. Jan Friso Groote and M.P.A. Sellink. Confluence for process verification. TCS, 170(1):47 - 81, 1996. URL: http://dx.doi.org/10.1016/S0304-3975(96)80702-X.
  26. Yuqin He, Xiangping Chen, and Ge Lin. Composition of monitoring components for on-demand construction of runtime model based on model synthesis. In Internetware, pages 1-5, 2013. URL: http://dx.doi.org/10.1145/2532443.2532472.
  27. Matthew Hennessy and Anna Ingolfsdottir. A Theory of Communicating Processes with Value Passing. Information and Computation, 107(2):202 - 236, 1993. URL: http://dx.doi.org/10.1006/inco.1993.1067.
  28. Matthew Hennessy and Huimin Lin. Symbolic bisimulations. TCS, 138(2):353 - 389, 1995. URL: http://dx.doi.org/10.1016/0304-3975(94)00172-F.
  29. Oscar H. Ibarra and Bala Ravikumar. On Sparseness, Ambiguity and other decision problems for Acceptors and Transducers. In STACS, pages 171-179, 1986. URL: http://dx.doi.org/10.1007/3-540-16078-7_74.
  30. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In POPL, pages 582-594, 2016. URL: http://dx.doi.org/10.1145/2837614.2837662.
  31. Jerzy Klamka. Control System, Robotics and Automation, volume 7, chapter System Characteristics: Stability, Controllability, Observability. EOLLS, 2009. Google Scholar
  32. John Klein and Ian Gorton. Runtime Performance Challenges in Bigdata Systems. In WOSP, pages 17-22, 2015. URL: http://dx.doi.org/10.1145/2693561.2693563.
  33. D. König. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Litt. ac. sci. Szeged, 3, 1927. Google Scholar
  34. Dexter Kozen. Results on the propositional μ-calculus. TCS, 27:333-354, 1983. Google Scholar
  35. Jonathan Laurent, Alwyn Goodloe, and Lee Pike. Assuring the Guardians. In RV, pages 87-101, 2015. Google Scholar
  36. Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur., 4(1-2):2-16, 2005. URL: http://dx.doi.org/10.1007/s10207-004-0046-8.
  37. Qingzhou Luo and Grigore Roşu. EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs. In ISSTA, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2483760.2483766.
  38. Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, and Grigore Roşu. An overview of the MOP runtime verification framework. STTT, 14(3):249-289, 2012. URL: http://dx.doi.org/10.1007/s10009-011-0198-6.
  39. Luca Padovani. Contract-based discovery of web services modulo simple orchestrators. TCS, 411(37), 2010. Google Scholar
  40. Anna Philippou and David Walker. On confluence in the π-calculus. In ICALP, pages 314-324, 1997. URL: http://dx.doi.org/10.1007/3-540-63165-8_188.
  41. Giles Reger, Helena Cuenca Cruz, and David E. Rydeheard. MarQ: Monitoring at Runtime with QEA. In TACAS, pages 596-610, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46681-0_55.
  42. Davide Sangiorgi. An introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  43. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, 2000. URL: http://dx.doi.org/10.1145/353323.353382.
  44. Michael Sipser. Introduction to the Theory of Computation. Cengage Learning, 3rd edition, 2012. Google Scholar
  45. Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Inf.&Comp., 115(1):1-37, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1092.
  46. Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, and Mitsuharu Yamamoto. Runtime monitoring for concurrent systems. In RV, pages 386-403, 2016. URL: http://dx.doi.org/10.1007/978-3-319-46982-9_24.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact