PUMA
Istituto di Informatica e Telematica     
Matteucci I., Costa G. Elective Temporal Logic. In: QoSA-ISARCS '11 (Boulder, Colorado, USA, 20-24 June 2011). Proceedings, pp. 143 - 152. ACM, 2011.
 
 
Abstract
(English)
In this paper we present a novel formalism for de ning properties over linear execution traces, namely elective temporal logic (ETL). Di erently from several other temporal logics, ETL is not dedicated to a speci c time model, e.g. discrete time or real time. Hence, properties can be applied to each temporal context with no changes to the speci ed formulas. Moreover, the ETL denotational semantics is given through elective functions. In this way we map formulas into the characteristic functions of a set of accepted traces, i.e. the valid executions. A further contribution of this work is an application of ETL to runtime monitoring. As a matter of fact, using a security monitor driven by an ETL formula, we can ignore irrelevant security actions performed by the guarded program reducing the monitor workload.
DOI: 10.1145/2000259.2000283
Subject Program Verification
Application Monitoring
Formal language
Logics and Meanings of Programs (F.3.1)
D.4.6 Security and Protection (K.6.5)
D.3.3 Language Constructs and Features


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional