Full text
Preview |
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
López García, Pedro and Darmawan, Luthfi and Bueno Carrillo, Francisco and Hermenegildo, Manuel V. (2011). Interval-based resource usage verification: Formalization and prototype. In: "Second International Workshop, FOPARA 2011", May 19, 2011, Madrid, Spain. ISBN 9783642324949.
Title: | Interval-based resource usage verification: Formalization and prototype |
---|---|
Author/s: |
|
Item Type: | Presentation at Congress or Conference (Article) |
Event Title: | Second International Workshop, FOPARA 2011 |
Event Dates: | May 19, 2011 |
Event Location: | Madrid, Spain |
Title of Book: | Foundational and Practical Aspects of Resource Analysis |
Date: | May 2011 |
ISBN: | 9783642324949 |
Subjects: | |
Freetext Keywords: | 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. |
Faculty: | Facultad de Informática (UPM) |
Department: | Inteligencia Artificial |
Creative Commons Licenses: | Recognition - No derivative works - Non commercial |
Preview |
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
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.
Item ID: | 14579 |
---|---|
DC Identifier: | https://oa.upm.es/14579/ |
OAI Identifier: | oai:oa.upm.es:14579 |
Official URL: | http://link.springer.com/chapter/10.1007%2F978-3-6... |
Deposited by: | Biblioteca Facultad de Informatica |
Deposited on: | 02 Mar 2013 06:56 |
Last Modified: | 27 Feb 2023 11:39 |