×

zbMATH — the first resource for mathematics

A brief account of runtime verification. (English) Zbl 1192.68433
Summary: In this paper, a brief account of the field of runtime verification is given. Starting with a definition of runtime verification, a comparison to well-known verification techniques like model checking and testing is provided, and applications in which runtime verification brings out its distinguishing features are pointed out. Moreover, extensions of runtime verification such as monitor-oriented programming, and monitor-based runtime reflection are sketched and their similarities and differences are discussed. Finally, the use of runtime verification for contract enforcement is briefly pointed out.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Coq; JPAX
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] IEEE Std 1012-2004 IEEE standard for software verification and validation, IEEE Std 1012-2004 (Revision of IEEE Std 1012-1998), 2005, pp. 1-110.
[2] A. Alves, A. Arkin, S. Askary, C. Barreto, et al. Web services business process execution language version 2.0, April 2007, OASIS Standard. <http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html>.
[3] A. Banerji, C. Bartolini, D. Beringer, V. Chopella, et al. Web services conversation language (WSCL) 1.0, March 2002. W3C. <http://www.w3.org/TR/2002/NOTE-wscl10-20020314>.
[4] A. Abrahams. Developing and executing electronic commerce applications with occurrences, PhD thesis, University of Cambridge, 2002.
[5] Alur, R.; Dill, D., Automata for modeling real-time systems, (), 322-335 · Zbl 0765.68150
[6] H. Barringer, A. Goldberg, K. Havelund, K. Sen, Rule-based runtime verification, in: Verification, Model Checking, and Abstract Interpretation (VMCAI’04), pp. 44-57, 2004. · Zbl 1202.68243
[7] A. Bauer, M. Leucker, C. Schallhart, Model-based methods for the runtime analysis of reactive distributed systems, in: Proceedings of the Australian Software Engineering Conference (ASWEC’06), 2006, pp. 243-252.
[8] A. Bauer, M. Leucker, C. Schallhart, Monitoring of realtime properties, in: Foundations of Software Technology and Theoretical Computer Science (FSTTCS’06), 2006, pp. 260-272. · Zbl 1177.68141
[9] A. Bauer, M. Leucker, C. Schallhart, The good, the bad, and the ugly—but how ugly is ugly? in: Proceedings of the 7th International Workshop on Runtime Verification (RV’07), 2007, pp. 126-138.
[10] A. Bauer, M. Leucker, C. Schallhart. Runtime verification for LTL and TLTL, Technical Report TUM-I0724, TU München, 2007. · Zbl 1213.68363
[11] A. Bauer, M. Leucker, C. Schallhart. The good, the bad, and the ugly—but how ugly is ugly? Technical Report TUM-I0803, TU München, 2008.
[12] Bertot, Y.; Castéran, P., Interactive theorem proving and program development coq’art: the calculus of inductive constructions, An EATCS series, (2004), Springer · Zbl 1069.68095
[13] Biere, A.; Cimatti, A.; Clarke, E.; Strichman, O.; Zhu, Y., Bounded model checking, Advances in computers, vol. 58, (2003), Academic Press
[14] P. Bouyer, F. Chevalier, D. D’Souza, Fault diagnosis using timed automata, in: Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS’05), 2005, pp. 219-233. · Zbl 1118.68374
[15] T.D. Breaux, M.W. Vail, A.I. Anton, Towards regulatory compliance: extracting rights and obligations to align requirements with regulations, in: Proceedings of the 14th International Requirements Engineering Conference (RE’06), 2006.
[16] ()
[17] G. Castagna, N. Gesbert, L. Padovani, A theory of contracts for web services, in: Proceedings of the 35th Symposium on Principles of programming languages (POPL’08), 2008, pp. 261-272. · Zbl 1295.68080
[18] F. Chen, G. Roşu, MOP: an efficient and generic runtime verification framework, in: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications (OOPSLA’07), ACM, New York, NY, 2007, pp. 569-588.
[19] Chow, T.S., Testing software design modeled by finite-state machines, IEEE trans. softw. eng. (TSE), 4, 3, 178-187, (1978) · Zbl 0379.68039
[20] Clarke, E.M.; Grumberg, O.; Peled, D.A., Model checking, (1999), The MIT Press
[21] C. Colombo, G. Pace, G. Schneider, Dynamic event-based runtime monitoring of real-time and contextual properties, in: 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS’08). · Zbl 1262.68111
[22] J. Crow, J. Rushby, Model-based reconfiguration: diagnosis and recovery, NASA Contractor Report 4596, NASA Langley Research Center, 1994.
[23] M. d’Amorim, G. Rosu, Efficient monitoring of omega-languages. in: Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05), 2005, pp. 364-378. · Zbl 1081.68050
[24] B. D’Angelo, S. Sankaranarayanan, C. Sánchez, W. Robinson, B. Finkbeiner, H.B. Sipma, S. Mehrotra, Z. Manna, LOLA: runtime monitoring of synchronous systems, in: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME’05), 2005, pp. 166-174.
[25] Delgado, N.; Gates, A.Q.; Roach, S., A taxonomy and catalog of runtime software-fault monitoring tools, IEEE trans. softw. eng. (TSE), 30, 12, 859-872, (2004)
[26] Demri, S., LTL over integer periodicity constraints, Theoret. comput. sci. (TCS), 360, 1-3, 96-123, (2006) · Zbl 1097.68073
[27] N. Dinesh, A. Joshi, I. Lee, O. Sokolsky, Checking traces for regulatory conformance, in: Proceedings of the 8th International Workshop on Runtime Verification (RV’08), 2008. · Zbl 1143.03351
[28] W. Dong, M. Leucker, C. Schallhart, Impartial anticipation in runtime verification, in: Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA’08), 2008. · Zbl 1183.68367
[29] C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIsaac, D. Van Campenhout, Reasoning with temporal logic on truncated paths, in: Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), 2003, pp. 27-39. · Zbl 1278.68168
[30] M. Geilen, On the construction of monitors for temporal logic properties, Electron. Notes Theoret. Comput. Sci. (ENTCS) 55 (2) (2001).
[31] D. Giannakopoulou, K. Havelund, Automata-based verification of temporal properties on running programs, in: Proceedings of the 16th International Conference on Automated Software Engineering (ASE’01), 2001, pp. 412-416.
[32] D. Giannakopoulou, K. Havelund, Runtime analysis of linear temporal logic specifications, Technical Report 01.21, RIACS/USRA, 2001.
[33] C. Giblin, A. Liu, S. Muller, B. Pfitzmann, X. Zhou, Regulations expressed as logical models (realm), in: M.F. Moens, P. Spyns (Eds.), Legal Knowledge and Information Systems, 2005.
[34] Håkansson, J.; Jonsson, B.; Lundqvist, O., Generating online test oracles from temporal logic specifications, J. softw. tools technol. transfer (STTT), 4, 4, 456-471, (2003)
[35] K. Havelund, G. Rosu, Monitoring Java Programs with Java PathExplorer, Electron. Notes Theoret. Comput. Sci. (ENTCS) 55 (2) (2001). · Zbl 1073.68549
[36] K. Havelund, G. Rosu, Monitoring programs using rewriting, in: Proceedings of the 16th International Conference on Automated Software Engineering (ASE’01), 2001, p. 135.
[37] K. Havelund, G. Rosu, Synthesizing monitors for safety properties, in: Tools and Algorithms for Construction and Analysis of Systems (TACAS’02), 2002, pp. 342-356. · Zbl 1043.68534
[38] Havelund, K.; Rosu, G., Efficient monitoring of safety properties, J. softw. tools technol. transfer (STTT), (2004)
[39] Hinchey, M.; Sterritt, R., Self-managing software, IEEE comput., 39, 2, 107-109, (2006)
[40] Hoare, C.A.R., An axiomatic basis for computer programming, Commun. ACM (CACM), 12, 10, 576-580, (1969) · Zbl 0179.23105
[41] Hopcroft, J.E.; Ullman, J.D., Introduction to automata theory, Languages and computation, (1979), Addison-Wesley · Zbl 0196.01701
[42] H.W. Kamp, Tense logic and the theory of linear order, PhD Thesis, University of California, Los Angeles, 1968.
[43] Kupferman, O.; Vardi, M.Y., Model checking of safety properties, Form. methods syst. des. (FMSD), 19, 3, 291-314, (2001) · Zbl 0995.68061
[44] M. Kyas, C. Prisacariu, G. Schneider, Run-time monitoring of electronic contracts, in: 6th International Symposium on Automated Technology for Verification and Analysis (ATVA’08), 2008. · Zbl 1183.68074
[45] O. Maler, D. Nickovic, Monitoring temporal properties of continuous signals, in: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, and Formal Techniques in Real-Time and Fault-Tolerant Systems (FORMATS/FTRTFT’04), 2004, pp. 152-166. · Zbl 1109.68518
[46] O. Maler, D. Nickovic, A. Pnueli, From MITL to timed automata, in: Proceedings of the 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’06), 2006, pp. 274-289. · Zbl 1141.68436
[47] Manna, Z.; Pnueli, A., Temporal verification of reactive systems: safety, (1995), Springer New York
[48] B. Meyer, Contract-driven development, in: Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering (FASE’07), 2007, p. 11.
[49] Myers, G.J.; Badgett, T.; Thomas, T.M.; Sandler, C., The art of software testing, (2004), John Wiley and Sons
[50] D. Nickovic, O. Maler, Amt: a property-based monitoring tool for analog systems, in: Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’07), 2007, pp. 304-319.
[51] A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th Symposium on the Foundations of Computer Science (FOCS’77), 1977, pp. 46-57.
[52] A. Pnueli, A. Zaks, PSL Model checking and run-time verification via testers, in: Proceedings of the 14th International Symposium on Formal Methods (FM’06), 2006, pp. 573-586.
[53] A. Pretschner, M. Leucker, Model-based testing – a glossary, in: Broy et al. [16], pp. 607-609.
[54] C. Prisacariu, G. Schneider, A formal language for electronic contracts, in: 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS’07), 2007, pp. 174-189. · Zbl 1202.68266
[55] Raskin, J.-F.; Schobbens, P.-Y., The logic of event clocks—decidability, complexity and expressiveness, J. autom. lang. combin., 4, 3, 247-286, (1999) · Zbl 0978.03015
[56] G. Rosu, F. Chen, T. Ball, Synthesizing monitors for safety properties – this time with calls and returns, in: Proceedings of the 8th Workshop on Runtime Verification (RV’08).
[57] Sistla, A.P., Safety, liveness and fairness in temporal logic, Form. aspects comput., 6, 5, 495-512, (1994) · Zbl 0820.68077
[58] Sistla, A.P.; Clarke, E.M., Complexity of propositional temporal logics, J. ACM (jacm), 32, 733-749, (1985) · Zbl 0632.68034
[59] V. Stolz, Temporal assertions with parametrised propositions, in: Proceedings of the 7th International Workshop on Runtime Verification (RV’07), 2007, pp. 176-187.
[60] V. Stolz, E. Bodden, Temporal assertions using aspect, in: Proceedings of the 5th International Workshop on Runtime Verification (RV’05), 2006, pp. 109-124.
[61] S. Tripakis, Fault diagnosis for timed automata, in: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’02), 2002, pp. 205-224. · Zbl 1278.68140
[62] Tsai, J.J.P.; Bi, Y.-D.; Yang, S., Debugging for timing-constraint violations, IEEE softw., 13, 2, 89-99, (1996)
[63] Tsai, J.J.P.; Chen, H.-Y., A noninvasive architecture to monitor real-time distributed systems, IEEE comput., 23, 3, 11-23, (1990)
[64] Tsai, J.J.P.; Fang, K.-Y.; Chen, H.-Y.; Bi, Y.-D., A noninterference monitoring and replay mechanism for real-time software testing and debugging, IEEE trans. softw. eng. (TSE), 16, 8, 897-916, (1990)
[65] M.Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, in: Symposium on Logic in Computer Science (LICS’86), 1986, pp. 332-345.
[66] Vasilevski, M.P., Failure diagnosis of automata, Cybernetic, 9, 4, 653-665, (1973)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.