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 디지털이 강좌에 대하여
최근 조회 5,137회
공유 가능한 수료증
완료 시 수료증 획득
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 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 Checking9m
Computation Tree Logic11m
Computation Tree Logic Algorithm10m
Computation Tree Logic Example7m
3개 연습문제
Size of state space10m
CTL equivalence10m
CTL example10m
완료하는 데 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 tree10m
Reduced ordered decision tree10m
ROBDD10m
완료하는 데 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 120m
BDD quiz 220m
BDD algorithm30m
완료하는 데 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 rabbits8m
Deadlock checking in a network10m
Networks, BMC, conclusions10m
3개의 읽기 자료
NuSMV source of foxes and rabbits problem10m
Introduction10m
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 프로필에 수료증을 추가할 수 있습니다. 강좌 콘텐츠만 읽고 살펴보려면 해당 강좌를 무료로 청강할 수 있습니다.
환불 규정은 어떻게 되나요?
결제일 기준 2주 후 또는 (방금 시작된 강좌의 경우) 강좌의 첫 번째 세션이 시작된 후 2주 후 중에서 나중에 도래하는 날짜까지 전액 환불받을 수 있습니다. 2주 환불 기간 이내에 강좌를 완료했더라도 강좌 수료증을 받았으면 환불받을 수 없습니다. 전체 환불 정책을 확인하세요.
재정 지원을 받을 수 있나요?
예, Coursera는 수업료를 지급하기 어려운 학습자들에게 재정 지원을 제공합니다. 왼쪽의 "등록" 버튼 아래에 있는 재정 지원 링크를 클릭하면 재정 지원을 신청할 수 있습니다. 이 링크를 클릭하면 신청서를 작성하라는 메시지가 나타나며, 신청서가 승인되면 통지를 받게 됩니다. 자세히 알아보세요.
궁금한 점이 더 있으신가요? 학습자 도움말 센터를 방문해 보세요.
