Login

Real-time MTL with durations as SMT with applications to schedulability analysis
Ref: CISTER-TR-200703       Publication Date: 11 to 13, Dec, 2020

Real-time MTL with durations as SMT with applications to schedulability analysis

Ref: CISTER-TR-200703       Publication Date: 11 to 13, Dec, 2020

Abstract:
This paper introduces a synthesis procedure for the satisfiability problem of RMTL-R formulas as SAT solving modulo theories. RMTL-R is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL-R with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL-R formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach.

Authors:
André Pedro
,
Martin Leucker
,
David Pereira
,
Jorge Sousa Pinto


Events:

TASE 2020
11, Dec, 2020 >> 13, Dec, 2020
14th International Symposium on Theoretical Aspects of Software Engineering
Hangzhou, China


14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020).
Hangzhou, China.



Record Date: 16, Jul, 2020