REliable and Safe Code execUtion for Embedded systems


Rescue Team




Jan.2008 Kick-off meeting (25/01/2008)

Currently active RESCUE-related research opportunities (at the undergraduate and post-graduate levels) are announced here.

PhD Opportunities

Master Opportunities

Automated Model checking in ADA/Spark Topic: Model checking for real-time systems allows to ensure that a system (the model) verifies the required temporal properties. To be useful, the model must be automatically inferred/translated from the system source code. In the scope of the RESCUE project, it was developed a translation from HTL (a coordination language for concurrent real-time systems) to timed-automata networks of the UPPAAL system. Based on this experience, it is intended to extend/adapt this framework To the ADA/Spark language. The work will include the construction of a translator able to abstract ADA tasks coordination and provide a model for which temporal properties can be analysed.

Call closes on November 12, 2009. To apply see

For more information contact or

Research Training Opportunities

r7 - 15 Oct 2009 - 23:04:32 - NelmaMoreira?
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM