vendredi 13 décembre 2024

Pavlo Tokariev soutiendra sa thèse de doctorat le vendredi 13 Décembre 2024 à 14h00 au Centre Inria d'Université Côte d'Azur dans la salle Euler Bleu.

La thèse intitulée « Langage modulaire pour la spécification de contraintes d’horloges logiques et temps-réel » a été réalisée dans le pôle Comred sous la direction de Frédéric Mallet.

La présentation sera en anglais.

 

Résumé :
Les systèmes en temps réel critiques (réactifs) sont des systèmes qui contrôlent des processus complexes et dont la faute n'est pas acceptable en raison des graves conséquences pour le système, l'infrastructure et les humains. Dans ces systèmes, le moment de la réaction est aussi critique que l'exécution de la bonne action. Dans ce travail, nous nous concentrons sur le premier. Pour ce faire, nous utilisons une abstraction du temps, connue sous le nom de temps logique. Il abstrait totalement les instants auxquels les événements se produisent par leur position relative. Le langage sur lequel nous basons notre travail, Clock Constraint Specification Language (CCSL), est purement basé sur la notion d'horloge logique et conçu pour décrire les exigences temporelles des systèmes. L'application du langage nous a permis de constater que l'approche purement logique n'est pas toujours adéquate. Le langage de spécification doit permettre de décrire des relations temps réel. Leur simulation purement avec des horloges logiques échoue en général en raison de la différence de complexité. Ceci nous incite à trouver des moyens d'abstraire ou de résoudre en utilisant des méthodes moins exactes. Ainsi, dans ce travail, nous proposons une série d'extensions du langage original, orthogonales mais se complétant. Celles-ci couvrent les contraintes en temps réel et les contraintes auxiliaires pour augmenter l'expressivité, la paramétrisation des contraintes et le cadre modulaire avec une fonction similaire au raffinement. Nous les définissons formellement et motivons leur conception à l'aide de plusieurs cas d'utilisation. Nous rapportons nos expériences avec l'interprétation abstraite dans l'analyse des spécifications et proposons plusieurs modifications pour la rendre plus précise. Enfin, nous introduisons notre propre solveur ad hoc utilisant une représentation polyédrique sur un fragment du langage.