Coursera
探索
  • 浏览
  • 搜索
  • 企业版
  • 登录
  • 注册

Quantitative Model Checking

总览授课大纲常见问题解答制作方评分和审阅

主页计算机科学软件开发

Quantitative Model Checking

EIT 数字

关于此课程: The integration of ICT (information and communications technology) in different applications is rapidly increasing in e.g. Embedded and Cyber physical systems, Communication protocols and Transportation systems. Hence, their reliability and dependability increasingly depends on software. Defects can be fatal and extremely costly (with regards to mass-production of products and safety-critical systems). First, a model of the real system has to be built. In the simplest case, the model reflects all possible states that the system can reach and all possible transitions between states in a (labelled) State Transition System. When adding probabilities and discrete time to the model, we are dealing with so-called Discrete-time Markov chains which in turn can be extended with continuous timing to Continuous-time Markov chains. Both formalisms have been used widely for modeling and performance and dependability evaluation of computer and communication systems in a wide variety of domains. These formalisms are well understood, mathematically attractive while at the same time flexible enough to model complex systems. Model checking focuses on the qualitative evaluation of the model. As formal verification method, model checking analyzes the functionality of the system model. A property that needs to be analyzed has to be specified in a logic with consistent syntax and semantics. For every state of the model, it is then checked whether the property is valid or not. The main focus of this course is on quantitative model checking for Markov chains, for which we will discuss efficient computational algorithms. The learning objectives of this course are as follows: - Express dependability properties for different kinds of transition systems . - Compute the evolution over time for Markov chains. - Check whether single states satisfy a certain formula and compute the satisfaction set for properties.

此课程适用人群: This course is meant for Master students in Computer Science, Electrical Engineering and Embedded Systems as a specialisation in the area of formal models and methods. Note that as a consequence, quiz questions are more like exam questions where you have to construct the answer based on the principles that are taught in the web lectures, rather than to recall the literal text of the teacher.


制作方:  EIT 数字
EIT 数字

  • Anne Remke

    教学方:  Anne Remke, Prof. dr.

    Computer Science
级别Intermediate
承诺学习时间5 weeks of study, each with around 2.h hours work
语言
English
如何通过通过所有计分作业以完成课程。
用户评分
4.1 星
平均用户评分 4.1查看学生的留言
授课大纲
第 1 周
Module 1: Computational Tree Logic
We introduce Labeled Transition Systems (LTS), the syntax and semantics of Computational Tree Logic (CTL) and discuss the model checking algorithms that are necessary to compute the satisfaction set for specific CTL formulas.
6 视频, 3 阅读材料, 1 练习测试
  1. 视频: Welcome!
  2. 视频: Introduction
  3. Leyendo: Script 1 and 2.1
  4. 视频: Semantics of CTL
  5. Leyendo: Script 2.2 and 2.3
  6. 视频: Model Checking CTL
  7. 视频: The Until Operator
  8. Cuestionario de práctica: Check your understanding of CTL
  9. 视频: The Always Operator
  10. Leyendo: Script 2.4
已评分: Formulate for yourself
已评分: Test your understanding of CTL semantics
已评分: Model checking eventually, always and until
第 2 周
Discrete Time Markov Chains
We enhance transition systems by discrete time and add probabilities to transitions to model probabilistic choices. We discuss important properties of DTMCs, such as the memoryless property and time-homogeneity. State classification can be used to determine the existence of the limiting and / or stationary distribution.
5 视频, 2 阅读材料, 2 练习测试
  1. 视频: Introduction to DTMCs
  2. Leyendo: Script 3.1 and 3.2
  3. 视频: Evolution in Time
  4. Cuestionario de práctica: Evolution of DTMCs
  5. 视频: Transient probabilities
  6. 视频: State classification
  7. Leyendo: Script 3.3
  8. Cuestionario de práctica: Classification of DTMC states True or False?
  9. 视频: Steady-state probabilities
已评分: Compute transient probabilities
已评分: State classification
已评分: Steady-state computation
第 3 周
Probabilistic Computational Tree Logic
We discuss the syntax and semantics of Probabilistic Computational Tree logic and check out the model checking algorithms that are necessary to decide the validity of different kinds of PCTL formulas. We shortly discuss the complexity of PCTL model checking.
5 视频, 3 阅读材料, 3 练习测试
  1. 视频: Syntax of PCTL
  2. Cuestionario de práctica: PCTL Syntax
  3. 视频: Model checking and the Next operator
  4. Leyendo: Script: 4.1 and 4.2
  5. 视频: Time-bounded Until
  6. Cuestionario de práctica: Test your understanding of PCTL Until
  7. 视频: Backwards computation
  8. Leyendo: Script: 4.3.1 and 4.3.2
  9. 视频: Unbounded Until
  10. Leyendo: Script 4.3.3
  11. Cuestionario de práctica: Test your understanding of PCTL
