AFSEC

Les journées du GDR GPL se tiendront du lundi 14 au vendredi 18 juin prochain, à distance. À cette occasion, une session AFSEC sera organisée le mercredi 16 juin de 13h30 à 15h30. Deux exposés sur la thématique des solveurs SMT seront donnés. Pour s’inscrire c’est ici : https://gdr-gpl-2021.sciencesconf.org/

On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets (par Nicolas Amat)

We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstraction. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used during the 2020 edition of the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.

SMT-Based Bounded Model Checking of Max-Plus Linear Systems (par Muhammad Syifa’ul Mufid)

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. MPL systems can be naturally modeled as infinite-state transition systems, and exhibit interesting structural properties (e.g. periodicity or steady-state), for which analysis methods have been recently proposed. In this talk, we tackle the open problem of specifying and analyzing user-defined temporal properties for MPL systems. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete-time events governed by an MPL system, and characterizes the problem of model checking TDLTL over MPL. We propose a family of specialized algorithms leveraging the periodic behaviour of an MPL system. We prove soundness and completeness, showing that the transient and cyclicity of the MPL system induce a completeness threshold for the verification problem. The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the computation of the bound, and on the unrolling of the transition relation. Our comprehensive experiments show that the proposed techniques can be applied to MPL systems of large dimensions and on general TDLTL formulae, with remarkable performance gains against a dedicated abstraction-based technique and a translation to the nuXmv symbolic model checker.

Journée du GT AFSEC du GDR GPL

Vérification formelle de systèmes distribués

Quand: Le 11 décembre 2019
Lieu: ENSEEIHT, Toulouse (salle F-501)
2 rue Charles Camichel, Toulouse
Métro ligne B station François Verdier ou ligne A station Jean Jaurès
L’inscription (gratuite) est nécessaire pour la bonne organisation de l’événement (envoi d’un email à julien.brunel@onera.fr ; objet : “Inscription AFSEC 11 décembre”) (cliquer sur le lien) – préciser : Nom et Affiliation.

Programme :

• 10h – 10h30 accueil, café
• 10h30 – 11h15 Stephan Merz, LORIA
  Formal Techniques for the Verification and Synthesis of Security Chains
• We describe work on the formal verification (using SMT solving and symbolic model checking) and on the synthesis of chains of networking functions intended to limit the ability of mobile applications to carry out attacks on servers and networking infrastructure. In order to generate a security chain dedicated to a particular application, represent its networking activity as a Markov chain, based on network flows captured on-device. Rules expressed as Horn clauses that take into account the structure of the Markov chain and thresholds provided by network operators classify the network activity according to different types of attacks and infer predicates representing network rules. Chains for individual applications are merged and then optimized for deployment in a given infrastructure. The security chains are expressed in Pyretic, a domain-specific language for programming software-defined networks and can be deployed in a cloud infrastructure. Preliminary experiments in a network simulator indicate that the proposed approach for synthesizing and deploying security chains appears feasible, although the precision of detecting attacks remains to be improved for some types of applications.
• 11h15 – 12h Philippe Queinnec, IRIT
  Tasks in Modular Proofs of Concurrent Algorithms
• Proving correctness of distributed or concurrent algorithms is a mind-challenging and complex process. Slight errors in the reasoning are difficult to find, calling for computer-checked proof systems. In order to build computer-checked proofs with usual tools, such as Coq or TLA+, having sequential specifications of all base objects that are used as building blocks in a given algorithm is a requisite to provide a modular proof built by composition. Alas, many concurrent objects do not have a sequential specification. This article describes a systematic method to transform any task, a specification method that captures concurrent one-shot distributed problems, into a sequential specification involving two calls, Set and Get. This transformation allows system designers to compose proofs, thus providing a framework for modular computer-checked proofs of algorithms designed using tasks and sequential objects as building blocks. The Moir & Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition.
• 12h – 14h déjeuner – buffet
• 14h – 14h45 Robin Pelle, LRI
  Mouvement Asynchrone, Continus vs. Discrets: une approche certifié pour les robots mobiles
• Oblivious Mobile Robots have been studied both in continuous Euclidean spaces, and discrete spaces (that is, graphs). However the obtained literature forms distinct sets of results for the two settings. In this paper, we explore the possibility of transforming results obtained in one model into results for the other one. Our approach focuses on certified results using the COQ proof assistant.
• 14h45 – 15h30 Julien Brunel, ONERA
  Vérification formelle du protocole distribué Chord
