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.
(52 avis)
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
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 5 modules dans ce cours
Nous présentons les systèmes de transition étiquetés (LTS), la syntaxe et la sémantique de la logique arborescente computationnelle (CTL) et discutons des algorithmes de vérification de modèle nécessaires pour calculer l'ensemble de satisfaction pour des formules CTL spécifiques.
Inclus
6 vidéos3 lectures4 devoirs
Nous améliorons les systèmes de transition par le temps discret et ajoutons des probabilités aux transitions pour modéliser les choix probabilistes. Nous discutons des propriétés importantes des DTMC, telles que la propriété sans mémoire et l'homogénéité temporelle. La classification des états peut être utilisée pour déterminer l'existence de la distribution limite et/ou stationnaire.
Inclus
5 vidéos2 lectures5 devoirs
Nous discutons de la syntaxe et de la sémantique de la logique de l'arbre computationnel probabiliste et vérifions les algorithmes de vérification de modèle qui sont nécessaires pour décider de la validité de différents types de formules PCTL. Nous discutons brièvement de la complexité de la vérification de modèles PCTL.
Inclus
5 vidéos3 lectures6 devoirs
Nous améliorons les chaînes de Markov en temps discret avec le temps réel et discutons de la façon dont le formalisme de modélisation résultant évolue dans le temps. Nous calculons l'état d'équilibre pour différents types de chaînes de Markov à temps discret et examinons comment les probabilités transitoires peuvent être calculées efficacement à l'aide d'une méthode appelée uniformisation.
Inclus
5 vidéos2 lectures6 devoirs
Nous introduisons la syntaxe et la sémantique de la logique stochastique continue et décrivons comment les différents types de formules CSL peuvent être vérifiés. En particulier, la vérification du modèle de l'opérateur time bounded until nécessite l'application du concept d'uniformisation, que nous avons abordé dans le module précédent.
Inclus
5 vidéos2 lectures6 devoirs
Instructeur
Offert par
Recommandé si vous êtes intéressé(e) par Développement de logiciels
Politecnico di Milano
Politecnico di Milano
Dartmouth College
École Polytechnique Fédérale de Lausanne
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?
Avis des étudiants
Affichage de 3 sur 52
52 avis
- 5 stars
57,69 %
- 4 stars
25 %
- 3 stars
5,76 %
- 2 stars
5,76 %
- 1 star
5,76 %
Révisé le 26 août 2023
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.