L’objectif de cette UF est d’introduire les grands principes de la sûreté de fonctionnement (SDF) : les concepts de base et les méthodes et techniques permettant de l’obtenir.
Un premier cours donne une introduction générale de la SDF en précisant la terminologie, les attributs, les moyens, etc.
Des cours spécifiques permettent d’aller un peu plus loin en se focalisant sur deux aspects:
– la modélisation de systèmes temporisés avec une introduction aux formalismes des Réseaux de Petri temporels et des automates temporisés et aux techniques de vérification associées ;
– la vérification de modèles qui permet de s’assurer de la satisfaction des propriétés à vérifier. Elle nécessite un modèle opérationnel du comportement, un modèle des propriétés à satisfaire (exprimées en logiques temporelles) et des algorithmes de contrôle de modèles (model-checking) pour s’assurer de la correction du modèle