• Chord is a protocol that provides a scalable distributed hash table over an underlying peer-to-peer network. Since it combines data structures, asynchronous communications, concurrency, and fault tolerance, it features rich structural and temporal properties that make it an interesting target for formal specification and verification. Previous work has mainly focused on (semi-)automatic proofs of safety properties, instead of studying the full correctness of the protocol (a liveness property). We report here on an automated verification of the correctness property using our model checker Electrum, and on the first mechanized (and partly manual) proof of the same property.
• 15h30 – 16h15 Quentin Peyras, ONERA
  Un fragment expressif et décidable de la logique temporelle du premier-ordre FO-LTL
• First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems, and distributed systems in particular. However, FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To address this, a possible track is to constrain specifications to a decidable fragment of FOLTL, but known fragments are too restricted to be usable in practice. In this paper, we exhibit various fragments of increasing scope that provide a pertinent basis for abstract specification of infinite-state systems. We show that these fragments enjoy the Bounded Domain Property (any satisfiable FOLTL formula has a model with a finite, bounded FO domain), which provides a basis for complete, automated verification by reduction to LTL satisfiability. Finally, we present a toy distributed system illustrating the applicability and limitations of our results.

Une journée de travail conjointe entre le GT AFSEC et le GT VS-CPS aura lieu le 16 novembre prochain à Nantes, durant JAMACS.

Le programme de cette journée est le suivant
Vendredi 16 novembre, 10h-12h

• Ocan Sankur (IRISA), Admissible Strategies in Quantitative Games
• Simon Rohou (ENSTA Bretagne), Verifying loops in robot trajectories under uncertainties
• Luc Jaulin (ENSTA Bretagne), Computing the no-lost zone for a mobile robot to find safe paths

Un Workshop AFSEC se tiendra le mecredi 13 juin (session 14h-15h30) lors des journées nationales du GDR GPL qui se dérouleront à Grenoble du 12 au 15 juin 2018.

Programme du Workshop AFSEC :

• Julien Brunel (ONERA)
  Modelling the structure and the behaviour of systems.
  

• Loïg Jezequel (Université de Nantes)
  Analyse paresseuse d’atteignabilité dans des réseaux d’automates temporisés..

• Marc Pouzet (Ecole Normale Supérieure)
  Un peu d’ordre supérieur dans Zélus.

Jeudi 17 novembre 2017
Session “Outils” Lors du 11e Colloque sur la Modélisation des Systèmes Réactifs MSR 2017.
Le programme est disponible : ici

Organisée par le GT SED et le GT AFSEC

• TABS : Outil logiciel d’ordonnancement de la production basée sur les automates temporisés
  Rémi Pannequin, Pascale Marangé, Alexis Aubry et Jean-François Petin
• SEDMA – un outil pour la Modélisation, l’Analyse et la génération automatique de programme pour les SEDs
  Romain Pichard, Michel Combacau, Alexandre Philippot, Ramla Saddem et Bernard Riera
• MinMaxGDJS – Calcul dans le semi-anneau MinMax[[gamma,delta]]
  Mehdi Lhommeau, Laurent Hardouin et Bertrand Cottenceau
• Identification de systèmes réactifs (logiques)
  Jérémie Saives, Gregory Faraut et Jean-Jacques Lesage
• IMITATOR: vérification de systèmes temps-réel concurrents en présence d’incertitude
  Étienne André
• Modeling and Simulation of Air France Baggage-Handling System with Colored Petri Nets
  Dina H. Hafilah, Andi Cakravastia, Younsse Lafdail et Naly Rakoto-Ravalontsalama
• MaxplusPy : librairie Python de calcul dans l’algèbre max-plus et de manipulation d’automates à multiplicités
  Sébastien Lahaye
• Evaluation de performances des automates temporisés avec gardes en utilisant l’algèbre (Max,+) – Application aux systèmes de commande en réseau
  Ferhat Tamssaouet et Saïd Amari
• Démonstrateur ASSecIN: ligne industrielle virtuelle permettant l’évaluation de passerelle intelligente
  Thomas Toublanc, Sébastien Guillet, Florent Frizon De Lamotte et Pascal Berruet
• DIAG-IPF: A Software Tool for Fault Diagnosis of Discrete Event Systems
  Abderraouf Boussif et Mohamed Ghazel

