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.
Raisonnement automatisé : Vérification de modèles symboliques
Enseigné en Anglais
Certains éléments de contenu peuvent ne pas être traduits
2 615 déjà inscrits
(26 avis)
Expérience recommandée
Détails à connaître
Ajouter à votre profil LinkedIn
12 quizzes
Découvrez comment les employés des entreprises prestigieuses maîtrisent des compétences recherchées
Obtenez un certificat professionnel
Ajoutez cette qualification à votre profil LinkedIn ou à votre CV
Partagez-le sur les réseaux sociaux et dans votre évaluation de performance
Il y a 4 modules dans ce cours
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 quizzes
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 quizzes
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 quizzes
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 quizzes
Instructeur
Offert par
Recommandé si vous êtes intéressé(e) par Développement de logiciels
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?
Ouvrez de nouvelles portes avec Coursera Plus
Accès illimité à plus de 7 000 cours de renommée internationale, à des projets pratiques et à des programmes de certificats reconnus sur le marché du travail, tous inclus dans votre abonnement
Faites progresser votre carrière avec un diplôme en ligne
Obtenez un diplôme auprès d’universités de renommée mondiale - 100 % en ligne
Rejoignez plus de 3 400 entreprises mondiales qui ont choisi Coursera pour les affaires
Améliorez les compétences de vos employés pour exceller dans l’économie numérique
Foire Aux Questions
L'accès aux cours et aux devoirs dépend de votre type d'inscription. Si vous suivez un cours en mode audit, vous pourrez consulter gratuitement la plupart des supports de cours. Pour accéder aux devoirs notés et obtenir un certificat, vous devrez acheter l'expérience de certificat, pendant ou après votre audit. Si vous ne voyez pas l'option d'audit :
Il se peut que le cours ne propose pas d'option d'audit. Vous pouvez essayer un essai gratuit ou demander une aide financière.
Le cours peut proposer l'option "Cours complet, pas de certificat" à la place. 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.
Lorsque vous vous inscrivez au cours, vous avez accès à tous les cours de la Specializations, et vous obtenez un certificat lorsque vous terminez le travail. Votre certificat électronique sera ajouté à votre page de réalisations - de là, vous pouvez imprimer votre certificat ou l'ajouter à votre profil LinkedIn. Si vous souhaitez uniquement lire et visualiser le contenu du cours, vous pouvez auditer le cours gratuitement.
Si vous vous êtes abonné, vous bénéficiez d'une période d'essai gratuite de 7 jours pendant laquelle vous pouvez annuler votre abonnement sans pénalité. Après cette période, nous ne remboursons pas, mais vous pouvez résilier votre abonnement à tout moment. Consultez notre politique de remboursement complète.