Logiques temporelles pour l'apprentissage et la détection de comportements anormaux

La complexité croissante des systèmes modernes nécessite des méthodes de détection d'anomalies automatisées pour détecter d'éventuels comportements anormaux déterminés par des malfonctionnements ou des attaques extérieures. Nous présentons des méthodes formelles pour inférer (via l'apprentissage supervisé) et détecter (via l'apprentissage non supervisé) des comportements anormaux. Nos procédures utilisent des données pour construire une formule de logique temporelle de signal (STL) qui décrit le comportement normal du système. Cette logique peut être utilisée pour formuler des propriétés telles que « Si le train freine à moins de 500 m de la plateforme à une vitesse de 50 km/h, il s'arrêtera en au moins 30 s et au maximum 50 s. » Notre procédure infère non seulement les paramètres physiques impliqués dans la formule (par exemple, 500 m dans l'exemple ci-dessus) mais aussi sa structure logique. La STL offre une représentation plus lisible par l'homme du comportement que les classificateurs représentés comme des surfaces dans des espaces de caractéristiques à haute dimension. La formule apprise nous permet de réaliser une détection précoce en utilisant des techniques de surveillance et une atténuation des anomalies en utilisant des techniques de synthèse formelle. Nous démontrons la puissance de nos méthodes avec des exemples de surveillance navale et d'un système de freinage de train.