Efficient monitoring of parametric context-free patterns
Tóm tắt
Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite automata, limiting their expressivity. For example, neither can specify structured properties that refer to the call stack of the program. While context-free grammars (CFGs) are expressive and well-understood, existing techniques for monitoring CFGs generate large runtime overhead in real-life applications. This paper demonstrates that monitoring parametric CFGs is practical (with overhead on the order of 12% or lower in most cases). We present a monitor synthesis algorithm for CFGs based on an LR(1) parsing algorithm, modified to account for good prefix matching. In addition, a logic-independent mechanism is introduced to support matching against the suffixes of execution traces.
Tài liệu tham khảo
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers, Principles, Techniques, and Tools. Addison-Wesley, Reading (1986), pp. 215–246
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA’05, pp. 345–364. ACM, New York (2005)
Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhotak, J., Lhotak, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: ABC: an extensible AspectJ compiler. In: AOSD’05, pp. 87–98. ACM, New York (2005)
Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. In: OOPSLA’07, pp. 589–608. ACM, New York (2007)
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from eagle to ruler. J. Log. Comput. exn076+ (2008)
Blackburn, S.M., Garner, R., Hoffman, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M. Lee, H., Moss, J.E.B., Phansalkar, A., Stefanović, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA’06, pp. 169–190. ACM, New York (2006)
Bodden, E.: J-LO, a tool for runtime-checking temporal assertions. Master’s thesis, RWTH Aachen University (2005)
Bodden, E., Hendren, L., Lhoták, O.: A staged static program analysis to improve the performance of runtime monitoring. In: ECOOP’07. LNCS, vol. 4609, pp. 525–549. Springer, Berlin (2007)
Bodden, E. Lam, P., Hendren, L.: Tracematches Benchmarks (2008). http://abc.comlab.ox.ac.uk/tmahead
Chaudhuri, S., Alur, R.: Instrumenting C programs with nested word monitors. In: Model Checking Software (SPIN’07). LNCS, vol. 4595, pp. 279–283. Springer, Berlin (2007)
Chen, F., Roşu, G.: Towards monitoring-oriented programming: A paradigm combining specification and implementation. In: Runtime Verification (RV’03). ENTCS, vol. 89 (2003)
Chen, F., Roşu, G.: MOP: An efficient and generic runtime verification framework. In: OOPSLA’07, pp. 569–588. ACM, New York (2007)
Chen, F., Roşu, G.: Parametric trace slicing and monitoring. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS’09). LNCS, vol. 5505, pp. 246–261. Springer, Berlin (2009)
Chen, F., D’Amorim, M., Roşu, G.: A formal monitoring-based framework for software development and analysis. In: ICFEM’04. LNCS, vol. 3308, pp. 357–372. Springer, Berlin (2004)
Chen, F., D’Amorim, M., Roşu, G.: Checking and correcting behaviors of Java programs at runtime with JavaMOP. In: Runtime Verification(RV’06), ENTCS, vol. 144, pp. 3–20 (2006)
Chen, F., Meredith, P., Jin, D., Rosu, G.: Efficient formalism-independent monitoring of parametric properties. In: Automated Software Engineering (ASE’09), IEEE, pp. 383–394 (2009)
d’Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. ACM SIGSOFT Softw. Eng. Not. 30(4), 1–7 (2005)
Drusinsky, D.: Temporal Rover (1997–2009). http://www.time-rover.com
Duncan, A.G.: Test grammars: A method for generating program test data. In: Workshop on Software Testing and Test Documentation, pp. 270–281 (1978)
Duncan, A.G., Hutchison, J.S.: Using attributed grammars to test designs and implementations. In: International Conference on Software Engineering (ICSE’81), pp. 170–178 (1981)
Goldsmith, S., O’Callahan, R., Aiken, A.: Relational queries over program traces. In: OOPSLA’05, pp. 385–402. ACM, New York (2005)
Hanford, K.: Automatic generation of test cases. IBM Syst. J. 9(4), 242–257 (1970)
Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. In: Runtime Verification(RV’01), ENTCS, vol. 55 (2001)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 2nd edn. Addison-Wesley, Reading (2001)
Houssais, B.: Verification of an Algol 68 implementation. In: Strathclyde Algol 68 Conference (1977)
Hughes, G., Bultan, T.: Interface grammars for modular software model checking. In: International Symposium on Software Testing and Analysis (ISSTA’07), pp. 39–49. ACM, New York (2007)
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: ECOOP’01. LNCS, vol. 2072, pp. 327–353. Springer, Berlin (2001)
Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: A run-time assurance approach for Java programs. Form. Methods Syst. Des. 24(2), 129–155 (2004)
Knuth, D.E.: On the translation of languages from left to right. Inf. Control 8(6), 607–639 (1965)
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA’00, pp. 105–106. ACM, New York (2000)
Martin, M., Livshits, V.B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. In: OOPSLA’07, pp. 365–383. ACM, New York (2005)
Maurer, P.M.: Generating test data with enhanced context-free grammars. IEEE Softw. 7(4), 50–55 (1990)
Meredith, P., Jin, D., Chen, F., Roşu, G.: Efficient monitoring of parametric context-free patterns. In: Automated Software Engineering (ASE ’08), IEEE, pp. 148–15 (2008)
Purdom, P.: A sentence generator for testing parsers. BIT 2, 336–375 (1972)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)
Sirer, E., Bershad, B.: Using production grammars in software testing. In: Domain Specific Languages (DSL’00), pp. 1–13 (1999)