Abstract
The underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the spaces of properties for which runtime verification approaches can be applied to.
This paper presents a unified view of runtime verification and enforcement of properties in the safety-progress classification. Firstly, we characterize the set of properties which can be verified (monitorable properties) and enforced (enforceable properties) at runtime. We propose in particular an alternative definition of “property monitoring” to the one classically used in this context. Secondly, for the delineated spaces of properties, we obtain specialized verification and enforcement monitors.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Runtime Verification (2001-2009), http://www.runtime-verification.org
Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Journal of Logic and Computation (2008) (accepted for publication)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. Technical Report TUM-I0724, Institut für Informatik, Technische Universität München (2007)
Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 374–383. Springer, Heidelberg (2008)
Roşu, G., Chen, F., Ball, T.: Synthesizing monitors for safety properties – this time with calls and returns. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 51–68. Springer, Heidelberg (2008)
Havelund, K., Rosu, G.: Efficient monitoring of safety properties. Software Tools and Technology Transfer (2002)
d’Amorim, M., Roşu, G.: Efficient monitoring of ω-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 30–50 (2000)
Hamlen, K.W., Morrisett, G., Schneider, F.B.: Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst. 28, 175–205 (2006)
Viswanathan, M.: Foundations for the run-time analysis of software systems. PhD thesis, University of Pennsylvania, Philadelphia, PA, USA (2000)
Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Transactions on Information and System Security 12, 1–41 (2009)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties, invited paper 1989. In: PODC 1990: Proceedings of the ninth annual ACM symposium on Principles of distributed computing, pp. 377–410. ACM, New York (1990)
Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474–486. Springer, Heidelberg (1992)
Falcone, Y., Fernandez, J.C., Mounier, L.: Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 41–55. Springer, Heidelberg (2008)
Falcone, Y., Fernandez, J.C., Mounier, L.: Enforcement Monitoring wrt. the Safety-Progress Classification of Properties. In: SAC 2009: Proceedings of the 2009 ACM symposium on Applied Computing, pp. 593–600. ACM, New York (2009)
Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime Verification of Safety-Progress Properties. Technical Report TR-2009-6, Verimag Research Report (2009)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19, 291–314 (2001)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125–143 (1977)
Alpern, B., Schneider, F.B.: Defining liveness. Technical report, Cornell University, Ithaca, NY, USA (1984)
Ligatti, J., Bauer, L., Walker, D.: Enforcing Non-safety Security Policies with Program Monitors. In: de di Vimercati, S.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 355–373. Springer, Heidelberg (2005)
Chen, F., Roşu, G.: MOP: An Efficient and Generic Runtime Verification Framework. In: Object-Oriented Programming, Systems, Languages and Applications(OOPSLA 2007), pp. 569–588. ACM press, New York (2007)
Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78, 293–303 (2008)
Martinell, F., Matteucci, I.: Through modeling to synthesis of security automata. Electron. Notes Theor. Comput. Sci. 179, 31–46 (2007)
Matteucci, I.: Automated synthesis of enforcing mechanisms for security properties in a timed setting. Electron. Notes Theor. Comput. Sci. 186, 101–120 (2007)
Streett, R.S.: Propositional dynamic logic of looping and converse. In: STOC 1981: Proceedings of the thirteenth annual ACM symposium on Theory of computing, pp. 375–383. ACM, New York (1981)
Falcone, Y., Fernandez, J.C., Mounier, L.: Specifying Properties for Runtime Verification in the Safety-Progress Classification. Technical Report TR-2009-5, Verimag Research Report (2009)
Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1, 146–160 (1972)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Falcone, Y., Fernandez, JC., Mounier, L. (2009). Runtime Verification of Safety-Progress Properties. In: Bensalem, S., Peled, D.A. (eds) Runtime Verification. RV 2009. Lecture Notes in Computer Science, vol 5779. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04694-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-04694-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04693-3
Online ISBN: 978-3-642-04694-0
eBook Packages: Computer ScienceComputer Science (R0)