This page gathers examples illustrating usage of AltaRica language in modelling process and also the use of ARC tool to analyze these models.

Design of a lift

In this example the model of a lift system is described. The system must fulfil some safety or liveness properties. The documentation shows how the model is fixed to satisfy requirements.

Download the PDF file.

Proof of Peterson’s algorithm for Mutual Exclusion

This example studies the well-known algorithm proposed by G. L. Peterson to solve mutual exclusion of concurrent processes.

Download the PDF file.

Controller synthesis: Winning strategy in the Nim game

Here we model a two-player game and show how one can compute a strategy to ensure the win of the game.
Such winning strategies are the basics for the synthesis of controllers that guaranteed critical requirements.

Download the PDF file.