Chevron Left
Quantitative Model Checking(으)로 돌아가기

EIT 디지털 의 Quantitative Model Checking 학습자 리뷰 및 피드백

51개의 평가

강좌 소개

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....
필터링 기준:

Quantitative Model Checking의 7개 리뷰 중 1~7

교육 기관: ElissaHu

2018년 4월 27일

difficult in week4&week5, but interesting

교육 기관: Carl H

2019년 2월 1일

Lectures are rushed and not explained well. Discussion forms seem to be filled with "Is there inaccuracy in in quiz X". Here is a direct quote from one of the discussions "I actually didn't use the formula from the lecture but from the cited paper by Baier et. al. - same stuff. works for 11, doesn't for 12". Granted that the subject matter this course covers is difficult, I feel like this course makes it harder rather than easier. I wouldn't recommend it to anyone.

교육 기관: Joseph V

2018년 1월 19일

The lectures on Coursera are nice, but please remove to cringe parts (any outside shot video material).

Overall the course is very bad because the tele lectures are very bad quality and thus does not motivate you at all to keep track of the course during the period. Recommendation: Ditch tele lectures all together and give actual bonus points for completing Coursera parts on time.

교육 기관: 潘临杰

2017년 8월 24일


교육 기관: Mario G S

2017년 9월 16일

Very good course!!!

교육 기관: Алина Г

2022년 3월 21일

Some quizs have a mistakes and typos.

No useful example for quiz in the last week.

교육 기관: Hao L

2020년 6월 1일

I can tell the course team did put a lot of time and energy to make this course and I am thankful for that. I have also learned a lot through this course. However, the defects make the abstract course even harder to follow: mistakes are not rare thorough the whole course; lacking involvement in the discussion forum from the team and the illustration can be sometimes hard to understand. Prepare to suffer if you want to learn this course along especially without any previous background (time consumption should be expected to be ~5hours/week).