​Que ce soit dans le domaine aéronautique ou automobile, les architectures matérielles ainsi que les algorithmes de contrôle commande utilisés ne cessent de se complexifier, et l'écart entre les performances en moyenne et en pire cas ne cesse de se creuser. Or dans les systèmes embarqués, il est nécessaire de faire cohabiter des fonctions avec différents niveaux de criticité et d'exigence sur un même calculateur. Tandis que ces derniers doivent réagir à des événements en des temps bornés et maîtrisés, les calculateurs sont dimensionnés en considérant un temps de réponse "pire cas", largement surestimé pour bénéficier d'une marge afin de garantir la sûreté.

Evaluer plus finement les propriétés temporelles des calculateurs (anomalies temporelles, contentions mémoires…) permettrait de mieux tirer parti de la puissance de calcul disponible, et de réduire la marge de manœuvre nécessaire sans faire de concession sur la sûreté. Dans cet objectif, le List s'est rapproché de l'université de Berkeley pour bénéficier des compétences de ses chercheurs sur les architectures prédictibles et leur visibilité scientifique. Une équipe du List a démarré le développement de Leaf, un outil utilisant judicieusement les méthodes formelles pour reproduire, analyser et vérifier avec précision le comportement de programmes sur un calculateur donné.

A terme, Leaf devrait permettre de fournir des informations visant à aider les industriels à concevoir et à dimensionner leurs systèmes, et ainsi augmenter la confiance dans leurs comportements.