RAMONA

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

  Windows executable (.exe) Download for another OS

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.

Download

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 …
Oct 4, 2019

Tasks system

Ramona is a realtime model-checker that generates an abstraction of the state-space of systems of preemptive tasks, with fixed priority …
Oct 5, 2019

Contact

The easiest way to contact us is through the TINA mailing list. Subscribe or update your list subscription(s) at:

Send submissions to tina-users@laas.fr

For bug reports or additional information specifically about Ramona, please contact: