RESTK

Performance Tools BSC Group: Computer Sciences Software

RESTK is an implementation of the algorithm to upper-bound extremely high quantiles using Markov's inequality to the power-of-k for probabilistic WCET.

Further details can be found in this publication: https://drops.dagstuhl.de/opus/volltexte/2022/16337/

Software Author: 

Sergi Vilardell

Contact:

Sergi Vilardell (sergi.vilardell@bsc.es)

License: 

GPL License (Version 3.0)

Primary tabs

In real-time embedded systems the timing analysis is a crucial part of the Verification and Validation process. In particular, the analysis of the Worst-Case Execution Time (WCET), is an on-going problem in the real-time community. For safety reasons, the difficulty lies in being able to upper-bound the WCET, which is arguably very hard to actually measure. In RESTK, we provide with a solution for upper-bounding the WCET. Markov's inequality is a probabilistic tool that allows to compute upper-bounds for the probability of exceeding a certain value. In its simplest form Markov's inequality is very pessimistic in its upper-bounding. We provide with a much tighter solution for upper-bounding extremely high quantiles by using Markov's inequality to the power-of-k in the Restricted K (RESTK) algorithm in order to ensure that the estimations always upper-bound the true WCET. The implementation allows to input an execution time profile and compute an upper-bound for the desired high-quantiles. The software is written in R, and the last version can be founs in the Comprehensive R Archive Network (CRAN) repository.