Abstract
Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool Larva. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of Larva. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ahrendt, W.: Using KeY. In: Beckert et al. [11], pp. 409–451
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4, 32–54 (2005)
Aktug, I., Naliuka, K.: Conspec: A formal language for policy specification. In: FLACOS 2007, Oslo, Norway, pp. 107–109 (October 2007)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113–132. Springer, Heidelberg (2008)
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to aspectj. SIGPLAN Not. 40, 345–364 (2005)
Artho, C., Biere, A.: Combined static and dynamic analysis. In: AIOOL 2005. Electr. Notes Theor. Comput. Sci., vol. 131, pp. 3–14 (2005)
Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with slam. Commun. ACM 54(7), 68–76 (2011)
Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Beckert, B.: A Dynamic Logic for the Formal Verification of Java Card Programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6–24. Springer, Heidelberg (2001)
Beckert, B., Gladisch, C.: White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 207–216. Springer, Heidelberg (2007)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Bensalem, S., Lakhnech, Y., Owre, S.: InVeST: A tool for the verification of invariants. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 505–510. Springer, Heidelberg (1998)
Bhargavan, K., Gunter, C.A., Kim, M., Lee, I., Obradovic, D., Sokolsky, O., Viswanathan, M.: Verisim: Formal analysis of network simulations. IEEE Trans. Software Eng. 28(2), 129–145 (2002)
Bodden, E., Hendren, L.J., Lam, P., Lhoták, O., Naeem, N.A.: Collaborative Runtime Verification with Tracematches. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 22–37. Springer, Heidelberg (2007)
Bodden, E., Hendren, L.J., Lam, P., Lhoták, O., Naeem, N.A.: Collaborative runtime verification with tracematches. J. Log. Comput. 20(3), 707–723 (2010)
Bodden, E., Hendren, L., Lhoták, O.: A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 525–549. Springer, Heidelberg (2007)
Bodden, E., Lam, P., Hendren, L.J.: Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In: SIGSOFT FSE 2008, pp. 36–47. ACM (2008)
Bodden, E., Lam, P., Hendren, L.J.: Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 183–197. Springer, Heidelberg (2010)
Brucker, A.D., Wolff, B.: Interactive Testing with HOL-TestGen. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 87–102. Springer, Heidelberg (2006)
Burdy, L., Requet, A., Lanet, J.-L.: Java Applet Correctness: A Developer-Oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)
Chen, F., Roşu, G.: Java-MOP: A Monitoring Oriented Programming Environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005)
Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: SERP 2002, pp. 322–328. CSREA Press (2002)
Colombo, C.: Practical runtime monitoring with impact guarantees of Java programs with real-time constraints. Master’s thesis, University of Malta (2008)
Colombo, C., Pace, G.J., Abela, P.: Safer asynchronous runtime monitoring using compensations. Formal Methods in System Design 40, 1–26 (2012)
Colombo, C., Pace, G.J., Schneider, G.: Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135–149. Springer, Heidelberg (2009)
Colombo, C., Pace, G.J., Schneider, G.: Larva - a tool for runtime monitoring of java programs. In: SEFM 2009, pp. 33–37. IEEE Computer Society (2009)
d’Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. SIGSOFT Softw. Eng. Notes 30(4), 1–7 (2005)
D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: TIME 2005, pp. 166–174. IEEE Computer Society Press (June 2005)
Deng, X., Lee, J., Robby: Bogor/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE 2006, pp. 157–166. IEEE Computer Society (2006)
Engel, C., Hähnle, R.: Generating Unit Tests from Formal Proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169–188. Springer, Heidelberg (2007)
Ernst, M., Cockrell, J., Griswold, W., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27(2), 99–123 (2001)
Falzon, K.: Combining runtime verification and testing techniques. Master’s thesis, University of Malta (2010)
Goldberg, A., Havelund, K.: Automated runtime verification with eagle. In: MSVVEIS (2005)
Grieskamp, W., Tillmann, N., Schulte, W.: XRT — exploring runtime for.NET architecture and applications. In: Proc. Workshop on Software Model Checking (SoftMC 2005), Edinburgh, UK. Electr. Notes Theor. Comput. Sci, vol. 144(3), pp. 3–26 (2006)
Gupta, A., Majumdar, R., Rybalchenko, A.: From Tests to Proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262–276. Springer, Heidelberg (2009)
Hähnle, R., Baum, M., Bubel, R., Rothe, M.: A visual interactive debugger based on symbolic execution. In: ASE 2010, pp. 143–146. ACM, New York (2010)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580, 583 (1969)
Hunt, J.J., Jenn, E., Leriche, S., Schmitt, P., Tonin, I., Wonnemann, C.: A case study of specification and verification using JML in an avionics application. In: JTRES 2006, pp. 107–116. ACM Press (2006)
Jacobs, B., Marché, C., Rauch, N.: Formal Verification of a Commercial Smart Card Applet with Multiple Tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 241–257. Springer, Heidelberg (2004)
Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-mac: A run-time assurance approach for java programs. Formal Methods in System Design 24(2), 129–155 (2004)
King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: a java modeling language. In: Formal Underpinnings of Java Workshop, at OOPSLA 1998 (1998)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Draft Revision 1. 200 (2007)
Logozzo, F.: Our Experience with the CodeContracts Static Checker. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 241–242. Springer, Heidelberg (2012)
Meredith, P.O., Jin, D., Chen, F., Rosu, G.: Efficient monitoring of parametric context-free patterns. Autom. Softw. Eng. 17(2), 149–180 (2010)
Meyer, B.: Design by Contract. Technical Report TR-EI-12/CO, Interactive Software Engineering Inc. (1986)
Mostowski, W.: Formalisation and Verification of Java Card Security Properties in Dynamic Logic. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 357–371. Springer, Heidelberg (2005)
Pace, G.J., Schneider, G.: Challenges in the Specification of Full Contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 292–306. Springer, Heidelberg (2009)
Prisacariu, C., Schneider, G.: A dynamic deontic logic for complex contracts. J. Log. Algebr. Program 81(4), 458–490 (2012)
Rümmer, P.: Generating counterexamples for Java Dynamic logic. In: Prel. Proc. of Workshop on Disproving at CADE 2005, pp. 32–44 (2005)
Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: SEFM 2007, pp. 47–56. IEEE Press (2007)
Stenzel, K.: Verification of Java Card Programs. PhD thesis, Fakultät für angewandte Informatik, University of Augsburg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ahrendt, W., Pace, G.J., Schneider, G. (2012). A Unified Approach for Static and Runtime Verification: Framework and Applications. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2012. Lecture Notes in Computer Science, vol 7609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34026-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-34026-0_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34025-3
Online ISBN: 978-3-642-34026-0
eBook Packages: Computer ScienceComputer Science (R0)