Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
Interval-Based Resource Usage Verification: Formalization and Prototype
Áreas de investigación
  • Ingenierías
In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to en- sure 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 com- bined 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.
Nombre congreso
Foundational and Practical Aspects of Resource Analysis
Tipo de participación
Lugar del congreso
Fecha inicio congreso
Fecha fin congreso
Desde la página
Hasta la página
Título de las actas
Foundational and Practical Aspects of Resource Analysis. Second Iternational Workshop FOPARA 2011, Revised Selected Papers
Esta actividad pertenece a memorias de investigación
  • Autor: Pedro Lopez Garcia (Instituto IMDEA Software)
  • Autor: Luthfi Darmawan (Instituto IMDEA Software)
  • Autor: Francisco Bueno Carrillo (UPM)
  • Autor: Manuel de Hermenegildo Salinas (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Inteligencia Artificial
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)