Session “Outils” Lors du 11e Colloque sur la Modélisation des Systèmes Réactifs (MSR 2017)

Lors du 11e Colloque sur la Modélisation des Systèmes Réactifs (MSR 2017), qui aura lieu à Marseille du 15 au 17 novembre 2017, les groupes AFSEC et SED organisent une session de démonstration de logiciels relatifs à la modélisation, l’analyse et la commande des systèmes réactifs et temps réel. Le but est de présenter à la communauté les outils logiciels que vous avez développés ou que vous utilisez dans le cadre de vos travaux de recherche.

Cette présentation se fera en deux temps :
– Une présentation rapide (5 minutes) en session plénière : genèse de l’outil, fonctionnalités, licences, copies d’écran…
РUn temps plus long de discussion autour des d̩monstrateurs, ou chacun pourra de mani̬re informelle ̩changer avec les pr̩sentateurs et tester les outils qui les int̩ressent particuli̬rement.

Nous lançons donc un appel à propositions à tous ceux qui souhaitent présenter un outil qu’ils jugent intéressant. Le but n’est pas de vendre ou de gagner un prix mais de partager votre expérience ou votre travail. N’hésitez donc pas à proposer de présenter votre propre création, même si elle n’est qu’en version alpha, ou au contraire un outil mature que vous maitrisez.

Les personnes intéressées sont invitées à soumettre avant le 17 septembre 2017 un résumé d’une ou deux pages en suivant la procédure du site de MSR: http://www.lsis.org/msr2017/index.php?menu=sou

MSR: 15-17 novembre 2017
Lieu: Campus de St-Charles à Marseille.

Journée AFSEC organisée par Pierre Bieber, Julien Brunel et Claire Pagetti.
Organisée avec le soutien du GDR GPL.
Organisation locale: Xiaoting Li, Sebti Mouelhi ECE

Quand: Le 21 juin 2017
Lieu: ECE Paris — Ecole d’ingénieurs
Campus Eiffel 1   10 rue Sextius Michel – 75015 Paris
Métro ligne 6 (stations Bir-hakeim ou Duplex), RER C (station Champ de Mars)

Du fait des restrictions budgétaires, l’action prendra en charge les pauses café et le repas de midi sera à la charge de chacun. L’inscription (gratuite) est nécessaire en envoyant un email à claire.pagetti@onera.fr ; objet : “Inscription AFSEC 21 juin” (cliquer sur le lien) – préciser : Nom et Affiliation.

Programme :

• 9h15-9h30: accueil
• 9h30-9h45: Mot d’accueil ECE
• 9h45-11h0  La sécurite des systèmes embarqués : quelques cas d’études (Vincent Nicomette, LAAS)
• Résumé: Les systèmes informatiques d’aujourd’hui ne sont plus des simples PC de bureau classiques. L’informatique est partout et elle est notamment de plus en plus embarquée, dans les moyens de transport par exemple mais aussi dans les objets connectés qui envahissent chaque jour d’avantage notre quotidien. Par ailleurs, l’utilisation massive du réseau Internet a facilité la propagation de logiciels malveillants, qui peuvent aujourd’hui cibler tous ces types d’équipements informatiques. Alors qu’il existe déjà des normes permettant d’évaluer la sécurité d’équipements informatiques “classiques”, leur application aux équipements embarqués est encore limitée. La présence et la criticité des vulnérabilités qui peuvent affecter ces équipements sont encore mal connues car pas suffisamment étudiées.
  Cet exposé présente des travaux de recherche qui ont été menés au LAAS depuis plusieurs années sur le thème de la sécurité des systèmes embarqués. Deux exemples seront présentés sur différents types d’équipements. La première étude
  présente une analyse de vulnérabilités d’un système embarqué critique avionique, réalisé dans la cadre d’une collaboration avec Airbus. La seconde étude concerne une analyse de vulnérabilités de systèmes embarqués dans deux types d’équipements connectés : les box ADSL et les téléviseurs connectés. Cette étude a été réalisée dans le cadre d’une collaboration avec Thalès. La présentation de ces cas d’études sera précédée d’une introduction générale à la sécurité informatique et aux propriétés associées.
• Bio: Vincent Nicomette est professeur à l’INSA de Toulouse et chercheur dans l’équipe Tolérance aux Fautes et Sûreté de Fonctionnement Informatique du LAAS-CNRS. Il est diplômé de l’ENSEEIHT option Informatique
  en 1992, a obtenu son doctorat de l’TNP de Toulouse en 1996 et son HDR de l’INP de Toulouse en 2009. Ses principaux thèmes de recherche concernent la sécurité dans les systèmes répartis, la sécurité des systèmes d’exploitation et des systèmes embarqués.
