When will I have access to the lectures and assignments?

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.

What will I get if I subscribe to this Specialization?

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.

Is financial aid available?

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.

Introduction to Modeling for Formal Verification

kurs ist nicht verfügbar in Deutsch (Deutschland)

Wir übersetzen es in weitere Sprachen. Sehen Sie sich die Sprachen an, die wir anbieten.

Introduction to Modeling for Formal Verification

Dieser Kurs ist Teil von Spezialisierung „Fundamentals of Model Checking“

Dozent: Hao Zheng

Bei enthalten

Mehr erfahren

3 Module

Verschaffen Sie sich einen Einblick in ein Thema und lernen Sie die Grundlagen.

11 Bewertungen

Stufe Anfänger

Empfohlene Erfahrung

1 Woche zu vervollständigen

unter 10 Stunden pro Woche

Flexibler Zeitplan

In Ihrem eigenen Lerntempo lernen

3 Module

Verschaffen Sie sich einen Einblick in ein Thema und lernen Sie die Grundlagen.

11 Bewertungen

Stufe Anfänger

Empfohlene Erfahrung

1 Woche zu vervollständigen

unter 10 Stunden pro Woche

Flexibler Zeitplan

In Ihrem eigenen Lerntempo lernen

Was Sie lernen werden

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.

Kompetenzen, die Sie erwerben

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

Werkzeuge, die Sie lernen werden

Kategorie: Software Systems

Wichtige Details

Zertifikat zur Vorlage

Zu Ihrem LinkedIn-Profil hinzufügen

Bewertungen

10 Aufgaben

Unterrichtet in Englisch

91% of learners achieved a positive career outcome

Erfahren Sie, wie Mitarbeiter führender Unternehmen gefragte Kompetenzen erwerben.

Weitere Informationen zu Coursera für Unternehmen

Logos von Petrobras, TATA, Danone, Capgemini, P&G und L'Oreal

Erweitern Sie Ihre Fachkenntnisse

Dieser Kurs ist Teil der Spezialisierung Spezialisierung „Fundamentals of Model Checking“

Wenn Sie sich für diesen Kurs anmelden, werden Sie auch für diese Spezialisierung angemeldet.

Lernen Sie neue Konzepte von Branchenexperten
Gewinnen Sie ein Grundverständnis bestimmter Themen oder Tools
Erwerben Sie berufsrelevante Kompetenzen durch praktische Projekte
Erwerben Sie ein Berufszertifikat zur Vorlage

In diesem Kurs gibt es 3 Module

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.

Moduldetails

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.

Das ist alles enthalten

7 Videos8 Lektüren3 Aufgaben

7 VideosInsgesamt 53 Minuten

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

8 LektürenInsgesamt 151 Minuten

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

3 AufgabenInsgesamt 30 Minuten

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

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.

Das ist alles enthalten

10 Videos3 Lektüren3 Aufgaben

10 VideosInsgesamt 110 Minuten

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

3 LektürenInsgesamt 135 Minuten

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

3 AufgabenInsgesamt 65 Minuten

Background Quiz30 Minuten
Transition Systems Quiz20 Minuten
Program Graphs Quiz15 Minuten

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.