ALPROSE

Ce projet vise à définir une architecture informatique à déclenchement par le temps qui permette de vérifier formellement des propriétés importantes d’un système en particulier la garantie du maintien des échéances temporelles. Les systèmes ciblés sont des systèmes perceptifs embarqués à bord de petits drones. Ces systèmes impliquent des composants très variés, tout en imposant des contraintes extrêmement fortes en embarquement, sûreté et fonctionnement temps réel. L’architecture développée doit supporter l'ensemble des composants de ces systèmes perceptifs. Le projet vise également la définition d’un langage formel permettant de décrire les spécifications logiques et temporelles imparties aux différents applicatifs embarqués. Il vise à vérifier par calcul si l’exécution des applicatifs peut se conformer aux spécifications. Les applicatifs sont alors exécutables et le contrôle de l'exécution est produit par les compilateurs.