• 11h-12h Sécurité des applications : quels outils ? quelles techniques ? (Marie-Laure Potet, Verimag)
• Résumé: L’analyse de code pour chercher des vulnérabilités ou évaluer leur robustesse vis-à-vis d’attaques pose des problèmes différents de la vérification ou la recherche de bugs pour la sûreté. Dans un premier temps nous illustrerons ceci à travers des exemples et montrerons les outils adaptés pour ces analyses. Un premier type d’analyse de vulnérabilités sera ensuite illustré par l’approche Gueb, développée dans le cadre du projet ANR BinSec, qui combine analyses statique et concolique pour la détection de use-after-free. Nous nous intéresserons ensuite à l’analyse de la robustesse de code contre l’injection de fautes. Nous présenterons FISCC, la première collection publique de code durci contre l’injection de fautes ainsi que des métriques d’évaluation de la robustesse à l’injection de fautes. Ces derniers travaux sont développés dans le cadre du projet DGA-ANR Sertif.
• Bio: Marie-Laure Potet est Professeur à l’Ensimag, école de Grenoble INP, et chercheur au laboratoire Verimag. Elle a travaillé dans le domaine des méthodes formelles (approche correction par construction) pour la validation de systèmes sûrs et la certification Critères Communs. Depuis 8 ans elle anime une équipe à Vérimag sur l’analyse de code pour la sécurité et l’analyse de vulnérabilités à partir de modèles. Elle est impliquée dans de nombreux projets collaboratifs en sécurité.
• 13h-14h Vérification automatique de propriétés d’équivalence (Vincent Cheval, LORIA)
• Résumé: La conception et l’analyse des protocoles de sécurité sont connues pour être difficiles puisqu’elles demandent de considérer toutes les actions malicieuses d’un attaquant sur le protocole. Les modèles symboliques ont été utilisées avec succès pour prouver la sécurité de protocoles et pour découvrir de nouvelles failles de sécurité. Pourtant, prouver à la main la sécurité des protocoles cryptographiques est difficile et souvent source d’erreurs. C’est pourquoi une grande variété d’outils de vérification automatiques a été développée afin de prouver ou découvrir des attaques sur les protocoles. Je présenterai dans un premier temps un aperçu des outils existants puis je parlerai plus précisément des techniques de vérification automatique développées au sein de l’équipe PESTO pour vérifier différentes notions d’équivalence de processus. Ces notions étant particulièrement importantes pour exprimer de nombreuses propriétés de sécurité (ex: l’anonymat, la confidentialité du vote, la non-traçabilité).
• Bio: Vincent Cheval est  chargé de recherche à Inria Nancy au sein du LORIA. Ses thèmes de recherche concernent l’analyse et la vérification de protocoles cryptographiques au sein de modèles formels, développement d’outils et la vérification de programmes.
• 14h-15h Formal Methods and the Dark Side of the Force (Jean-Louis Lanet, Université de Rennes)
• Résumé: Formal methods have been used in the industry for a long time with some noticeable successes. Unfortunately any technology can have a dual use, and in particular, attackers can use rigorous technologies for discovering weaknesses in a product or hidding a code inside another one.
• Bio: Jean-Louis Lanet joined INRIA- Rennes Bretagne Atlantique in September 2014 to be involved into the High Security Labs (LHS) for a four years period. He has been Professor at the University of Limoges (2007-2014) at the Computer Science department, where he lead the team SSD (Smart Secure Device). He was also associate professor of the University of Sherbrooke and was in charge of the Security and Cryptology course of the USTH Master (Hanoi). His research interests included the security of small systems like smart cards, but also software engineering. Prior to that, he was senior researcher at Gemplus Research Labs (1996-2007) the smart card manufacturer. During this period he spent two years at INRIA (2003-2004) as an engineer at DirDRI (Direction des Relations Industrielles) and senior research associate in the Everest team at INRIA Sophia-Antipolis. He got my Habilitation à Diriger des Recherches (HdR) during the first INRIA period. He was researcher at the Advanced Studies Labs of Elecma, Electronic division of the Snecma, now part of the Safran group where he worked on hard real time techniques for jet engine control (1984-1995).
• 15h15-16h15 Model Based Safety and Security Analyses of Avionics Systems (Pierre Bieber et Julien Brunel, ONERA)
• Résumé: We aim at developing common models and tools to assess safety and security. In this talk we propose adaptations of models devised for safety assessment of avionics platforms in order to analyse their security. We describe  a security modelling and analysis approach based on the AltaRica and Alloy languages and their associated tools. The approach is illustrated by avionics case-studies. We report lessons learnt about the convergence and divergence points between security and safety with respect to modelling and analysis techniques.
• Bio: Pierre Bieber et Julien Brunel sont ingénieurs de recherche à l’ONERA Toulouse, ils travaillent sur les méthodes d’analyse de la sécurité des systèmes aéronautiques.
• 16h15-17h15 Opacité probabiliste (Béatrice Bérard, LIP6)
• Résumé: L’opacité est un cadre générique qui permet de décrire formellement certaines propriétés de sécurité liées aux fuites d’information. Elle prend comme paramètres les exécutions d’un système, dont
  certaines sont considérées comme secrètes, et une fonction d’observation fournissant une vue partielle des exécutions à un agent extérieur qui connaît la structure du système. Le secret est opaque si pour toute exécution secrète, il en existe une non secrète avec la même observation. Après un bref panorama des résultats obtenus, je présenterai des extensions probabilistes de la notion d’opacité, avec pour but de mesurer la résistance d’un système aux fuites d’information et d’en comparer plusieurs réalisations. (travaux communs avec Serge Haddad, Olga Kouchnarenko, Engel Lefaucheux, John Mullins et Mathieu Sassolas).
