Monitoring for a decidable fragment of MTLD
Ref: CISTER-TR-151009 Publication Date: 22 to 25, Sep, 2015
Monitoring for a decidable fragment of MTLD
Ref: CISTER-TR-151009 Publication Date: 22 to 25, Sep, 2015Abstract:
Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTLD, we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.
André Pedro
David Pereira
Luis Miguel Pinho
Jorge Sousa PintoDocument:
View
DownloadThe 15th International Conference on Runtime Verification (RV'15).
Vienna, Austria.
Record Date: 14, Oct, 2015
Short links for this page: www.cister-labs.pt/docs/cister_tr_151009 www.cister-labs.pt/docs/1155