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.
제공자:
Automated Reasoning: Symbolic Model Checking
EIT 디지털이 강좌에 대하여
최근 조회 3,019회
유연한 마감일
일정에 따라 마감일을 재설정합니다.
공유 가능한 수료증
완료 시 수료증 획득
100% 온라인
지금 바로 시작해 나만의 일정에 따라 학습을 진행하세요.
중급 단계
Basic logic and programming on a bachelor level.
완료하는 데 약 13시간 필요
영어
자막: 영어
유연한 마감일
일정에 따라 마감일을 재설정합니다.
공유 가능한 수료증
완료 시 수료증 획득
100% 온라인
지금 바로 시작해 나만의 일정에 따라 학습을 진행하세요.
중급 단계
Basic logic and programming on a bachelor level.
완료하는 데 약 13시간 필요
영어
자막: 영어
제공자:
EIT 디지털
EIT Digital is a European education and innovation organisation with a mission 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분)
완료하는 데 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분)
완료하는 데 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분)
완료하는 데 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 개의 테스트
자주 묻는 질문
강의 및 과제를 언제 이용할 수 있게 되나요?
이 수료증을 구매하면 무엇을 이용할 수 있나요?
재정 지원을 받을 수 있나요?
궁금한 점이 더 있으신가요? 학습자 도움말 센터를 방문해 보세요.
