Temporal Logic Model Checking

Temporal Logic Model Checking

本课程是 Fundamentals of Model Checking 专项课程的一部分

位教师：Hao Zheng

访问权限由 Coursera Learning Team 提供

4个模块

深入了解一个主题并学习基础知识。

初级等级

推荐体验

5 周完成

在 10 小时一周

灵活的计划

自行安排学习进度

4个模块

深入了解一个主题并学习基础知识。

初级等级

推荐体验

5 周完成

在 10 小时一周

灵活的计划

自行安排学习进度

您将学到什么

Identify linear time behavior and specify linear time properties using linear time logic (LTL)
Describe basic concepts of LTL model checking
Specify properties using computation tree logic (CTL)
Describe basic concepts of CTL model checking and its symbolic version

您将获得的技能

要了解的详细信息

可分享的证书

添加到您的领英档案

作业

11 项作业

授课语言：英语（English）

了解顶级公司的员工如何掌握热门技能

了解关于 Coursera for Business 的更多信息

Petrobras, TATA, Danone, Capgemini, P&G 和 L'Oreal 的徽标

积累特定领域的专业知识

本课程是 Fundamentals of Model Checking 专项课程专项课程的一部分

在注册此课程时，您还会同时注册此专项课程。

向行业专家学习新概念
获得对主题或工具的基础理解
通过实践项目培养工作相关技能
获得可共享的职业证书

该课程共有4个模块

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 concepts of linear-time interpretation of transition systems, and shows how to specify various types of properties on the linear-time behavior.

涵盖的内容

13个视频5篇阅读材料3个作业

13个视频总计130分钟

Deadlock 12分钟
Linear Time Behavior 13分钟
Linear Time Properties 17分钟
Basic Concepts of Invariant Properties 5分钟
Algorithms for Checking Invariant Properties 12分钟
Safety Properties 10分钟
Trace Equivalence and Safety Properties 6分钟
Liveness Properties 15分钟
Checking Liveness Properties - Illustration 11分钟
Safety Vs Liveness 5分钟
Concepts of Fairness 8分钟
Fairness Constraints 9分钟
Fair Satisfaction of LT Properties 9分钟

5篇阅读材料总计61分钟

Course Updates and Accessibility Support 1分钟
Non-Credit Students: Welcome and Where to Find Help 10分钟
Principles of Model Checking - Section 3.2 20分钟
Principles of Model Checking - Section 3.3 15分钟
Principles of Model Checking - Sections 3.4, 3.5.1 15分钟

3个作业总计65分钟

Linear Time Behavior and Properties 25分钟
Safety Properties and Invariants 20分钟
Liveness Properties and Fairness 20分钟

This module introduces linear-time logic (LTL) for specifying linear-time properties and framework for deciding truth of LTL formulas with respect to transition systems.

涵盖的内容

26个视频3篇阅读材料3个作业

26个视频总计289分钟

Linear Time Logic (LTL): Syntax 18分钟
Semantics of LTL 10分钟
Satisfaction of LTL on Transition Systems 13分钟
Semantics of Negation 6分钟
Equivalence of LTL Formulas 17分钟
Positive Normal Form 13分钟
Fairness in LTL 11分钟
Overview of LTL Model Checking 9分钟
Non-Deterministic Buchi Automata (NBA) 10分钟
Generalize NBA (GNBA) 7分钟
GNBA to NBA 10分钟
Persistency Checking - Concepts 7分钟
Persistency Checking - Example 12分钟
Closure & Elementary Sets 14分钟
Translating LTL Formulas to NBA 17分钟
A Tutorial on SPIN 8分钟
Overview of Promela 9分钟
Process Structure 9分钟
Promela Statements - Part 1 10分钟
Promela Statements - Part 2 12分钟
Promela Statements - Part 3 8分钟
Operational Semantics - Part 1 10分钟
Operational Semantics - Part 2 7分钟
Communication Models 18分钟
Overview of SPIN Model Checker 12分钟
Property Specifications 12分钟

3篇阅读材料总计60分钟

Principles of Model Checking - Section 5.1 20分钟
Principles of Model Checking - Sections 4.3, 4.4, 5.2 30分钟
Online SPIN Tutorial 10分钟

3个作业总计125分钟

Linear Time Logic: Syntax and Semantics 30分钟
LTL Model Checking 35分钟
Getting Familiar with SPIN 60分钟

This module introduces computation tree logic (CTL) for specifying properties and model checking algorithms for deciding truth of CTL formulas with respect to transition systems.

涵盖的内容

13个视频3篇阅读材料3个作业

13个视频总计148分钟

Introduction to Computation Tree Logic 9分钟
CTL Syntax 11分钟
CTL Semantics 13分钟
CTL Equivalence and Normal Forms 10分钟
Expressiveness of CTL Vs LTL 14分钟
Introduction to CTL Model Checking 8分钟
Computing the Satisfaction Sets of CTL Formulas - Part 1 10分钟
Computing the Satisfaction Sets of CTL Formulas - Part 2 10分钟
Fairness in CTL 8分钟
CTL Model Checking with Fairness 11分钟
Counterexamples and Witnesses 19分钟
Generation of Counterexamples and Witnesses 17分钟
Counterexamples and Witnesses with Fairness 7分钟

3篇阅读材料总计60分钟

Principles of Model Checking - Sections 6.1, 6.2, 6.3 20分钟
Principles of Model Checking - Sections 6.4, 6.5 30分钟
Principles of Model Checking - Section 6.6 10分钟

3个作业总计100分钟

Computational Tree Logic 50分钟
CTL Model Checking 30分钟
Counterexamples and Witnesses 20分钟

This module introduces basic concepts of symbolic model checking, how transition systems can be encoded as switch functions, mode checking algorithms based on switch functions, and BDDs as a compact representation of switch functions.

涵盖的内容

16个视频3篇阅读材料2个作业1次同伴评审

16个视频总计181分钟

Introduction to Symbolic CTL Model Checking 16分钟
Symbolic Encoding of Transition Systems 8分钟
Symbolic Encoding of Transition Systems - An Example 5分钟
Symbolic Composition of Transition Systems 8分钟
Symbolic Image Computation 11分钟
Symbolic Preimage Computation 11分钟
Symbolic Computation for Existential Until and Existential Always Operators 14分钟
Symbolic Model Checking - An Example 9分钟
Overview of Switching Function Representations 18分钟
Constructing Reduced OBDDs 8分钟
Considerations of ROBDDs 7分钟
Variable Ordering Problem 7分钟
Boolean Operations in OBDDs 12分钟
NuSMV Overview 16分钟
Modeling in NuSMV 13分钟
Uses of NuSMV 17分钟