Introduction to Modeling for Formal Verification

Économisez sur les compétences qui vous font briller avec 40 % de réduction sur 3 mois de Coursera Plus. Économisez maintenant

Ce cours n'est pas disponible en Français (France)

Nous sommes actuellement en train de le traduire dans plus de langues. Consultez les langues disponibles.

Introduction to Modeling for Formal Verification

Ce cours fait partie de Spécialisation "Fundamentals of Model Checking"

Instructeur : Hao Zheng

Inclus avec

3 modules

Obtenez un aperçu d'un sujet et apprenez les principes fondamentaux.

11 avis

niveau Débutant

Expérience recommandée

1 semaine à compléter

à 10 heures par semaine

Planning flexible

Apprenez à votre propre rythme

3 modules

Obtenez un aperçu d'un sujet et apprenez les principes fondamentaux.

11 avis

niveau Débutant

Expérience recommandée

1 semaine à compléter

à 10 heures par semaine

Planning flexible

Apprenez à votre propre rythme

Ce que vous apprendrez

Explain functional verification and model checking, including their benefits and drawbacks
Describe transition systems and how they represent behavior of hardware and software
Use program graphs to describe systems with data-dependent control
Describe communication models for system composition, including concurrency, shared variables, handshake, and synchronous parallelism.

Compétences que vous acquerrez

Catégorie : Computational Logic
Catégorie : Communication Systems
Catégorie : Theoretical Computer Science
Catégorie : Graph Theory
Catégorie : Systems Design
Catégorie : Verification And Validation
Catégorie : Computer Engineering
Catégorie : Process Modeling

Outils que vous découvrirez

Catégorie : Software Systems

Détails à connaître

Certificat partageable

Ajouter à votre profil LinkedIn

Évaluations

10 devoirs

Enseigné en Anglais

Découvrez comment les employés des entreprises prestigieuses maîtrisent des compétences recherchées

En savoir plus sur Coursera pour les affaires

logos de Petrobras, TATA, Danone, Capgemini, P&G et L'Oreal

Élaborez votre expertise du sujet

Ce cours fait partie de la Spécialisation "Fundamentals of Model Checking"

Lorsque vous vous inscrivez à ce cours, vous êtes également inscrit(e) à cette Spécialisation.

Apprenez de nouveaux concepts auprès d'experts du secteur
Acquérez une compréhension de base d'un sujet ou d'un outil
Développez des compétences professionnelles avec des projets pratiques
Obtenez un certificat professionnel partageable

Il y a 3 modules dans ce cours

This course introduces the basic concepts of functional verification and model checking, highlighting their importance in modern system designs. It explains different modeling formalisms for representing the behavior of hardware and software, which are either suitable for automated analysis or can represent data-dependent controls that are common in computing system designs. Additionally, it describes system compositions with respect to different communication models.

This module introduces basic concepts of functional verification and model checking. It demonstrates the importance of verification via some examples, outlines the challenges, and reviews pros and cons of model checking with respect to other verification methods.

Inclus

7 vidéos8 lectures3 devoirs

7 vidéosTotal 53 minutes

Motivating Examples7 minutes
High Profile Previous Bugs and Their Impacts10 minutes
Overview of Functional Verification5 minutes
Techniques for Functional Verification10 minutes
Overview of Formal Verification and Model Checking7 minutes
Elements of Model Checking6 minutes
Challenge to Model Checking: State Space Explosion6 minutes

8 lecturesTotal 151 minutes

Course Updates and Accessibility Support1 minute
Non-Credit Students: Welcome and Where to Find Help10 minutes
Principles of Model Checking - Chapter 1, Introduction - Part 115 minutes
Hardware and Software Bugs - Wikipedia20 minutes
Functional Verification30 minutes
Principles of Model Checking - Chapter 1, Introduction - Part 215 minutes
Principles of Model Checking - Section 1.1, 1.230 minutes
Formal Verification and Model Checking - Wikipedia30 minutes

3 devoirsTotal 30 minutes

Motivation of Verification Quiz10 minutes
Overview of Verification Quiz10 minutes
Formal Verification and Model Checking Quiz10 minutes

