Vérification d'applications temps-réel basées sur le paradigme de Logical Execution Time (LET)

National audienceLe design de logiciel de contrôle/commande embarqué dépend de contraintes temporelles strictes. Pour cela, des formalismes et des théories basés sur la notion de temps logique permettent d'abstraire les durées temps-réel qui ne sont pas toujours connues au niveau conception. Cet article propose une comparaison des formalismes synchrones et du paradigme Logical Execution Time (LET) dans le but d'adapter au langage industriel PsyC, qui est proche du LET, des méthodes de vérification issues des langages synchrones