La production de la chaire ASC

L'ensemble des articles scientifiques publiés est ici : https://ip-paris.hal.science/search/index?q=collCode_s%3AASC

Quelques exemples de publications :

Correct-by-construction requirement decomposition

Georgios BAKIRTZIS

Correct-by-construction requirement decomposition / Décomposition des exigences correcte par construction

En ingénierie des systèmes, la décomposition précise des exigences est cruciale pour créer des composants de système bien définis et gérables, en particulier dans les domaines critiques pour la sécurité. Malgré ce besoin crucial, les méthodologies rigoureuses et descendantes pour décomposer efficacement des exigences complexes en sous-exigences précises et actionnables sont rares, surtout comparées à la richesse des techniques de vérification ascendantes. Dans cet article les auteurs démontrent l'efficacité et la faisabilité d'une approche correcte par construction à travers une étude de cas complète, mettant en évidence comment la méthodologie qu’ils proposent améliore l'interprétabilité, la traçabilité et la vérifiabilité des exigences du système.

Pour en savoir plus : 

• Lien vers l'article
• Lien vers le post LinkedIn associé

Safety Assurance under Uncertainties From Software to Cyber-Physical/Machine Learning Systems

Jérémy DUBUT

L'assurance de la sécurité des systèmes logiciels n'a jamais été un problème aussi imminent qu'aujourd'hui. Les praticiens et les chercheurs qui travaillent sur ce problème sont confrontés à un défi unique aux systèmes logiciels modernes : les incertitudes. D'une part, la nature cyber-physique des systèmes logiciels modernes, comme l'illustrent les systèmes de conduite automatisée, impose de traiter les incertitudes environnementales et d'atténuer les risques qui en résultent. De plus, l'abondance de composants d'apprentissage automatique statistiques et d'unités massives de calcul numérique pour le raisonnement statistique, comme les réseaux de neurones profonds, rendent les systèmes difficiles à expliquer, comprendre, analyser ou vérifier.

Ce livre est le premier à fournir un aperçu complet de ces efforts unis et interdisciplinaires. En s'appuyant sur les systèmes de conduite automatisée comme exemple principal, le livre décrit diverses techniques pour spécifier, modéliser, tester, analyser et vérifier les systèmes logiciels modernes.

Dans son domaine d’expertise, Jérémy Dubut-Kross a corédigé le chapitre « Formal Specification of Temporal Properties » qui est une base pour de nombreux autres chapitres de l’ouvrage car il introduit ce que l'on appelle les spécifications formelles. Les spécifications formelles sont nécessaires chaque fois que l'on souhaite vérifier automatiquement si un système se comporte comme prévu pour une entrée donnée. Elles sont donc nécessaires dans de nombreuses méthodes de test et de vérification.

Safety Assurance under Uncertainties est donc un ouvrage de synthèse à retrouver dans les bibliothèques de toutes les structures impliquées dans la validation de systèmes critiques.

Pour en savoir plus :

• Lien vers l'article
• Lien vers le post LinkedIn associé

Petri Nets and Higher-Dimensional Automata

Philipp SCHLEHUBER

Les réseaux de Petri en tant qu’automates de dimensions supérieures, Les réseaux de Petri et leurs variantes sont souvent étudiés à travers leurs sémantiques entrelacées, c'est-à-dire en considérant des exécutions où, à chaque étape, une seule transition se produit. Cela constitue clairement une lacune, car les réseaux de Petri sont un modèle de concurrence réelle. Cet article revisite la sémantique des réseaux de Petri en tant qu'automates de dimension supérieure (ADS), comme introduit par van Glabbeek, qui prennent systématiquement en compte la concurrence. Les auteurs étendent la traduction pour inclure certaines caractéristiques courantes. Ils considèrent les réseaux avec arcs inhibiteurs, sous les deux sémantiques concurrentes utilisées dans la littérature, ainsi que les réseaux auto-modifiants généralisés. Enfin, les auteurs présentent un outil qui implémente leurs traductions.

Pour en savoir plus :

• Lien vers l'article
• Lien vers le post LinkedIn associé