# RAMONA

A realtime model-checker for analyzing systems of RAte MONotonic tAsks

# The RAte MONotonic tasks Analyzer

Ramona is a tool for analyzing real-time properties of systems of RAte MONotonic tAsks. Its main objective is to check the schedulabity of a set of periodic tasks using some hypothesis on the behavior; more specifically the use of fixed priority scheduling and a Logical Execution Time (LET) model.

The results of our analyses can also be used to compute timing information on the flow of messages across a sequence of (logically dependent) tasks; such as minimal traversal delays; worst case response time; or age delays for different services of a system.

The tool is based on a specialized version of the State Class Graph construction, the method used in the TINA (TIme petri Net Analyzer) toolbox. Like for TINA, this tool is maintained by the Verification of Time Critical Systems (VERTICS) group, which develops new verification methods and tools for checking properties of critical systems having strong temporal and timing requirements.

## Release 0.5.2 (a697a61, October 2019)

64 bits versions; other targets possible on request, see here.

ramona-linux   ramona for PCs under Linux: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, stripped

ramona.exe   ramona for PCs under Windows: PE32+ executable (console) x86-64 (stripped to external PDB), for MS Windows; only tested on Windows 10

ramona-darwin   ramona for Intel Macs under MacOS 10.10 and above: Mach-O 64-bit x86_64 executable

## Installation

Simply download the right executable for your OS and put it in a place where it can be found by your shell (this may include updating your PATH variables).

## Usage

Download some examples of task systems—e.g. files t1.task, t4.task, or errored.task (an example with a scheduling error)—and call ramona:

\$ ramona -v t1.task


For more information on ramona, you can have a look at the how-to page.

# News and Informations

### How-To use ramona

You can find a list of possible options for the tool using option -h. By default ramona uses option -W, that computes the (weak) state …