Andreas Bauer
Christian Schallhart
Skip Abstract Section
Abstract
This article studies runtime verification of properties expressed either in lineartime temporal logic (LTL) or timed lineartime temporal logic (TLTL). It classifies runtime verification in identifying its distinguishing features to model checking and testing, respectively. It introduces a three-valued semantics (with truth values true, false, inconclusive) as an adequate interpretation as to whether a partial observation of a running system meets an LTL or TLTL property.
For LTL, a conceptually simple monitor generation procedure is given, which is optimal in two respects: First, the size of the generated deterministic monitor is minimal, and, second, the monitor identifies a continuously monitored trace as either satisfying or falsifying a property as early as possible. The feasibility of the developed methodology is demontrated using a collection of real-world temporal logic specifications. Moreover, the presented approach is related to the properties monitorable in general and is compared to existing concepts in the literature. It is shown that the set of monitorable properties does not only encompass the safety and cosafety properties but is strictly larger.
For TLTL, the same road map is followed by first defining a three-valued semantics. The corresponding construction of a timed monitor is more involved, yet, as shown, possible.
- Aho, A., Sethi, R., and Ullman, J. 1986. Compilers: Principles and Techniques and Tools. Addison-Wesley. Google Scholar
Digital Library
- Allan, C., Avgustinov, P., Christensen, A. S., Hendren, L. J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., and Tibble, J. 2005. Adding trace matching with free variables to aspectj. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 345--364. Google ScholarDigital Library
- Alpern, B. and Schneider, F. B. 1987. Recognizing safety and liveness. Distrib. Comput. 2, 3, 117--126.Google ScholarDigital Library
- Alur, R. and Dill, D. L. 1994. A theory of timed automata. Theor. Comput. Sci. 126, 2, 183--235. Google ScholarDigital Library
- Alur, R., Courcoubetis, C., and Dill, D. L. 1993. Model-checking in dense real-time. Inform. Computat. 104, 1, 2--34. Google ScholarDigital Library
- Alur, R., Fix, L., and Henzinger, T. A. 1999. Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211, 1--2, 253--273. Google ScholarDigital Library
- Barbon, F., Traverso, P., Pistore, M., and Trainotti, M. 2006. Run-time monitoring of instances and classes of web service compositions. In Proceedings of the International Conference on Web Services (ICWS). IEEE Computer Society, 63--71. Google ScholarDigital Library
- Baresi, L., Guinea, S., and Pasquale, L. 2008. Towards a unified framework for the monitoring and recovery of bpel processes. In Proceedings of the Workshop on Testing, Analysis, and Verification of Web Services and Applications (TAV-WEB). T. Bultan and T. Xie Eds., ACM, 15--19. Google ScholarDigital Library
- Barringer, H., Goldberg, A., Havelund, K., and Sen, K. 2004. Program monitoring with ltl in eagle. In Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS).Google Scholar
- Barringer, H., Rydeheard, D. E., and Havelund, K. 2007. Rule systems for run-time monitoring: From eagle to ruler. In International Workshop on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 4839, 111--125. Google ScholarDigital Library
- Bauer, A., Leucker, M., and Schallhart, C. 2006a. Model-based runtime analysis of reactive distributed systems. In Proceedings of the Australian Software Engineering Conference (ASWEC). IEEE Computer Society, 243--252. Google ScholarDigital Library
- Bauer, A., Leucker, M., and Schallhart, C. 2006b. Monitoring of real-time properties. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). S. Arun-Kumar and N. Garg Eds., Lecture Notes in Computer Science, vol. 4337, Springer-Verlag, 260--272. Google ScholarDigital Library
- Bauer, A., Leucker, M., and Schallhart, C. 2007. The good, the bad, and the ugly---but how ugly is ugly? In Proceedings of the International Workshop on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 4839, Springer-Verlag, 126--138. Google ScholarDigital Library
- Bauer, A., Leucker, M., and Schallhart, C. 2010. Comparing LTL semantics for runtime verification. J. Logic Comput. 20, 3, 651--674. Google ScholarDigital Library
- Behrmann, G., David, A., Larsen, K. G., Håkansson, J., Pettersson, P., Yi, W., and Hendriks, M. 2006. Uppaal 4.0. In Proceedings of the International Conference on the Quantitative Evaluaiton of Systems (QEST). IEEE Computer Society, 125--126. Google ScholarDigital Library
- Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P., and Yi, W. 1996. UPPAAL: a tool suite for the automatic verification of real-time systems. In Hybrid Systems III. R. Alur, T. A. Henzinger, and E. D. Sontag Eds., Lecture Notes in Computer Science, vol. 1066., Springer-Verlag, 232--243. Google ScholarDigital Library
- Berg, T., Jonsson, B., Leucker, M., and Saksena, M. 2003. Insights to Angluin’s learning. In Proceedings of the International Workshop on Software Verification and Validation (SVV). Electronic Notes in Theoretical Computer Science, vol. 118, 3--18.Google ScholarCross Ref
- Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. 1999. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). R. Cleaveland Ed., Lecture Notes in Computer Science, vol. 1579, Springer, 193--207. Google ScholarDigital Library
- Biere, A., Cimatti, A., Clarke, E., Strichman, O., and Zhu, Y. 2003. Bounded model checking. In Advances in Computers, vol. 58. Academic Press, 118--149.Google Scholar
- Bodden, E. 2004. A lightweight ltl runtime verification tool for java. In OOPSLA Companion. J. M. Vlissides and D. C. Schmidt Eds., ACM, 306--307. Google ScholarDigital Library
- Bouyer, P., Chevalier, F., and D’Souza, D. 2005. Fault diagnosis using timed automata. In Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). V. Sassone Ed., Lecture Notes in Computer Science, vol. 3441, Springer, 219--233. Google ScholarDigital Library
- Bryant, R. E. 1985. Symbolic manipulation of boolean functions using a graphical representation. In Proceedings of the 22nd ACM/IEEE Design Automation Conference. IEEE Computer Society Press, 688--694. Google ScholarDigital Library
- Büchi, J. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science. 1--11.Google Scholar
- Chaudhuri, S. and Alur, R. 2007. Instrumenting c programs with nested word monitors. In Proceedings of the International SPIN Workshop. D. Bosnacki and S. Edelkamp Eds., Lecture Notes in Computer Science, vol. 4595, Springer, 279--283. Google ScholarDigital Library
- Chechik, M., Devereux, B., and Gurfinkel, A. 2001. Model-checking infinite state-space systems with fine-grained abstractions using spin. In Proceedings of the International SPIN Workshop. M. B. Dwyer Ed., Lecture Notes in Computer Science, vol. 2057, Springer, 16--36. Google ScholarDigital Library
- Chen, F. and Rosu, G. 2003. Towards monitoring-oriented programming: A paradigm combining specification and implementation. Electron. Notes Theor. Comput. Sci. 89, 2.Google ScholarCross Ref
- Chen, F. and Roşu, G. 2007. MOP: An Efficient and Generic Runtime Verification Framework. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). 569--588. Google ScholarDigital Library
- Chow, T. S. 1978. Testing software design modeled by finite-state machines. IEEE Trans. Softw. Engin 4, 3, 178--187. Google ScholarDigital Library
- Clarke, E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- d’Amorim, M. and Rosu, G. 2005. Efficient monitoring of omega-languages. In Proceedings of the International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 3576, 364--378. Google ScholarDigital Library
- D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H. B., Mehrotra, S., and Manna, Z. 2005. LOLA: Runtime monitoring of synchronous systems. In Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME). 166--174. Google ScholarDigital Library
- Delgado, N., Gates, A. Q., and Roach, S. 2004. A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Engin. 30, 12, 859--872. Google ScholarDigital Library
- Dewhurst, S. 2002. C++ Gotchas: Avoiding Common Problems in Coding and Design. Addison-Wesley Longman Publishing Co., Inc., Boston, MA. Google ScholarDigital Library
- Dill, D. L. 1989. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems. J. Sifakis Ed., Lecture Notes in Computer Science, vol. 407, Springer, 197--212. Google ScholarDigital Library
- D’Souza, D. 2003. A logical characterisation of event clock automata. Int. J. Found. Comput. Sci. 14, 4, 625--639.Google ScholarCross Ref
- Dwyer, M. B., Avrunin, G. S., and Corbett, J. C. 1999. Patterns in property specifications for finite-state verification. In Proceedings of the International Conference on Software Engineering (ICSE). IEEE, Computer Society Press, 411--420. Google ScholarDigital Library
- Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., and Campenhout, D. V. 2003. Reasoning with temporal logic on truncated paths. In Proceedings of the International Conference Computer Aided Verification (CAV). W. A. H. Jr. and F. Somenzi Eds., Lecture Notes in Computer Science, vol. 2725, Springer, 27--39.Google Scholar
- Erlingsson, Ú. and Schneider, F. B. 2000. Sasi enforcement of security policies: A retrospective. Proceedings of the DARPA Information Survivability Conference and Exposition 2, 1287.Google Scholar
- Finkbeiner, B. and Sipma, H. 2004. Checking finite traces using alternating automata. Form. Meth. Syst. Des. 24, 2, 101--127. Google ScholarDigital Library
- Fritz, C. 2003. Constructing Büchi automata from linear temporal logic using simulation relations for alternating büchi automata. In Proceedings of the International Conference on Implementation and Application of Automata (CIAA). O. H. Ibarra and Z. Dang Eds., Lecture Notes in Computer Science, vol. 2759, Springer, 35--48. Google ScholarDigital Library
- Gastin, P. and Oddoux, D. 2001. Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2102. Google ScholarDigital Library
- Geilen, M. 2001. On the construction of monitors for temporal logic properties. Electron. Notes Theor. Comput. Sci. 55, 2.Google ScholarCross Ref
- Giannakopoulou, D. and Havelund, K. 2001a. Automata-based verification of temporal properties on running programs. In Proceedings of the International Conference on Automated Software Engineering (ASE). IEEE Computer Society, 412--416. Google ScholarDigital Library
- Giannakopoulou, D. and Havelund, K. 2001b. Runtime analysis of linear temporal logic specifications. Tech. rep. 01.21, RIACS/USRA. Google ScholarDigital Library
- Goldsmith, S., O’Callahan, R., and Aiken, A. 2005. Relational queries over program traces. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 385--402. Google ScholarDigital Library
- Gollu, A., Puri, A., and Varaiya, P. 1994. Discretization of timed automata. In Proceedings of the 33rd IEEE Conference on Decision and Control. 957--958.Google Scholar
- Grinchtein, O. and Leucker, M. 2008. Network invariants for real-time systems. Form. Asp. Comput. 20, 619--635. Google ScholarCross Ref
- Håkansson, J., Jonsson, B., and Lundqvist, O. 2003. Generating online test oracles from temporal logic specifications. J. Softw. Tools Technol. Transfer 4, 4, 456--471.Google ScholarDigital Library
- Havelund, K. and Rosu, G. 2001. Monitoring Java Programs with Java PathExplorer. Electron. Notes Theor. Comput. Sci. 55, 2.Google ScholarCross Ref
- Havelund, K. and Rosu, G. 2002. Synthesizing Monitors for Safety Properties. In Proceedings of the Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 2280, 342--356. Google ScholarDigital Library
- Havelund, K. and Rosu, G. 2004. Efficient monitoring of safety properties. J. Softw. Tools Technol. Transfer 6, 2, 158--173. Google ScholarDigital Library
- Hopcroft, J. 1971. An n log n algorithm for minimizing states in a finite automation. In Theory of Machines and Computations. 189--196.Google Scholar
- Kamp, H. W. 1968. Tense logic and the theory of linear order. Ph.D. thesis, University of California, Los Angeles.Google Scholar
- Kim, M., Kannan, S., Lee, I., Sokolsky, O., and Viswanathan, M. 2002. Computational analysis of run-time monitoring/fundamentals of java-mac. Electron. Notes Theor. Comput. Sci. 70, 4.Google ScholarCross Ref
- Kim, M., Viswanathan, M., Kannan, S., Lee, I., and Sokolsky, O. 2004. Java-mac: A run-time assurance approach for java programs. Form. Meth. Syst. Des. 24, 2, 129--155. Google ScholarDigital Library
- Kopetz, H. 1991. Event-triggered versus time-triggered real-time systems. In Operating Systems of the 90s and Beyond. A. I. Karshmer and J. Nehmer Eds., Lecture Notes in Computer Science, vol. 563, Springer, 87--101. Google ScholarDigital Library
- Kupferman, O. and Vardi, M. Y. 2001. Model checking of safety properties. Form. Meth. Syst. Des. 19, 3, 291--314. Google ScholarDigital Library
- Lamport, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Engin. 3, 2, 125--143. Google ScholarDigital Library
- Lichtenstein, O. and Pnueli, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Conference on Principles of Programming Languages (POPL). ACM, New York, 97--107. Google ScholarDigital Library
- Maler, O. and Nickovic, D. 2004. Monitoring temporal properties of continuous signals. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems/Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FORMATS/FTRTFT). Y. Lakhnech and S. Yovine Eds., Lecture Notes in Computer Science, vol. 3253, Springer, 152--166.Google Scholar
- Manna, Z. and Pnueli, A. 1995. Temporal Verification of Reactive Systems: Safety. Springer, New York. Google ScholarDigital Library
- Markey, N. and Schnoebelen, P. 2003. Model checking a path. In Proceedings of the Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 2761, 248--262.Google Scholar
- Martin, M. C., Livshits, V. B., and Lam, M. S. 2005. Finding application errors and security flaws using pql: a program query language. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 365--383. Google ScholarDigital Library
- Peled, D., Vardi, M., and Yannakakis, M. 1999. Black box checking. In Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV). Kluwer, 225--240. Google ScholarDigital Library
- Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the Symposium on the Foundations of Computer Science (FOCS). IEEE Computer Society Press, 46--57. Google ScholarDigital Library
- Pnueli, A. and Zaks, A. 2006. PSL model checking and run-time verification via testers. In Proceedings of the International Symposium on Formal Methods (FM). J. Misra, T. Nipkow, and E. Sekerinski Eds., Lecture Notes in Computer Science, vol. 4085, Springer, 573--586. Google ScholarDigital Library
- Raskin, J.-F. 1999. Logics, automata and classical theories for deciding real-time. Ph.D. thesis, Namur, Belgium.Google Scholar
- Raskin, J.-F. and Schobbens, P.-Y. 1999. The logic of event clocks---decidability, complexity and expressiveness. J. Autom. Lang. Combina. 4, 3, 247--286. Google ScholarDigital Library
- Robinson, W. 2006. A requirements monitoring framework for enterprise systems. Require. Engin. 11, 1, 17--41. Google ScholarDigital Library
- Rosu, G. and Bensalem, S. 2006. Allen linear (interval) temporal logic - translation to LTL and monitor synthesis. In Proceedings of the International Conference on Computer Aided Verification (CAV). T. Ball and R. B. Jones Eds., Lecture Notes in Computer Science, vol. 4144, Springer, 263--277. Google ScholarDigital Library
- Schwoon, S. and Esparza, J. 2005. A note on on-the-fly verification algorithms. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 3440, 174--190. Google ScholarDigital Library
- Sen, K. and Rosu, G. 2003. Generating optimal monitors for extended regular expressions. Electron. Notes Theor. Comput. Sci. 89, 2.Google ScholarCross Ref
- Sistla, A. P. and Clarke, E. M. 1985. Complexity of propositional temporal logics. J. ACM 32, 733--749. Google ScholarDigital Library
- Stolz, V. and Bodden, E. 2006. Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144, 4, 109--124. Google ScholarDigital Library
- Stroustrup, B. 2000. The C++ Programming Language Special Ed. Addison-Wesley, Boston, MA. Google ScholarDigital Library
- Tarjan, R. 1972. Depth-first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146--160.Google ScholarDigital Library
- Thati, P. and Rosu, G. 2005. Monitoring algorithms for metric temporal logic specifications. Electron. Notes Theor. Comput. Sci. 113, 145--162. Google ScholarDigital Library
- Tripakis, S. 2002. Fault diagnosis for timed automata. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). W. Damm and E.-R. Olderog Eds., Lecture Notes in Computer Science, vol. 2469, Springer, 205--224. Google ScholarDigital Library
- Tripakis, S. and Yovine, S. 2001. Analysis of timed systems using time-abstracting bisimulations. Form. Meth. Syst. Des. 18, 1, 25--68. Google ScholarDigital Library
- Vardi, M. Y. 1996. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure Versus Automata. Lecture Notes in Computer Science, vol. 1043, 238--266. Google ScholarDigital Library
- Vardi, M. Y. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, 332--345.Google Scholar
- Vasilevski, M. 1973. Failure diagnosis of automata. Cybernetic 9, 4, 653--665.Google ScholarCross Ref
Index Terms
- Runtime Verification for LTL and TLTL
Recommendations
Optimized temporal monitors for SystemC
SystemC is a modeling language built as an extension of C++ . Its growing popularity and the increasing complexity of designs have motivated research efforts aimed at the verification of SystemC models using assertion-based verification (ABV), where ...
A lightweight LTL runtime verification tool for java
OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applicationsRuntime verification is a special form of runtime testing, employing formal methods and languages. In this work, we utilize next-time free linear-time temporal logic (LTL\textbackslash X) as formal framework. The discipline serves the purpose of ...
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...
Comments