📢 Nous sommes heureux de vous informer qu’Andrei Samokish fera une présentation à JFLA 2023.
Il présentera une traduction des modèles arKItect en prouveur de théorème de Coq. Cela permet de spécifier et de démontrer formellement les propriétés des modèles de système arKItect avec un environnement formel de premier ordre. Nous nous concentrons ici sur l’analyse de la sécurité. Le choix de Coq était naturel car les systèmes sont des définitions inductives (les systèmes sont faits de systèmes), et arKItect gère les modèles de systèmes comme un ensemble d’arbres reflétant cette structure. Cela correspond bien aux types inductifs de Coq.
Bien sûr, de nombreuses questions se posent: qu’est-ce qu’un modèle de système complet et correct? Qu’est-ce qu’une analyse de la sûreté ou un dossier de sûreté complet et correct. L’autre enjeu est de rendre tout cela transparent pour l’utilisateur final qui est intéressé à bien faire les choses avec une interface simple et intuitive et non des choses linguistiques complexes.
📌 Mercredi 1 février 2023 📌