• Bio: Béatrice Bérard est professeur à l’Université P. et M. Curie et chercheur au LIP6, en délégation Inria au LSV pour 2016/2017. Ses thèmes de recherche concernent les questions d’expressivité et de vérification pour des modèles quantitatifs (temporisés ou probabilistes), avec des applications à la sécurité et aux systèmes de transport automatisés.

Journée commune AFSEC/PACS (ANR PACS : Parametric Analyses of Concurrent Systems)

Pour définir la taille de la salle et prévoir les autorisations d’accès au bâtiment , une inscription (gratuite) au plus tard le 10 mai 2016 est nécessaire en envoyant un email à olivier-h.roux@irccyn.ec-nantes.fr ; objet : “Inscription AFSEC 26 mai” (cliquer sur le lien) – préciser : Nom et Affiliation.

Quand: Le 26 mai 2016
Lieu: Salle 1009, Bâtiment Sophie Germain, IRIF, Université Paris Diderot
M° 14 / RER C Bibliothèque François Mitterrand / Tramway T3a Porte de France.

Programme (en cours d’élaboration) :

• 10h-11h Polynomial Interrupt Timed Automata (Serge Haddad, LSV – ENS Cachan)
• Résumé: Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA.
  Joint work with B. Bérard (LIP6), C. Picaronny (LSV) , M. Safey El Din (LIP6) and M. Sassolas (LACL).
• 11h-12h Symbolic Robustness Analysis of Timed Automata. (Ocan Sankur, IRISA – Rennes)
• Résumé:
  We study the robust safety problem for timed automata under guard imprecisions which consists in computing a bound on the perturbations on delays under which a safety specification holds. We give a symbolic semi-algorithm for the problem based on a parametric data structure, and evaluate its performance in comparison with a recently published one, and with a binary search on enlargement values.
• 14h-15h Reachability in Networks of Register Protocols under a Fair Stochastic Scheduler (Arnaud Sangnier, LIAFA – Paris 7)
• Résumé: We study the almost-sure reachability problem in a distributed system
  obtained as the asyn- chronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
  This is a joint work with Patricia Bouyer, Nicolas Markey, Mickael Randour and Daniel Stan.
• 15h-16h Controlling Actions and Time in Parametric Timed Automata (Laure Petrucci, LIPN – Paris 13)
• Résumé:
  Cyber-physical systems involve both discrete actions and real-time that elapses depending on timing constants.
  In this paper, we introduce a formalism for such systems containing both real-time parameters in linear timing constraints and switchable (Boolean) actions.
  We define a new approach for synthesizing combinations of parameter valuations and allowed actions, under which the system correctness is ensured when expressed in the form of a safety property.
  We apply our approach to a railway crossing system example with a malicious intruder potentially threatening the system safety.

