response-time-analysis 0.1.1

An implementation of the response-time analyses (RTAs) verified by the PROSA project

pyRTA — Response-Time Analysis in Python

The Python response-time-analysis package (pyRTA) implements the response-time analyses (RTAs) formally verified in the PROSA project.

It provides Python models for real-time task parameters (arrivals, execution, deadlines, priorities) and ready-to-use analyses for fixed-priority (FP), earliest-deadline-first (EDF), and FIFO schedulers, including support for non-preemptive segments and restricted-supply models.

Features and Design

• Arrival models: periodic, periodic with jitter, sporadic, and arbitrary arrival curves, expressed either as minimum-separation vectors (i.e., "delta-min vectors") or as a list of steps and a prefix horizon.
• Preemption models: fully preemptive, fully non-preemptive, floating non-preemptive segments, and segmented limited-preemptive.
• Supply models: ideal processor and rate-delay model.
• Analyses: FP, EDF, and FIFO response-time analysis.
• Discrete time: pyRTA uses a discrete time model (model.Duration is an alias of int). Task parameters should be specified using an appropriate resolution (e.g., in nanoseconds or processor cycles).

Installation

pyRTA is a pure Python package that can be installed from PyPI.

With the uv package manager (recommended):

uv add response-time-analysis

With pip:

pip install response-time-analysis

Quickstart

Compute a response-time bound for a task under fixed-priority (FP), earliest-deadline-first (EDF), and first-in-first-out (FIFO) scheduling on an ideal uniprocessor:

from response_time_analysis import edf, fifo, fp
from response_time_analysis.model import (
    WCET,
    Deadline,
    FullyPreemptive,
    IdealProcessor,
    Periodic,
    Priority,
    Task,
    taskset,
)

# Two periodic tasks with implicit deadlines; higher priority has the larger numeric value as in Linux
tsk1 = Task(Periodic(period=5), FullyPreemptive(WCET(1)), Deadline(5), Priority(2))
tsk2 = Task(Periodic(period=10), FullyPreemptive(WCET(6)), Deadline(9), Priority(1))

supply = IdealProcessor()

tasks = taskset(tsk1, tsk2)

# RTA assuming uniprocessor fixed-priority scheduling.
solution = fp.rta(tasks, tsk2, supply)
assert solution.bound_found()
assert solution.response_time_bound == 8

# RTA assuming uniprocessor earliest-deadline first scheduling.
solution = edf.rta(tasks, tsk2, supply)
assert solution.bound_found()
assert solution.response_time_bound == 7

# RTA assuming uniprocessor FIFO scheduling.
solution = fifo.rta(tasks, supply)
assert solution.bound_found()
assert solution.response_time_bound == 7

# Use the horizon parameter to prevent the RTA from diverging.
tsk3 = Task(Periodic(period=9), FullyPreemptive(WCET(3)), Deadline(20), Priority(3))
overload = taskset(tsk1, tsk2, tsk3)
solution = fifo.rta(overload, supply, horizon=1000)
assert solution.bound_found() is False
assert solution.search_space is None
assert solution.response_time_bound is None

See the test cases in tests/test_usage_examples.py for further examples.

Development

• Run tests with uv run pytest
• Type-check with uvx basedpyright
• Lint and format with uvx ruff check --fix

Disclaimer

While PROSA verifies the underlying RTA theory, the implementations in pyRTA are not verified themselves — this is just a regular Python library.

However, pyRTA serves as the underlying RTA of the POET foundational response-time analysis tool, which formally certifies the outputs of unverified analyses to formally prove that the particular analysis results are correct (i.e., it verifies the output of each run, rather than the full implementation). Please refer to the POET paper for a more in-depth explanation.

Contributions, Feedback, Questions

Please use the project's issue tracker or contact Björn Brandenburg.

A Github mirror is available and accepts pull requests.

Attribution

When using the pyRTA library in academic work, please cite the paper underlying the verified RTAs implemented in this library:

• Sergey Bozhko and Björn Brandenburg, “Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle”, Proceedings of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020), pp. 22:1–22:24, July 2020. DOI: 10.4230/LIPIcs.ECRTS.2020.22

@inproceedings{BB:20,
  author       = {Sergey Bozhko and
                  Bj{\"{o}}rn B. Brandenburg},
  title        = {Abstract Response-Time Analysis: {A} Formal Foundation for the Busy-Window
                  Principle},
  booktitle    = {Proceedings of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)},
  pages        = {22:1--22:24},
  year         = {2020}
}