已评分: Checking PCTL next
已评分: Checking time-bounded until
已评分: Checking unbounded until
第 4 周
Continuous Time Markov Chains
We enhance Discrete-Time Markov Chains with real time and discuss how the resulting modelling formalism evolves over time. We compute the steady-state for different kinds of CMTCs and discuss how the transient probabilities can be efficiently computed using a method called uniformisation.
5 视频, 2 阅读材料, 3 练习测试
  1. 视频: Definition of a CTMC
  2. Leyendo: Script: 5.1 and 5.2
  3. 视频: Generator matrix
  4. Cuestionario de práctica: Test your understanding of CTMCs
  5. 视频: Steady-state probabilities
  6. Cuestionario de práctica: Steady state probability in CTMCs
  7. 视频: Triple Modular Redundancy
  8. Leyendo: Script: 5.3
  9. 视频: Uniformisation
  10. Cuestionario de práctica: Test your understanding of Uniformisation
已评分: Generator matrix
已评分: Identifying BSCCs
已评分: Uniformisation
第 5 周
Continuous Stochastic Logic
We introduce the syntax and semantics of Continuous Stochastic Logic and describe how the different kinds of CSL formulas can be model checked. Especially, model checking the time bounded until operator requires applying the concept of uniformisation, which we have discussed in the previous module.
5 视频, 2 阅读材料, 3 练习测试
  1. 视频: Model checking CSL
  2. 视频: Model checking and Time-bounded next
  3. Leyendo: Script: 6.1
  4. Cuestionario de práctica: Test your understanding of CSL (I)
  5. 视频: Model checking the steady-state operator
  6. Cuestionario de práctica: Test your understanding of CSL (II)
  7. Leyendo: Script: 6.2
  8. 视频: Time-bounded Until
  9. Cuestionario de práctica: Test your understanding of CSL (III)
  10. 视频: An application
已评分: Assembly line
已评分: Steady state and next
已评分: Time bounded until in CSL

常见问题解答
运作方式
Trabajo del curso
Trabajo del curso

Cada curso es como un libro de texto interactivo, con videos pregrabados, cuestionarios y proyectos.

Ayuda de tus compañeros
Ayuda de tus compañeros

Conéctate con miles de estudiantes y debate ideas y materiales del curso, y obtén ayuda para dominar los conceptos.

Certificados
Certificados

Obtén reconocimiento oficial por tu trabajo y comparte tu éxito con amigos, compañeros y empleadores.

制作方
EIT 数字
EIT Digital is a pan-European education and research-based open innovation organization founded on excellence. Its 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. EIT Digital provides online "blended" Innovation and Entrepreneurship education to raise quality, increase diversity and availability of the top-level content provided by 20 reputable universities of technology around Europe. The universities all together deliver a unique blend of the best of technical excellence and entrepreneurial skills and mindset to digital engineers and entrepreneurs at all stages of their careers. The academic partners support Coursera’s bold vision to enable anyone, anywhere, to transform their lives by accessing the world’s best learning experience. This means that EIT Digital gradually shares parts of its entrepreneurial and academic education programmes to demonstrate its excellence and make it accessible to a much wider audience. EIT Digital’s online education portfolio can be used as part of blended education settings, in both Master and Doctorate programmes, and for professionals as a way to update their knowledge. EIT Digital offers an online programme in 'Internet of Things through Embedded Systems'. Achieving all certificates of the online courses and the specialization provides an opportunity to enroll in the on campus program and get a double degree. These are the courses in the online programme:
评分和审阅
已评分 4.1,总共 5 个 18 评分

MS

Very good course!!!

潘

模型检测入门教程,学完课程之后对于模型检测有了直观的认识。



您可能也喜欢
EIT 数字
System Validation (2): Model process behaviour
1 门课程
EIT 数字
System Validation (2): Model process behaviour
查看课程
EIT 数字
System Validation (3): Requirements by modal formulas
1 门课程
EIT 数字
System Validation (3): Requirements by modal formulas
查看课程
EIT 数字
System Validation (4): Modelling Software, Protocols, and other behaviour
1 门课程
EIT 数字
System Validation (4): Modelling Software, Protocols, and other behaviour
查看课程
EIT 数字
System Validation: Automata and behavioural equivalences
1 门课程
EIT 数字
System Validation: Automata and behavioural equivalences
查看课程
EIT 数字
Quantitative Formal Modeling and Worst-Case Performance Analysis
1 门课程
EIT 数字
Quantitative Formal Modeling and Worst-Case Performance Analysis
查看课程
Coursera
Coursera 致力于普及全世界最好的教育,它与全球一流大学和机构合作提供在线课程。
© 2018 Coursera Inc. 保留所有权利。
通过 App Store 下载通过 Google Play 获取
  • Coursera
  • 关于
  • 管理团队
  • 工作机会
  • 目录
  • 证书
  • 学位
  • 商务
  • 政府版
  • 社区
  • 合作伙伴
  • 社区助教
  • 专业译员
  • 开发者
  • Beta 测试人员
  • 连接
  • 博客
  • Facebook
  • 领英
  • Twitter
  • Google+
  • 技术博客
  • 更多
  • 条款
  • 隐私
  • 帮助
  • 内容访问
  • 媒体
  • 联系我们
  • 目录
  • 附属公司