Journée AFSEC organisée Par Claire Pagetti et Rémi Delmas
Organisée avec le soutien du GDR GPL.

Quand: Le 29 mars 2016
Lieu: Université Paris Diderot amphi Turing du bâtiment Sophie Germain map

Du fait des restrictions budgétaires, l’action prendra en charge les pauses café et le repas de midi sera à la charge de chacun. L’inscription (gratuite) au plus tard le 20 mars 2016 est nécessaire
en envoyant un email à claire.pagetti@onera.fr ; objet : “Inscription AFSEC 29 mars” (cliquer sur le lien) – préciser : Nom et Affiliation.

Programme :

• 9h30-10h00: accueil
• 10h00-11h15 Présentation de l’approche SMT (fondements mathématiques et logiques) et le standard SMT-lib (Pascal Fontaine, LORIA)
• Résumé: Avant d’aborder les solveurs Satisfaisabilité Modulo Théories (SMT), nous considérerons brièvement le problème SAT de la satisfaisabilité en logique propositionnelle, et les techniques actuelles pour le résoudre, ces techniques étant elles aussi utilisées au coeur des les solveurs SMT.  Nous verrons ensuite l’architecture SMT, et comment elle s’articule autour d’un solveur SAT.  En particulier, nous verrons par l’exemple comment on peut élever l’expressivité d’un solveur SAT vers des langages plus riches, et comment, à partir de procédures de décision pour différents langages, on peut construire une procédure de décision sur la combinaison des langages.
  Enfin, nous présenterons quelques solveurs SMT disponibles, la communauté SMT et les différentes initiatives, notamment le standard SMT-lib qui définit un langage d’entrée accepté par la majorité des solveurs SMT.
• 11h15-12h30 Implémentation d’un solveur SMT: le cas Alt-Ergo (Theory-comb, AC-comp, Quantificateurs, etc) (Mohamed Iguernlala, OCamlPro/LRI)
• Résumé: Alt-Ergo est un démonstrateur SMT conçu pour le domaine de la vérification de programmes. Il est intégré dans plusieurs outils, en particulier via la plateforme Why3. Il est utilisé par Frama-C et Caveat pour démontrer la validité d’obligations de preuves (OPs) issues de code C, par SPARK pour prouver les OPs générées à partir de programmes Ada, ainsi que sur des OPs générées par Atelier-B. Il est aussi utilisé par EasyCrypt pour la vérification de protocoles de cryptographie et par Cubicle pour faire du model-checking.
  Le langage d’entrée d’Alt-Ergo est une logique du premier ordre avec types polymorphes et théories prédéfinies. Son coeur combine un SAT-solver inspiré de la méthode des tableaux, un moteur d’instantiation de formules quantifiées, et un ensemble de procédures de décision pour des théories telles que la théorie de l’égalité non-interprétée, l’arithmétique linéaire sur les entiers et les rationnels, les tableaux fonctionnels polymorphes, les types énumérés ainsi que la théorie AC des symboles associatifs et commutatifs. Cet exposé sera l’occasion de revenir sur quelques détails d’implémentation d’Alt-Ergo, et sur les particularités qui font sa force dans le domaine de la vérification de programmes.
• 13h45-14h45 Vérification déductive de programmes (Claude Marché, LRI)
• Résumé: Le principe de l’approche déductive de la vérification consiste, à partir d’un programme et d’une spécification formelle, à générer des “obligations de preuve”: des formules logiques dont la validité implique que le programme respecte sa spécification. Nous illustrons cette approche telle qu’elle est implantée dans l’environnement Why3, ainsi que dans les plateformes Frama-C et SPARK pour la vérification de codes critiques C et Ada. Les solveurs SMT sont utilisés de manière prépondérante pour la preuve automatique des obligations de preuve. Nous examinons les avantages et les inconvénients de ces solveurs dans ce contexte.
• 14h45-15h45 Solveurs SAT application au model-checking (Loïg Jezequel, Université de Nantes)
• Résumé: La planification est un domaine de l’intelligence artificielle ayant pour objectif de trouver des séquences d’actions (des plans) permettant d’atteindre, depuis l’état initial d’un système, un état objectif. Au début des années 90 une méthode de planification reposant sur l’utilisation de solveurs SAT a été proposée. Il s’agit de re-coder un problème de planification comme un ensemble (généralement infini) de problèmes SAT, puis de chercher à les résoudre l’un après l’autre dans un ordre bien choisi. Dès qu’une solution à l’un de ces problèmes SAT est trouvée, le problème de planification correspondant est résolu. Cette technique de planification s’est révélée surprenamment efficace, notamment en raison des efforts importants ayant été menés pour optimiser l’implantation des solveurs SAT.
  Dans cet exposé, nous présenterons une manière d’encoder les problèmes de planification comme des ensembles de problèmes SAT. Nous montrerons ensuite comment cette approche peut se généraliser pour calculer non plus un seul plan, mais des ensembles exhaustifs de plans, sous forme d’arbres d’exécution. Enfin, nous discuterons la possibilité d’étendre l’approche pour calculer des préfixes finis complets de dépliages de réseaux de Petri, comparables aux arbres d’exécution, mais plus compacts car prenant en compte la concurrence des réseaux de Petri.
