La logique temporelle des signaux (STL) est un formalisme permettant d'exprimer des propriétés à horizon borné sur des systèmes critiques autonomes. La logique STL permet d'exprimer des propriétés sur des signaux à valeurs réelles et associe un intervalle borné non singleton à chaque opérateur temporel. Dans le cas des systèmes autonomes critiques, il peut être nécessaire de vérifier la validité d'une propriété STL en temps réel. À cette fin, nous proposons un encodage rigoureux des formules STL à temps discret sous la forme d’observateurs synchrones.
Dans un premier temps nous nous intéressons au cas particulier des propriétés temporelles non imbriquées. Nous fournissons une formalisation théorique des opérateurs. Nous en proposons par la suite une implémentation en Lustre accompagnée d’exemples d’utilisation.
Puis, en nous appuyant sur ces opérateurs ainsi modélisés, nous traitons le cas des opérateurs imbriqués. Nous apportons une proposition de stratégie d’implémentation et nous tentons de la mettre en oeuvre en Lustre. Nous montrons les possibilités et les limites de notre méthode.
Enfin, nous nous interrogeons sur les capacités de nos travaux pour détecter de potentielles cyberattaques sur des systèmes embarqués basés sur l’intelligence artificielle. Nous prenons comme exemple de cas d’application les travaux AITIVE concernant la pose sur Mars d’un rover à partir de différentes méthodes basées sur l’utilisation de réseaux de neurones. |
Signal-Time Logic (STL) is a formalism for expressing properties with bounded horizons on autonomous critical systems. STL allows for the expression of properties on real-valued signals and associates a bounded, non-singleton interval with each temporal operator. In the case of autonomous critical systems, it may be necessary to verify the validity of an STL property in real time. To this end, we propose a rigorous encoding of discrete-time STL formulas in the form of synchronous observers.
First, we focus on the specific case of non-nested temporal properties. We provide a theoretical formalization of the operators. We then propose an implementation in Lustre, accompanied by usage examples.
Then, building on these provided operators, we address the case of nested operators. We propose an implementation strategy and attempt to implement it in Lustre. We demonstrate the possibilities and limitations of our method through several examples.
Finally, we examine the potential of our work to detect potential cyberattacks on AI-based embedded systems. We use the AITIVE project—which involves landing a rover on Mars using various methods based on neural networks—as an example of a practical application. |