Prise en Compte de Règles de Sécurité Temporelles dans une Spécification TEFSM d'un Système

Overview & Synopsis

Dans cet article, nous proposons une approche formelle de modélisation conjointe des aspects fonc- tionnels et sécuritaires d'un système. Cette approche consiste à enrichir la spécification fonctionnelle d'un système, exprimée à l'aide d'une TEFSM (Timed Extended Finite State Machine), par des règles de sécurité temporelles modélisées en Nomad. Nomad est un langage formel bien adapté pour l'expression de propriétés de sécurité telles que les permissions, les interdictions et les obligations. Le modèle fonctionnel sécurisé global ainsi obtenu peut être utilisé à plusieurs fins tels que la génération de code, le test du système, la vérification du modèle(model checking), etc. Afin de s'assurer de la faisabilité de notre approche, celle-ci a été expérimentée à plusieurs applications distribuées.