0

(

ratings

)

1

students

Created by:

Profile Photo

Last updated:

September 25, 2023

Duration:

Unlimited Duration

FREE

This course includes:

Unlimited Duration

Badge on Completion

Certificate of completion

Unlimited Duration

Description

Model Checking. Instructor: Prof. B. Srivathsan, Department of Computer Science, Chennai Mathematical Institute.

Embedded software controls many of the safety-critical systems that we deal with in everyday life: for instance, modern cars are equipped with software to automatically change gears; pacemakers come with a software controller to regulate heart beat; aircrafts have flight control software, and so on. Typically, these (software) controllers have to make decisions based on inputs coming from multiple interacting components. As the size and the number of interacting components increase, the design and verification of controllers becomes increasingly complex. Model checking is a field of research that addresses this challenge by making use of mathematical models in the design and verification of controllers. The main idea is to look at the system as a mathematical model - commonly used models are extensions of finite-state machines. Design requirements on the controller then get translated to suitable questions on these mathematical models. The goal of this course is to understand some of the techniques and tools used in the process of model-checking. (from nptel.ac.in)

Course Curriculum

    • Lecture 01 – Course Overview Unlimited
    • Lecture 02 – Modeling Code Behaviour Unlimited
    • Lecture 03 – Modeling Hardware Circuits Unlimited
    • Lecture 04 – Modeling Data-dependent Programs Unlimited
    • Lecture 05 – Modeling Concurrent Systems Unlimited
    • Lecture 06 – Summary Unlimited
    • Lecture 07 – Model Checking Tools Unlimited
    • Lecture 08 – Simple Models in NuSMV Unlimited
    • Lecture 09 – Hardware Verification using NuSMV Unlimited
    • Lecture 10 – Modeling Concurrent Systems in NuSMV Unlimited
    • Lecture 11 – Summary Unlimited
    • Lecture 12 – A Problem in Concurrency Unlimited
    • Lecture 13 – What is a Property? Unlimited
    • Lecture 14 – Invariants Unlimited
    • Lecture 15 – Safety Properties Unlimited
    • Lecture 16 – Liveness Properties Unlimited
    • Lecture 17 – Summary Unlimited
    • Lecture 18 – Road Map Unlimited
    • Lecture 19 – A Gentle Introduction to Automata Unlimited
    • Lecture 20 – Simple Properties of Finite Automata Unlimited
    • Lecture 21 – Safety Properties Described by Automata Unlimited
    • Lecture 22 – Summary Unlimited
    • Lecture 23 – Specifying Properties Unlimited
    • Lecture 24 – Omega-Regular Expressions Unlimited
    • Lecture 25 – Bchi Automata Unlimited
    • Lecture 26 – Simple Properties of Bchi Automata Unlimited
    • Lecture 27 – Summary Unlimited
    • Lecture 28 – Overview Unlimited
    • Lecture 29 – Omega-Regular Expressions to NBA Unlimited
    • Lecture 30 – Checking Expressions of NBA Unlimited
    • Lecture 31 – Generalized NBA Unlimited
    • Lecture 32 – Summary Unlimited
    • Lecture 33 – Introduction to LTL Unlimited
    • Lecture 34 – Semantics of LTL Unlimited
    • Lecture 35 – A Puzzle Unlimited
    • Lecture 36 – Summary Unlimited
    • Lecture 37 – Automata based LTL Model-Checking Unlimited
    • Lecture 38 – LTL to NBA Unlimited
    • Lecture 39 – Automation Construction Unlimited
    • Lecture 40 – Summary Unlimited
    • Lecture 41 – Tree View of a Transition System Unlimited
    • Lecture 42 – CTL* Unlimited
    • Lecture 43 – CTL Unlimited
    • Lecture 44 – Summary Unlimited
    • Lecture 45 – Adequate CTL Formulae Unlimited
    • Lecture 46 – EX, EU, EG Unlimited
    • Lecture 47 – Final Algorithm Unlimited
    • Lecture 48 – State-space Explosion Unlimited
    • Lecture 49 – Summary Unlimited
    • Lecture 50 – Introduction to BDDs Unlimited
    • Lecture 51 – Ordered BDDs Unlimited
    • Lecture 52 – Representing Transition Systems as OBDDs Unlimited
    • Lecture 53 – Summary Unlimited
    • Lecture 54 – Timed Transition Systems Unlimited
    • Lecture 55 – Concluding Remarks Unlimited

About the instructor

5 5

Instructor Rating

6

Reviews

4637

Courses

24151

Students

Profile Photo
OpenCoursa
We are an educational and skills marketplace to accommodate the needs of skills enhancement and free equal education across the globe to the millions. We are bringing courses and trainings every single day for our users. We welcome everyone woth all ages, all background to learn. There is so much available to learn and deliver to the people.