Bienvenue au cours de pointe sur la vérification quantitative de modèles pour les chaînes de Markov ! Alors que la technologie s'infiltre dans tous les aspects de la vie moderne - systèmes intégrés, systèmes cyber-physiques, protocoles de communication et systèmes de transport - le besoin de logiciels fiables n'a jamais été aussi grand. Une seule petite faille peut entraîner des défaillances catastrophiques et des coûts énormes. Le cours commence par la création d'un système de transition d'états, le modèle de base qui capture la dynamique complexe des systèmes du monde réel. Bientôt, vous entrerez dans le monde des chaînes de Markov à temps discret et à temps continu, de puissants formalismes mathématiques suffisamment polyvalents pour modéliser des systèmes complexes tout en étant élégants dans leur conception. Il ne s'agit pas seulement de théories ; ce sont des outils activement utilisés dans divers domaines pour l'évaluation des performances et de la fiabilité. Mais nous ne nous arrêterons pas à la modélisation. Le cœur de ce cours est le "Model Checking", une méthode de vérification formelle qui examine minutieusement la fonctionnalité de votre modèle de système. Apprenez à exprimer les propriétés de sûreté de fonctionnement, à suivre l'évolution des chaînes de Markov dans le temps et à vérifier si les états répondent à des conditions particulières, tout cela en utilisant des algorithmes de calcul avancés. A la fin de ce cours, vous serez équipé des compétences nécessaires pour : - Spécifier les propriétés de sûreté de fonctionnement pour une gamme de systèmes de transition - Comprendre l'évolution temporelle des chaînes de Markov - Analyser et calculer l'ensemble de satisfaction pour des propriétés multiples. Êtes-vous prêt à devenir un expert pour assurer la fiabilité des technologies de demain ? Cliquez ici pour vous inscrire aujourd'hui et rejoignez-nous pour maîtriser l'art et la science du model checking.

Vérification quantitative des modèles

54 avis
Ce que vous apprendrez
Apprendre les fondements de la vérification quantitative de modèles pour les systèmes probabilistes et stochastiques.
Modéliser et analyser des systèmes à l'aide de chaînes de Markov à temps discret et à temps continu.
Appliquer la logique des arbres de calcul (CTL) et la logique des arbres probabilistes (PCTL) pour vérifier formellement les propriétés des systèmes.
Utiliser des techniques de vérification formelle pour évaluer la fiabilité, les performances et la sûreté de fonctionnement des systèmes embarqués, cyber-physiques et de communication
Compétences que vous acquerrez
- Catégorie : Analyse des systèmes
- Catégorie : Modèle de Markov
- Catégorie : Vérification et validation
- Catégorie : Logique informatique
- Catégorie : Raisonnement logique
- Catégorie : Modélisation mathématique
- Catégorie : Distribution de probabilité
- Catégorie : Informatique théorique
- Catégorie : Modélisation des processus
- Catégorie : Algorithmes
- Catégorie : Probabilité
Détails à connaître

Ajouter à votre profil LinkedIn
27 devoirs
Découvrez comment les employés des entreprises prestigieuses maîtrisent des compétences recherchées

Il y a 5 modules dans ce cours
Instructeur

Offert par
En savoir plus sur Développement de logiciels

University of Colorado Boulder
University of Colorado Boulder

University of Colorado Boulder
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?

Felipe M.

Jennifer J.

Larry W.

Chaitanya A.
Avis des étudiants
- 5 stars
59,25 %
- 4 stars
24,07 %
- 3 stars
5,55 %
- 2 stars
5,55 %
- 1 star
5,55 %
Affichage de 3 sur 54
Révisé le 26 août 2023
It's not my specialty, just thank you Thanks It's not my specialty, just thank you Thanks It's not my specialty, just thank you Thanks
Foire Aux Questions
Plus de questions
Aide financière disponible,





