Página 1 dos resultados de 3 itens digitais encontrados em 0.003 segundos

Timing analysis: from predictions to certificates

Gaspar, Nuno Miguel Pires
Fonte: Universidade da Beira Interior Publicador: Universidade da Beira Interior
Tipo: Dissertação de Mestrado
Publicado em //2010 ENG
Relevância na Pesquisa
35.88%
In real-time systems timing properties must be satisfied in order to guarantee that deadlines will be met. In this context, the calculation of theworst-case execution time(WCET) is of paramount importance for schedulability analysis. However, this problem can be difficult if the underlying architecture possesses features like caches and pipelines. This thesis presents all the necessary steps for the safe and preciseWCET calculation. We focus ourselves in the use of static analysis-based methods, and in the ARMarchitecture as target platform. Moreover, in order to ensure the correctness of our calculation to a program consumer, we produce a certificate (or proof ) whose validity entails compliance with the calculated WCET. This evidence permits to locally validate the calculated WCET, avoiding the need of a blind confidence on the producer.

Some Issues on Incremental Abstraction-Carrying Code

Albert, Elvira; Arenas, Puri; Puebla, German
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 17/01/2007
Relevância na Pesquisa
66.47%
Abstraction-Carrying Code (ACC) has recently been proposed as a framework for proof-carrying code (PCC) in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction thus plays the role of safety certificate and its generation (and validation) is carried out automatically by a fixed-point analyzer. Existing approaches for PCC are developed under the assumption that the consumer reads and validates the entire program w.r.t. the full certificate at once, in a non incremental way. In this abstract, we overview the main issues on incremental ACC. In particular, in the context of logic programming, we discuss both the generation of incremental certificates and the design of an incremental checking algorithm for untrusted updates of a (trusted) program, i.e., when a producer provides a modified version of a previously validated program. By update, we refer to any arbitrary change on a program, i.e., the extension of the program with new predicates, the deletion of existing predicates and the replacement of existing predicates by new versions for them. We also discuss how each kind of update affects the incremental extension in terms of accuracy and correctness.; Comment: Paper presented at the 16th Workshop on Logic-based Methods in Programming Environments (WLPE2006)

Certificate size reduction in Abstraction-Carrying Code

Albert, Elvira; Arenas, Puri; Puebla, Germán; Hermenegildo, Manuel
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 13/10/2010
Relevância na Pesquisa
56.47%
Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. Interestingly, the fact that the reduced certificate omits (parts of) the abstraction has implications in the design of the checker. We provide the sufficient conditions which allow us to ensure that 1) if the checker succeeds in validating the certificate...