Using informed best-first search algorithms Modere can find deadlocks in models which possibly have a wildly large state space, returning either the shortest or a relatively short counter-example.

In this project we present a Rebeca model of the production cell and compare it to different model implementations of the same specification.

We are working on the turn taking system of the RoboRadio Show  and modelling modelling the system using UPPAAL and Rebeca. We extracted the main modules that shall be modelled and the required properties.

The Rheo Knee is the world's first microprocessor swing and stance knee system to utilize the power of artificial intelligence. We study the embedded system and the controller software with UML and UPPAAL.

In RORA project we propose to extend Rebeca with real-time constraints and to propose a suitable temporal language to specify time dependent properties.