A Functional Synchronous Language with Integer Clocks

A Functional Synchronous Language with Integer Clocks

Mardi 31/03/2015, LUG, salle du bas, 10h30 (to be confirmed)

Adrien Guatto ENS Ulm/Parkas

Résumé:

Synchronous languages in the vein of Lustre are first-order functional languages dedicated to stream processing. Lustre compilers use a type-like static analysis, the clock calculus_, to reject programs that cannot be implemented as finite state machines. The broad idea is to assign to each element of a stream a logical computation date in a global, discrete time scale. When this analysis succeeds, the types obtained guide the code generation phase of the compiler, which produces transition functions. In practice, these functions consists in simple, bounded memory C code featuring only assignments and conditional statements.

This talk presents a variation on Lustre and its compilation. Our proposal is twofold. First, we add a new construct that creates a local time scale whose internal steps are invisible from the outside. Second, we change the clock calculus to allow several elements of a stream to be computed during the same time step. I will discuss the resulting type system, and how the code generation scheme of Lustre, once adapted to this new setting, generates code featuring nested loops.

Augmentation de la robustesse de systèmes et logiciels embarqués

Augmentation de la robustesse de systèmes et logiciels embarqués

18 avril 2014 LIP, salle B2, 14h30

Salma Bergaoui

Résumé:

Les systèmes critiques, parmi lesquels les systèmes embarqués construits autour d’un microprocesseur mono-cœur exécutant un logiciel d’application, ne sont pas à l’abri d’interférences naturelles ou malveillantes qui peuvent provoquer des fautes transitoires. Ces
travaux portent sur des protections qui peuvent être implantées pour détecter les effets de telles fautes transitoires sans faire d’hypothèses sur la multiplicité des erreurs générées.
Tout d’abord, une nouvelle méthode de vérification de flot de contrôle est proposée. Elle permet de vérifier, sans modifier le système initial, que les instructions du programme d’application sont lues sans erreur et dans le bon ordre. Les erreurs sur les données sont également prises en compte par une extension de la vérification de flot de contrôle. La méthode proposée offre un bon compromis entre les différents surcoûts, le temps de latence de détection et la couverture des erreurs. Les surcoûts peuvent aussi être ajustés aux besoins de l’application. La méthode est mise en œuvre sur un prototype, construit autour d’un microprocesseur Sparc v8.

Les fonctions d’analyse de criticité développées dans le cadre de la méthodologie proposée sont également utilisées pour évaluer l’impact des options de compilation sur la robustesse intrinsèque du logiciel d’application. Et enfin, une technique d’augmentation de la robustesse des systèmes d’exploitation par recouvrement au niveau processus a été conçue. Elle se base sur l’encapsulation des tâches dans des transactions, avec l’API RTSM, pour la récupération d’un état cohérent en cas de problème logiciel ou matériel.