Open Research Scholarship -Project RESCUE
A Research Grant position is available in the framework of project Rescue:: Reliable and Safe Code Execution for Embedded Systems, which aims at providing innovative, efficient and expressive mechanisms for the secure implementation and execution of code, with an emphasis on problems posed by embedded systems. The work will focus on the use of model checking based on timed-automata for ensure temporal properties of real-time systems.
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.
Grant duration: 6 months
Call closing date: 12/11/2009
For further information, please contact Nelma Moreira at firstname.lastname@example.org