Interval-based resource usage verification: Formalization and prototype

López García, Pedro; Darmawan, Luthfi; Bueno Carrillo, Francisco y Hermenegildo, Manuel V. (2011). Interval-based resource usage verification: Formalization and prototype. En: "Second International Workshop, FOPARA 2011", May 19, 2011, Madrid, Spain. ISBN 9783642324949.


Título: Interval-based resource usage verification: Formalization and prototype
  • López García, Pedro
  • Darmawan, Luthfi
  • Bueno Carrillo, Francisco
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: Second International Workshop, FOPARA 2011
Fechas del Evento: May 19, 2011
Lugar del Evento: Madrid, Spain
Título del Libro: Foundational and Practical Aspects of Resource Analysis
Fecha: Mayo 2011
ISBN: 9783642324949
Palabras Clave Informales: Cost analysis, Resource usage analysis, Resource usage verification, Program verification and debugging, Análisis de coste, Análisis del uso de los recursos, Depuración y verificación de programas, Verificacion del uso de los recursos.
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa


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 resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. 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 which 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 full 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.

Más información

ID de Registro: 14579
Identificador DC:
Identificador OAI:
URL Oficial:
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 02 Mar 2013 06:56
Ultima Modificación: 21 Abr 2016 14:18
  • GEO_UP4
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • InvestigaM
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM