SMT-based Schedulability Analysis using RMTL-∫
Ref: CISTER-TR-161101 Publication Date: 29, Nov to 2, Dec, 2016
SMT-based Schedulability Analysis using RMTL-∫
Ref: CISTER-TR-161101 Publication Date: 29, Nov to 2, Dec, 2016Abstract:
Several methods have been proposed for performing
schedulability analysis for both uni-processor and multi-processor
real-time systems. Very few of these works use the power of
formal logic to write unambiguous specifications and to allow
the usage of theorem provers for building the proofs of interest
with greater correctness guarantees. In this paper we address
this challenge by: 1) defining a formal language that allows to
specify periodic resource models; 2) describe a transformational
approach to reasoning about timing properties of resource models
by transforming the latter specifications into a SMT problem.
André Pedro
David Pereira
Luis Miguel Pinho
Jorge Sousa PintoDocument:
View
DownloadIEEE Real-Time Systems Symposium (RTSS 2016), CRTS.
Porto, Portugal.
Record Date: 3, Nov, 2016
Short links for this page: www.cister-labs.pt/docs/cister_tr_161101 www.cister-labs.pt/docs/1244