Calcul de propriétés temps réel de bout-en-bout dans un programme synchrone multi-périodique

National audienceLes systèmes temps réel critiques doivent souvent répondre à des exigences temporelles de bout en bout, exprimées au niveau modèle, mais qui ne sont pour la plupart vérifiées qu’au niveau de l’implantation. Cet article se focalise sur trois exigences : la latence d’une entrée vers une sortie, la fraîcheur d’une sortie relativement à une entrée, et enfin la réactivité du système vis-à-vis d’une entrée. Nous montrons que, en utilisant une approche synchrone enrichie par des horloges temps réel pour la modélisation du système, il est possible de calculer ces propriétés automatiquement en faisant abstraction des choix d’implantation