This course presents how properties of acting systems and programs can be verified automatically. The basic notion is a transition system: any system that can be described by states and steps. We present how in CTL (computation tree logic) properties like reachability can be described.
Оценки: 5
от партнера
Automated Reasoning: Symbolic Model Checking
EIT DigitalОб этом курсе
Недавно просмотрено: 6,121
Сертификат, ссылками на который можно делиться с другими людьми
Получите сертификат по завершении
100% онлайн
Начните сейчас и учитесь по собственному графику.
Гибкие сроки
Назначьте сроки сдачи в соответствии со своим графиком.
Промежуточный уровень
Basic logic and programming on a bachelor level.
Прибл. 13 часов на выполнение
Английский
Субтитры: Английский
Сертификат, ссылками на который можно делиться с другими людьми
Получите сертификат по завершении
100% онлайн
Начните сейчас и учитесь по собственному графику.
Гибкие сроки
Назначьте сроки сдачи в соответствии со своим графиком.
Промежуточный уровень
Basic logic and programming on a bachelor level.
Прибл. 13 часов на выполнение
Английский
Субтитры: Английский
от партнера
EIT Digital
EIT Digital is a pan-European organization whose mission is to foster digital technology innovation and entrepreneurial talent for economic growth and quality of life. By linking education, research and business, EIT Digital empowers digital top talents for the future.
Программа курса: что вы изучите
1 ч. на завершение
CTL model checking
After a general introduction to the MOOC, this module starts by a general description of model checking.Then Computation Tree Logic (CTL) is introduced: a language in which properties on transition systems can be described. The algorithm to check whether such a property holds is given in an abstract setting, leaving implicit how sets of states are represented.
1 ч. на завершение
5 видео ((всего 44 мин.))
5 видео
Model Checking9мин
Computation Tree Logic11мин
Computation Tree Logic Algorithm10мин
Computation Tree Logic Example7мин
3 практических упражнения
Size of state space10мин
CTL equivalence10мин
CTL example10мин
1 ч. на завершение
BDDs part 1
In this module BDDs (binary decision diagrams) are introduced as decision trees with sharing. They represent boolean functions.
1 ч. на завершение
4 видео ((всего 33 мин.))
3 практических упражнения
Decision tree10мин
Reduced ordered decision tree10мин
ROBDD10мин
2 ч. на завершение
BDDs part 2
After some examples of BDD, the algorithm is presented and discussed to compute the ROBDD of any propositional formula.
2 ч. на завершение
4 видео ((всего 35 мин.))
3 практических упражнения
BDD quiz 120мин
BDD quiz 220мин
BDD algorithm30мин
9 ч. на завершение
BDD based symbolic model checking
In this last module the topics of CTL model checking and BDDs are combined: it is shown how BDDs can be used to represent sets of states in a way that the abstract algorithm for CTL mode checking can be used, and much larger state spaces can be dealt with than by using explicit state based model checking. Sever examples are presented.
9 ч. на завершение
4 видео ((всего 39 мин.)), 3 материалов для самостоятельного изучения, 3 тестов
4 видео
An example: foxes and rabbits8мин
Deadlock checking in a network10мин
Networks, BMC, conclusions10мин
3 материала для самостоятельного изучения
NuSMV source of foxes and rabbits problem10мин
Introduction10мин
Explanation packet switching networks and file describing routing function1ч 10мин
3 практических упражнения
Problem 1: colored marbles1ч
Problem 2: reaching equal values2ч
Problem 3: deadlocks in packet switching networks4ч
Часто задаваемые вопросы
Когда я получу доступ к лекциям и заданиям?
Доступ к лекциям и заданиям предоставляется в зависимости от типа регистрации. Если вы проходите курс в режиме слушателя, то получите бесплатный доступ к большинству материалов курса. Чтобы открыть оцениваемые задания и возможность получить сертификат, необходимо будет приобрести прохождение с сертификатом. Это можно сделать во время прохождения в режиме слушателя или после него. Если вы не видите варианта 'Режим слушателя'.
- Курс может не предлагаться в режиме слушателя. Попробуйте бесплатную пробную версию или подайте заявку на финансовую помощь.
- Курс предлагаться в режиме 'Полный курс, без сертификата'. В нем можно просматривать все материалы, выполнять обязательные задания и получить итоговую оценку. Приобрести дополнительно прохождение с сертификатом в таком случае нельзя.
Что я получу, оплатив сертификацию?
Оплатив сертификацию, вы получите доступ ко всем материалам курса, включая оцениваемые задания. После успешного прохождения курса на странице ваших достижений появится электронный сертификат. Оттуда его можно распечатать или прикрепить к профилю LinkedIn. Просто ознакомиться с содержанием курса можно бесплатно.
Is financial aid available?
Да, Coursera предоставляет финансовую помощь учащимся, которые не могут оплатить обучение. Чтобы подать заявление, перейдите по ссылке 'Финансовая помощь' слева под кнопкой 'Зарегистрироваться' и заполните форму. Если его примут, вы получите уведомление. Подробнее
Остались вопросы? Посетите Центр поддержки учащихся.
