A carregar...
Publicação
Monitoring for a decidable fragment of MTLD
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 356.9 KB | Adobe PDF |
Orientador(es)
Resumo(s)
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.
Descrição
The 15th International Conference on Runtime Verification (RV'15). 22-25 September. Vienna, Austria.