Abstract
In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing the use of some resource, such as execution time, energy, or user-defined resources. In previous work we have presented a novel framework for data size-dependent, static resource usage verification (which can also be combined with run-time tests). Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach, in this paper we provide a number of novel contributions: we present a more complete formalization and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Albert, E., Arenas, P., Genaim, S., Herraiz, I., Puebla, G.: Comparing Cost Functions in Resource Analysis. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 1–17. Springer, Heidelberg (2010)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: Proc. of PLDI 2003. ACM Press (2003)
Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Programming Languages Design and Implementation 1993, pp. 46–55 (1993)
Bueno, F., Deransart, P., Drabent, W., Ferrand, G., Hermenegildo, M., Maluszynski, J., Puebla, G.: On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs. In: Proc. of the 3rd. Int’l WS on Automated Debugging–AADEBUG, pp. 155–170. U. Linköping Press (May 1997)
Comini, M., Levi, G., Meo, M.C., Vitiello, G.: Abstract diagnosis. Journal of Logic Programming 39(1-3), 43–93 (1999)
Comini, M., Levi, G., Vitiello, G.: Declarative diagnosis revisited. In: ILPS 1995, Portland, Oregon, pp. 275–287. MIT Press, Cambridge (1995)
Cousot, P.: Automatic Verification by Abstract Interpretation. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 20–24. Springer, Heidelberg (2002)
Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of POPL 1977, pp. 238–252. ACM Press (1977)
Galassi, M., Davies, J., Theiler, J., Gough, B., Jungman, G., Alken, P., Booth, M., Rossi, F.: GNU Scientific Library Reference Manual. Network Theory Ltd. (2009), http://www.gnu.org/software/gsl/
Hermenegildo, M., Puebla, G., Bueno, F.: Using Global Analysis, Partial Specifications, and an Extensible Assertion Language for Program Validation and Debugging. In: The Logic Programming Paradigm: a 25–Year Perspective, pp. 161–192. Springer (1999)
Hermenegildo, M., Puebla, G., Bueno, F., López García, P.: Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor). Science of Comp. Progr. 58(1-2) (2005)
Lichtenstein, Y., Shapiro, E.Y.: Abstract algorithmic debugging. In: Kowalski, R.A., Bowen, K.A. (eds.) Fifth International Conference and Symposium on Logic Programming, Seattle, Washington, pp. 512–531. MIT (August 1988)
López-García, P., Darmawan, L., Bueno, F.: A Framework for Verification and Debugging of Resource Usage Properties. In: Technical Communications of ICLP. LIPIcs, vol. 7, pp. 104–113. Schloss Dagstuhl (July 2010)
López-García, P., Darmawan, L., Bueno, F., Hermenegildo, M.: Towards Resource Usage Function Verification based on Input Data Size Intervals. Technical Report CLIP4/2011.0, UPM (2011), http://cliplab.org/papers/resource-verif-11-tr.pdf
Méndez-Lojo, M., Navas, J., Hermenegildo, M.V.: A Flexible (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, pp. 154–168. Springer, Heidelberg (2008)
Mera, E., López-García, P., Hermenegildo, M.: Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 281–295. Springer, Heidelberg (2009)
Muthukumar, K., Hermenegildo, M.: Compile-time Derivation of Variable Dependency Using Abstract Interpretation. JLP 13(2/3), 315–347 (1992)
Navas, J., Méndez-Lojo, M., Hermenegildo, M.: User-Definable Resource Usage Bounds Analysis for Java Bytecode. In: BYTECODE 2009. ENTCS, vol. 253, pp. 6–86. Elsevier (March 2009)
Navas, J., Mera, E., López-García, P., Hermenegildo, M.: User-Definable Resource Bounds Analysis for Logic Programs. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 348–363. Springer, Heidelberg (2007)
Puebla, G., Bueno, F., Hermenegildo, M.: An Assertion Language for Constraint Logic Programs. In: Deransart, P., Małuszyński, J. (eds.) DiSCiPl 1999. LNCS, vol. 1870, pp. 23–61. Springer, Heidelberg (2000)
Puebla, G., Bueno, F., Hermenegildo, M.: Combined Static and Dynamic Assertion-Based Debugging of Constraint Logic Programs. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 273–292. Springer, Heidelberg (2000)
Vaucheret, C., Bueno, F.: More Precise yet Efficient Type Inference for Logic Programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 102–116. Springer, Heidelberg (2002)
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
Lopez-Garcia, P., Darmawan, L., Bueno, F., Hermenegildo, M. (2012). Interval-Based Resource Usage Verification: Formalization and Prototype. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2011. Lecture Notes in Computer Science, vol 7177. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32495-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-32495-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32494-9
Online ISBN: 978-3-642-32495-6
eBook Packages: Computer ScienceComputer Science (R0)