Abstract
The LogicGuard specification language for the runtime monitoring of message/event streams specifies monitors by predicate logic formulas of a certain kind. In this paper we present an algorithm that gives upper bounds for the space requirements of monitors specified in a formally elaborated core of this language. This algorithm has been implemented in the LogicGuard software and experiments have been carried out to demonstrate the accuracy of its predictions.
Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 “LogicGuard II”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Büchi, J.R.: Weak SO arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66–92 (1960)
Cerna, D.: Space Complexity of LogicGuard Revisited. Technical report, RISC, JKU, Linz, October 2015
Cerna, D.M., Schreiner, W., Kutsia, T.: Space analysis of a predicate logic fragment for the specification of stream monitors. In: Davenport, J.H., Ghourabi, F. (eds.) 7th International Symposium on Symbolic Computation in Software Science. EPiC Computing, vol. 39, pp. 29–41 (2016)
Colombo, C., Pace, G.J., Schneider, G.: LARVA—safer monitoring of real-time Java programs (Tool Paper). In: 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, pp. 33–37, November 2009
D’Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174, June 2005
Finkbeiner, B., Kuhtz, L.: Monitor circuits for LTL with bounded and unbounded future. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 60–75. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04694-0_5
Frick, M., Grohe, M.: The complexity of FO and monadic SO logic revisited. Ann. Pure Appl. Logic 130(1–3), 3–31 (2004)
IEEE Std 1850-2007: Standard for Property Specification Language (PSL) (2007)
Kupferman, O., Lustig, Y., Vardi, M.Y.: On locally checkable properties. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 302–316. Springer, Heidelberg (2006). doi:10.1007/11916277_21
Kutsia, T., Schreiner, W.: Verifying the Soundness of Resource Analysis for LogicGuard Monitors. Technical Report 14–08, RISC, JKU, Linz (2014)
LogicGuard II, November 2015. http://www.risc.jku.at/projects/LogicGuard2/
Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: past, present, future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2–16. Springer, Heidelberg (2005). doi:10.1007/11603009_2
McNaughton, R., Papert, S.: Counter-Free Automata. Research Monograph, vol. 65. MIT Press, Cambridge (1971)
Schreiner, W., Kutsia, T., Cerna, D., Krieger, M., Ahmad, B., Otto, H., Rummerstorfer, M., Gössl, T.: The LogicGuard Stream Monitor Specification Language (Version 1.01). Tutorial and Reference Manual, RISC, JKU, Linz (2015)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, 16–18 June, Cambridge, Massachusetts, USA, pp. 332–344. IEEE Computer Society (1986)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Cerna, D.M., Schreiner, W., Kutsia, T. (2016). Predicting Space Requirements for a Stream Monitor Specification Language. In: Falcone, Y., Sánchez, C. (eds) Runtime Verification. RV 2016. Lecture Notes in Computer Science(), vol 10012. Springer, Cham. https://doi.org/10.1007/978-3-319-46982-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-46982-9_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46981-2
Online ISBN: 978-3-319-46982-9
eBook Packages: Computer ScienceComputer Science (R0)