RESCUE
REliable and Safe Code execUtion for Embedded systems
| PTDC/EIA/65862/2006 38 months (Jan 2008 to Feb 2011) | |
| Summary: | This proposal looks at an important requirement in safety critical systems -- that of supporting verifiability of software components. The proposers focus on embedded systems, thereby making the approach more manageable. The also provides a more significant challenge, in that the device in which the verification is being undetaken is resource constrained. The approach is clearly applicable to a variety of different contexts and scenarios. The use of certificates in Proof Carrying Codes provides a useful basis to support such verifiability provides a useful first step for the research being proposed here. The authors advocate the use of: (i) Type-based; (ii) Language-based; and (iii) Logic-based security enforcement mechanisms. A good and interesting proposal, that could impact the use of safety critical applications in embedded and mobile devices. |
| Funding: | Global: 161KEUR, CISTER: 80KEUR |
| Sponsors: |     |
| Partners: | |
| Contact Person at CISTER: | Luis Miguel Pinho |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Journal Papers
Deciding Kleene Algebra Terms Equivalence in Coq CISTER-TR-141205
David Pereira, Nelma Moreira, Simão Patrício Melo de SousaJournal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier. May 2015, Volume 84, Issue 3, pp 377-401.
David Pereira, Nelma Moreira, Simão Patrício Melo de SousaJournal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier. May 2015, Volume 84, Issue 3, pp 377-401.
On the Use of Code Mobility Mechanisms in Real-Time Systems HURRAY-TR-111205J
Luis Lino Ferreira, Luis Miguel NogueiraACM SIGBED Review - Special Issue on the 10th International Workshop on Real-time Networks (RTN 2011) (ACM SIGBED Rev), ACM New York. Dec 2011, Volume 8, Issue 4, pp 16-21. U.S.A..
Luis Lino Ferreira, Luis Miguel NogueiraACM SIGBED Review - Special Issue on the 10th International Workshop on Real-time Networks (RTN 2011) (ACM SIGBED Rev), ACM New York. Dec 2011, Volume 8, Issue 4, pp 16-21. U.S.A..
PDFConference or Workshop Papers/Talks
On the Use of Code Mobility Mechanisms in Real-Time Systems HURRAY-TR-111205
Luis Lino Ferreira, Luis Miguel Nogueirathe 10th International Workshop on Real-Time Networks (RTN 2011). 5, Jul, 2011. Porto, Portugal.
Luis Lino Ferreira, Luis Miguel Nogueirathe 10th International Workshop on Real-Time Networks (RTN 2011). 5, Jul, 2011. Porto, Portugal.
Managing contention of software transactional memory in real-time systems HURRAY-TR-101102
António Barros, Luis Miguel Pinho31st IEEE Real-Time Systems Symposium (RTSS 2010). 30, Nov to 3, Dec, 2010, Work-In-Progress Session. San Diego, U.S.A..
António Barros, Luis Miguel Pinho31st IEEE Real-Time Systems Symposium (RTSS 2010). 30, Nov to 3, Dec, 2010, Work-In-Progress Session. San Diego, U.S.A..
A Framework for QoS-Aware Service-based Mobile Systems HURRAY-TR-101002
Joel Gonçalves, Luis Lino FerreiraII Simpósio de Informática (Inforum 2010). 9 to 10, Oct, 2010, 711, pp 714. Braga, Portugal.
Joel Gonçalves, Luis Lino FerreiraII Simpósio de Informática (Inforum 2010). 9 to 10, Oct, 2010, 711, pp 714. Braga, Portugal.