ICE ROSE - Projects

Heuristic Guided Model Checking for Rebeca

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.

Read more

Production Cell: a benchmark Case Study

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

Read more

Modeling and verifying RoboRadio Show of CADIA

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.

Read more

Modeling and verifying bionic products of Össur

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.

Read more

RORA-Pilot

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

Read more