Les enseignements de la chaire ASC

École polytechnique : Filière Méthodes Formelles

Méthodes formelles et fondements des systèmes cyber-physiques

Les méthodes formelles sont des techniques mathématiquement rigoureuses pour la spécification, le développement, l'analyse et la vérification des systèmes logiciels et matériels. Les méthodes formelles ont développé des sujets logiques et mathématiques approfondis tels que l'interprétation abstraite, les méthodes de preuve et les assistants (et les cadres logiques d'ordre supérieur tels que Coq, Agda, Lean), la vérification de modèles et les algorithmes SAT/SMT qui sont au cœur de cette piste, avec tous les aspects sémantiques et algorithmiques pertinents.

Télécom SudParis : Complex Networks

Automata based approaches

Contenus du cursus 1 : Grands Graphes, systèmes complexes, réseaux sociaux, graph du web, diffusion de l’information dans les grands graphes

• Lois de d’échelle
• Rappel de théorie des graphes
• Graphes aléatoires
• Propriétés statistiques remarquables des grands graphes de terrain (graphe du web) : Effet petit monde, Lois d’échelle dans les grands graphes, Modélisation des grands graphes, Structure de l’internet
• Détections de communautés dans les graphs graphes de terrain : Application aux réseaux sociaux en ligne
• Navigation dans les graphes (Algorithme du PageRank)
• Robustesse des grands systèmes : Panne en cascade, Robustesse de l’Internet
• Mécanismes de diffusion de l’information dans les graphes (modélisation épidémie, Marketing virale dans les réseaux sociaux)

Contenus du cursus 2

• Aperçu Test vs vérification
• Modélisation et abstraction des systèmes du monde réel
• Des systèmes aux mots, traces et langages
• Réduction des expressions régulières en automates finis (2, p)
• Tour d'horizon des méthodes formelles
• Assistants de preuve formelle
• Analyse de code
• Systèmes concurrents et distribués
• Exécution séquentielle vs exécution concurrente
• Horloges de Lamport et relation « happens-before »
• Partage des ressources et exclusion mutuelle (2, p)
• Protocoles de validation et autres algorithmes distribués (3, p)
• Conception, raffinement et implémentation
• Implémentation d'une conception (2, p)
• Composition des sous-systèmes (3, p)

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 

Les partenaires industriels de la chaire ASC (Dassault Aviation, Naval Group et KNDS France) interviennent chaque année en conférence ou en chargé de cours aux sein des Écoles de l'Institut Polytechnique de Paris impliquées.

Par ailleurs Dassault Systèmes fournit aux écoles les licences logicielles pour les rôles utilisés en cours en lors des projets (3DS, Catia, CatiaMagic, Dymola...)

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 

Le challenge ASC : une réponse à la volonté de la chaire de diffuser l’Architecture des Systèmes Complexes de manière transversale et commune aux Écoles de l'Institut Polytechnique de Paris.

Ce challenge a pour but d’apporter aux élèves participants des connaissances dans les domaines de :

• La complexité ;
• L’approche systémiques ;
• L’approche des systèmes de systèmes (SoS) ;
• L’ingénierie système basée sur les modèles (MBSE) ;
• La comparaison et l’évaluation de variantes d’architectures de SoS. 

Pour accéder à la plateforme du challenge, cliquez ici.