К содержимому
learnspaceYOUR NEXT CHAPTER
ПРОСТРАНСТВО ОБУЧЕНИЯ
ГлавнаяКаталог курсовМоё обучениеCoursera

Знания без границ

Учитесь у лучших университетов и компаний мира.

Открыть Coursera
Интеграция
Пространство университета
Моё пространствоСтраница курса
↵
ЯЛичный кабинетСтудент
© 2026 LearnSpaceКаждый день — возможность узнать больше.Помощь
Temporal Logic Model Checking · LearnSpace
Назад в каталог
courseraПрограммирование

Temporal Logic Model Checking

Курс от University of Colorado Boulder
Начальный≈ 45.7 чАнглийский
О курсеНавыкиПрограммаПреподаватели

О курсе

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 course can also be taken for academic credit as ECEA ####, part of CU Boulder’s Master of Science in Electrical Engineering.

Навыки, которые вы освоите

Computational LogicTheoretical Computer ScienceSafety and SecurityVerification And ValidationAlgorithmsTest ToolsCommunication SystemsSystems DesignProcess ModelingFunctional Specification

Программа курса

4 модулей · 94 учебных материалов

01Linear Time Properties21 материалов

Linear Time Behavior and Properties

Course Updates and Accessibility SupportЧтениеNon-Credit Students: Welcome and Where to Find HelpЧтениеDeadlockВидеоLinear Time BehaviorВидео

Учитесь у экспертов

Hao Zheng

Преподаватель курса

Temporal Logic Model Checking
В каталоге вашей программы

Инвестируйте в себя

Новые знания — в удобное для вас время.

Начать на Coursera

Обучение откроется на Coursera
в новой вкладке

Обучение на Coursera

≈ 45.7 ч

4 модулей

Язык: Английский

Субтитры: Узбекский, Казахский

Часть программы вашего университета
Linear Time PropertiesВидео
Principles of Model Checking - Section 3.2Чтение
Linear Time Behavior and PropertiesЗадание

Safety Properties and Invariants

Basic Concepts of Invariant PropertiesВидеоAlgorithms for Checking Invariant PropertiesВидеоSafety PropertiesВидеоTrace Equivalence and Safety PropertiesВидеоPrinciples of Model Checking - Section 3.3ЧтениеSafety Properties and InvariantsЗадание

Liveness Properties and Fairness

Liveness PropertiesВидеоChecking Liveness Properties - IllustrationВидеоSafety Vs LivenessВидеоConcepts of FairnessВидеоFairness ConstraintsВидеоFair Satisfaction of LT PropertiesВидеоPrinciples of Model Checking - Sections 3.4, 3.5.1ЧтениеLiveness Properties and FairnessЗадание
02Linear Time Logic32 материалов

Linear Time Logic (LTL): Syntax and Semantics

Linear Time Logic (LTL): SyntaxВидеоSemantics of LTLВидеоSatisfaction of LTL on Transition SystemsВидеоSemantics of NegationВидеоEquivalence of LTL FormulasВидеоPositive Normal FormВидеоFairness in LTLВидеоPrinciples of Model Checking - Section 5.1ЧтениеLinear Time Logic: Syntax and SemanticsЗадание

LTL Model Checking

Overview of LTL Model CheckingВидеоNon-Deterministic Buchi Automata (NBA)ВидеоGeneralize NBA (GNBA)​ВидеоGNBA to NBAВидеоPersistency Checking - ConceptsВидеоPersistency Checking - ExampleВидео

SPIN Model Checker

A Tutorial on SPINВидеоOverview of PromelaВидеоProcess StructureВидеоPromela Statements - Part 1ВидеоPromela Statements - Part 2ВидеоPromela Statements - Part 3ВидеоOperational Semantics - Part 1
03Computation Tree Logic19 материалов

Computational Tree Logic

Introduction to Computation Tree LogicВидеоCTL SyntaxВидеоCTL SemanticsВидеоCTL Equivalence and Normal FormsВидеоExpressiveness of CTL Vs LTLВидеоPrinciples of Model Checking - Sections 6.1, 6.2, 6.3ЧтениеComputational Tree LogicЗадание

CTL Model Checking

Introduction to CTL Model CheckingВидеоComputing the Satisfaction Sets of CTL Formulas - Part 1ВидеоComputing the Satisfaction Sets of CTL Formulas - Part 2ВидеоFairness in CTLВидеоCTL Model Checking with FairnessВидеоPrinciples of Model Checking - Sections 6.4, 6.5Чтение

Counterexamples and Witnesses

Counterexamples and WitnessesВидеоGeneration of Counterexamples and WitnessesВидеоCounterexamples and Witnesses with FairnessВидеоPrinciples of Model Checking - Section 6.6ЧтениеCounterexamples and WitnessesЗадание
04Symbolic CTL Model Checking22 материалов

Symbolic Representation of Transition Systems

Introduction to Symbolic CTL Model CheckingВидеоSymbolic Encoding of Transition SystemsВидеоSymbolic Encoding of Transition Systems - An ExampleВидеоSymbolic Composition of Transition SystemsВидеоSymbolic Image ComputationВидеоSymbolic Preimage ComputationВидеоSymbolic Computation for Existential Until and Existential Always OperatorsВидеоSymbolic Model Checking - An ExampleВидеоPrinciples of Model Checking - Section 6.7, (Page 382-392)ЧтениеSymbolic Representation of Transition SystemsЗадание

Ordered Binary Decision Diagrams

Overview of Switching Function RepresentationsВидеоConstructing Reduced OBDDsВидеоConsiderations of ROBDDsВидеоVariable Ordering ProblemВидеоBoolean Operations in OBDDsВидеоPrinciples of Model Checking - Section 6.7, (Page 392-407)Чтение

Symbolic Model Checker NuSMV

NuSMV OverviewВидеоModeling in NuSMVВидеоUses of NuSMVВидеоNuSMV TutorialЧтениеBecoming Familiar with NuSMVВзаимная проверка
Closure & Elementary SetsВидео
Translating LTL Formulas to NBAВидео
Principles of Model Checking - Sections 4.3, 4.4, 5.2Чтение
LTL Model CheckingЗадание
Видео
Operational Semantics - Part 2Видео
Communication ModelsВидео
Overview of SPIN Model CheckerВидео
Property SpecificationsВидео
Online SPIN TutorialЧтение
Getting Familiar with SPINЗадание
CTL Model CheckingЗадание
Ordered Binary Decision DiagramsЗадание