Le cours Automated Reasoning : Le cours de vérification de modèles symboliques présente la manière dont les propriétés des systèmes d'action et des programmes peuvent être vérifiées automatiquement. La notion de base est un système de transition : tout système qui peut être décrit par des états et des étapes. Nous présentons comment, en CTL (computation tree logic), des propriétés telles que l'accessibilité peuvent être décrites. Typiquement, un espace d'états peut être très grand. L'une des façons de traiter ce problème est le model checking symbolique : une façon de représenter symboliquement des ensembles d'états. Les définitions et les propriétés de base des BDD sont présentées dans ce cours, ainsi que les algorithmes permettant de les calculer, comme cela est nécessaire pour la vérification de modèles CTL.
Après une introduction générale au MOOC, ce module commence par une description générale de la vérification de modèle, puis la logique des arbres de calcul (CTL) est introduite : un langage dans lequel les propriétés des systèmes de transition peuvent être décrites. L'algorithme permettant de vérifier si une telle propriété est valable est donné dans un cadre abstrait, laissant implicite la façon dont les ensembles d'états sont représentés.
Inclus
5 vidéos3 devoirs
Afficher les informations sur le contenu du module
5 vidéos•Total 44 minutes
Introduction générale•6 minutes
Contrôle des modèles•9 minutes
Arbre de calcul Logique•11 minutes
Algorithme logique de l'arbre de calcul•11 minutes
Exemple de logique d'arbre de calcul•8 minutes
3 devoirs•Total 30 minutes
Taille de l'espace d'état•10 minutes
Équivalence CTL•10 minutes
Exemple CTL•10 minutes
BDDs partie 1
Module 2•1 heure à terminer
Détails du module
Dans ce module, les BDD (diagrammes de décision binaires) sont présentés comme des arbres de décision avec partage. Des exigences supplémentaires concernant les arbres de décision et les BDD sont présentées, ce qui permet de conclure à l'unicité de la représentation.
Inclus
4 vidéos3 devoirs
Afficher les informations sur le contenu du module
4 vidéos•Total 33 minutes
Représentation des fonctions booléennes•8 minutes
Arbres de décision•7 minutes
Arbres de décision 2•10 minutes
BDD•8 minutes
3 devoirs•Total 30 minutes
Arbre décisionnel•10 minutes
Arbre de décision ordonné réduit•10 minutes
ROBDD•10 minutes
BDDs partie 2
Module 3•2 heures à terminer
Détails du module
Après quelques exemples de BDD, l'algorithme est présenté et discuté pour calculer le ROBDD de n'importe quelle formule propositionnelle.
Inclus
4 vidéos3 devoirs
Afficher les informations sur le contenu du module
4 vidéos•Total 35 minutes
Exemples de BDD•11 minutes
Algorithme BDD•10 minutes
Algorithme BDD 2•6 minutes
Exemple d'algorithme BDD•8 minutes
3 devoirs•Total 70 minutes
BDD quiz 1•20 minutes
BDD quiz 2•20 minutes
Algorithme BDD•30 minutes
Vérification de modèles symboliques basée sur BDD
Module 4•9 heures à terminer
Détails du module
Dans ce dernier module, les thèmes de la vérification de modèle CTL et des BDD sont combinés : il est montré comment les BDD peuvent être utilisés pour représenter des ensembles d'états de manière à ce que l'algorithme abstrait pour la vérification de mode CTL puisse être utilisé, et que des espaces d'états beaucoup plus grands puissent être traités qu'en utilisant la vérification de modèle basée sur les états explicites. Plusieurs exemples sont présentés.
Inclus
4 vidéos3 lectures3 devoirs
Afficher les informations sur le contenu du module
4 vidéos•Total 39 minutes
Algorithme BDD CTL•10 minutes
Un exemple : les renards et les lapins•9 minutes
Vérification des impasses dans un réseau•10 minutes
Réseaux, BMC, conclusions•10 minutes
3 lectures•Total 90 minutes
Le NuSMV à l'origine du problème des renards et des lapins•10 minutes
Introduction•10 minutes
Explication des réseaux de commutation par paquets et fichier décrivant la fonction de routage•70 minutes
3 devoirs•Total 420 minutes
Problème 1 : billes de couleur•60 minutes
Problème 2 : atteindre des valeurs égales•120 minutes
Problème 3 : blocages dans les réseaux de commutation par paquets•240 minutes
Instructeur
Évaluations de l’enseignant
Évaluations de l’enseignant
Nous avons demandé à tous les étudiants de fournir des commentaires sur nos enseignants au sujet de la qualité de leur pédagogie.
28DIGITAL est le moteur de l'innovation numérique en Europe, une plateforme multipartite, ancrée dans les valeurs européennes et ouverte sur le monde. Nous transformons la connaissance en innovation, transformons les start-ups en entreprises mondiales et formons la prochaine génération de talents numériques pour façonner un avenir numérique équitable, compétitif et centré sur l'humain.
nous travaillons à l'intersection de la science, des affaires et de la société, transformant les percées en IA, cybersécurité, robotique et informatique avancée en solutions qui favorisent l'innovation dans les technologies numériques, accélèrent la transition écologique et améliorent les vies. 28DIGITAL fournit un enseignement en ligne et en face-à-face sur l'innovation et l'entrepreneuriat afin d'améliorer la qualité, d'accroître la diversité et d'étendre la disponibilité d'un contenu de haut niveau provenant de 20 universités techniques de premier plan à travers l'Europe. Les universités offrent un mélange unique du meilleur de l'excellence technique, des compétences entrepreneuriales et de l'esprit aux ingénieurs et entrepreneurs numériques à tous les stades de leur carrière. Les partenaires académiques soutiennent la vision audacieuse de Coursera qui consiste à permettre à n'importe qui, n'importe où, de transformer sa vie en donnant accès aux meilleures expériences d'apprentissage au monde. Cela signifie que 28DIGITAL partage progressivement des parties de ses programmes d'éducation entrepreneuriale et académique pour démontrer son excellence et la rendre accessible à un public beaucoup plus large. Le portefeuille d'éducation en ligne de 28DIGITAL peut être utilisé dans des contextes d'éducation mixte, à la fois dans les programmes de maîtrise et de doctorat, et par les professionnels pour mettre à jour leurs connaissances
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?
Felipe M.
Étudiant(e) depuis 2018
’Pouvoir suivre des cours à mon rythme à été une expérience extraordinaire. Je peux apprendre chaque fois que mon emploi du temps me le permet et en fonction de mon humeur.’
Jennifer J.
Étudiant(e) depuis 2020
’J'ai directement appliqué les concepts et les compétences que j'ai appris de mes cours à un nouveau projet passionnant au travail.’
Larry W.
Étudiant(e) depuis 2021
’Lorsque j'ai besoin de cours sur des sujets que mon université ne propose pas, Coursera est l'un des meilleurs endroits où se rendre.’
Chaitanya A.
’Apprendre, ce n'est pas seulement s'améliorer dans son travail : c'est bien plus que cela. Coursera me permet d'apprendre sans limites.’
Pour accéder aux supports de cours, aux devoirs et pour obtenir un certificat, vous devez acheter l'expérience de certificat lorsque vous vous inscrivez à un cours. Vous pouvez essayer un essai gratuit ou demander une aide financière. Le cours peut proposer l'option "Cours complet, pas de certificat". Cette option vous permet de consulter tous les supports de cours, de soumettre les évaluations requises et d'obtenir une note finale. Cela signifie également que vous ne pourrez pas acheter un certificat d'expérience.
Qu'est-ce que je recevrai si je souscris à cette Specializations ?
Lorsque vous vous inscrivez au cours, vous avez accès à tous les cours de la spécialisation et vous obtenez un certificat lorsque vous terminez le travail. Votre certificat électronique sera ajouté à votre page Réalisations - de là, vous pouvez imprimer votre certificat ou l'ajouter à votre profil LinkedIn.
Une aide financière est-elle disponible ?
Oui, pour certains programmes de formation, vous pouvez demander une aide financière ou une bourse si vous n'avez pas les moyens de payer les frais d'inscription. Si une aide financière ou une bourse est disponible pour votre programme de formation, vous trouverez un lien pour postuler sur la page de description.