This module introduces transition systems, a basic modeling formalism for representing behavior of hardware and software that is suitable for automated analysis. The syntax and semantics of transition systems are explained, and how sequential circuits can be represented as transition systems is described. Next, program graphs as a formalism to model software are introduced. Syntax of program graphs is described, and semantic interpretation using transition systems is explained.

Inclus

10 vidéos3 lectures3 devoirs

10 vidéosTotal 110 minutes

Propositional Logic14 minutes
Predicate Logic9 minutes
Set Theory11 minutes
Transition Systems: Definitions13 minutes
Deterministic vs Non-Deterministic Systems8 minutes
Executions6 minutes
Modeling Sequential Circuits12 minutes
Program Graphs: Definitions10 minutes
Program Graphs: Examples16 minutes
From Program Graphs to Transition Systems12 minutes

3 lecturesTotal 135 minutes

Foundations of Logic and Set Theory - Key Concepts and Applications60 minutes
Principles of Model Checking - Section 2.1, Page 19-2945 minutes
Principles of Model Checking - Section 2.1, (Page 29-34)30 minutes

3 devoirsTotal 65 minutes

Background Quiz30 minutes
Transition Systems Quiz20 minutes
Program Graphs Quiz15 minutes

This module introduces some modeling formalisms capturing different types of system compositions. Particularly, interleaving of concurrent transition systems, compositions of systems communicating via shared variables or handshaking are explained. Additionally, synchronous parallelism is described for composing synchronous circuit composition.

Inclus

10 vidéos4 lectures4 devoirs

10 vidéosTotal 110 minutes

Concurrency and Interleaving10 minutes
Concurrency and Interleaving: Examples8 minutes
Interleaving Program Graphs12 minutes
Critical Actions and Atomicity11 minutes
Peterson's Mutual Exclusion Algorithm13 minutes
Synchronization and Handshaking13 minutes
Example: Railroad Crossing13 minutes
Synchronous Product - Part 111 minutes
Synchronous Product - Part 211 minutes
The State Space Explosion Problem9 minutes

4 lecturesTotal 110 minutes

Principles of Model Checking - Section 2.2.1, (Page 35-39)30 minutes
Principles of Model Checking - Section 2.2.2, (Page 39-47)30 minutes
Principles of Model Checking - Section 2.2.3, (Page 48-52)30 minutes
Principles of Model Checking - Section 2.2.6, (Page 73-75)20 minutes

4 devoirsTotal 65 minutes

Modeling Concurrency Using Transition Systems Quiz15 minutes
Modeling Communications Via Shared Variables Quiz20 minutes
Modeling Communications Via Handshaking Quiz10 minutes
Synchronous Parallelism Quiz20 minutes

Obtenez un certificat professionnel

Ajoutez ce titre à votre profil LinkedIn, à votre curriculum vitae ou à votre CV. Partagez-le sur les médias sociaux et dans votre évaluation des performances.

Instructeur

Hao Zheng

University of Colorado Boulder

3 Cours935 apprenants

Offert par

University of Colorado Boulder

En savoir plus sur Algorithms

Statut : Essai gratuit
University of Colorado Boulder
Temporal Logic Model Checking
Cours
Statut : Essai gratuit
University of Colorado Boulder
Fundamentals of Model Checking
Spécialisation
Statut : Prévisualisation
University of Colorado Boulder
Model Checking with SAT and SMT
Cours
Statut : Essai gratuit
University of Colorado Boulder
Verification and Synthesis of Autonomous Systems
Cours

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.’

Foire Aux Questions

To access the course materials, assignments and to earn a Certificate, you will need to purchase the Certificate experience when you enroll in a course. You can try a Free Trial instead, or apply for Financial Aid. The course may offer 'Full Course, No Certificate' instead. This option lets you see all course materials, submit required assessments, and get a final grade. This also means that you will not be able to purchase a Certificate experience.

When you enroll in the course, you get access to all of the courses in the Specialization, and you earn a certificate when you complete the work. Your electronic Certificate will be added to your Accomplishments page - from there, you can print your Certificate or add it to your LinkedIn profile.

Yes. In select learning programs, you can apply for financial aid or a scholarship if you can’t afford the enrollment fee. If fin aid or scholarship is available for your learning program selection, you’ll find a link to apply on the description page.