• 16h00-17h00 Synthèse d’un diagnostiqueur déterministe pour la prise de décision embarquée (Stéphanie Roussel, ONERA)
• Résumé: Nous nous intéressons au problème de la synthèse d’un diagnostiqueur à base de modèle devant être intégré avec un algorithme de planification en vue d’une prise de décision embarquée. Les planificateurs que nous visons étant déterministes (pas de gestion de l’incertitude), le diagnostiqueur doit renvoyer à chaque étape un unique diagnostic. Nous utilisons alors une combinaison de systèmes de transition, logique temporelle et réseau de préférences conditionnelles booléennes (CP-Nets) pour spécifier le diagnostiqueur. Nous décrivons différentes réductions du  calcul d’un diagnostic vers le cadre de satisfaction booléenne et comparons des implémentations basées SAT et BDD sur un benchmark de type mission multi-robots soumis à différentes pannes.
• 17h00-18h00 Synthèse d’architecture embarquées et vérification fonctionnelle de programmes synchrones basées SAT/SMT (Rémi Delmas, ONERA)
• Résumé: Dans cet exposé nous présenterons un panorama des applications de SAT et SMT conduites au DTIM pour l’assistance à la conception et à la vérification de systèmes embarqués, allant de la vérification de propriétés de safety pour des programmes synchrones écrits en lustre avec l’outil STUFF, à la synthèse de plans de câblage de poids minimal pour la connexion de capteurs au réseau avionique avec le langage eLogical et sa traduction en logique pseudo-booléenne, en passant par l’allocation de niveaux de DAL et de budgets de taux de défaillance aux composants d’un système avionique à partir d’informations issues d’analyses de safety (coupes minimales) et du profil d’utilisation de l’avion, à l’aide de solveurs SAT, pseudo-booléens et de programmation MILP.

Lors du 10e Colloque sur la Modélisation des Systèmes Réactifs (MSR 2015), qui aura lieu à Nancy du 18 au 20 novembre, les groupes SED (GDR MACS) et AFSEC organisent une session sur le thème des logiciels pour la recherche relatif à modélisation, l’analyse et la commande des systèmes réactifs et temps réel. Le but est de présenter à la communauté les logiciels que vous avez développés ou que vous utilisez dans le cadre de vos travaux de recherche.

Cette présentation se fera en deux temps :

• Une présentation rapide (5 minutes) en session plénière : genèse de l’outil, fonctionnalités, licences, copies d’écran…
• Un temps plus long de discussion autour des démonstrateurs, ou chacun pourra de manière informelle échanger avec les présentateurs et tester les outils qui les intéressent particulièrement

Nous lançons donc un appel à propositions à tous ceux qui souhaitent présenter un outil qu’ils jugent intéressant. Le but n’est pas de vendre ou de gagner un prix mais de partager votre expérience ou votre travail.
N’hésitez donc pas à proposer de présenter votre propre création, même si elle n’est qu’en version alpha, ou au contraire un outil mature que vous maîtrisez.

Nous espérons présenter entre 5 et 10 outils. Nous attendons vos propositions et dans un deuxième temps nous reviendrons vers celles
retenues pour préciser les moyens matériels et logiciels à mettre en oeuvre.

Les personnes intéressées sont invitées à se faire connaître (sans trop tarder) auprès de
РLaurent Pi̩trac, laurent.pietrac@insa-lyon.fr
РS̩bastien Lahaye, sebastien.lahaye@univ-angers.fr
– ou Olivier H. Roux, olivier-h.roux@irccyn.ec-nantes.fr
en transmettant une brève description de leur outil logiciel.