Monthly Subscription Starting at AED 99 + VAT

Quantitative Model Checking
  • Level Professional
  • المدة 18 ساعات hours
  • الطبع بواسطة EIT Digital
  • Offered by

عن

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.

الوحدات

Lecture 1: Introduction

    • 2 Videos
    • 1 Readings
    • 1 Assignment
Show info about module content

1 Assignment

  • Formulate for yourself

2 Videos

  • Welcome!
  • Introduction

1 Readings

  • Script 1 and 2.1

Lecture 2: Semantics of CTL

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • Semantics of CTL

1 Readings

  • Script 2.2 and 2.3

Lecture 3: Model Checking CTL

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Test your understanding of CTL semantics

1 Videos

  • Model Checking CTL

Lecture 4: The Until Operator

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Check your understanding of CTL

1 Videos

  • The Until Operator

Lecture 5: The Always Operator

    • 1 Videos
    • 1 Readings
    • 1 Assignment
Show info about module content

1 Assignment

  • Model checking eventually, always and until

1 Videos

  • The Always Operator

1 Readings

  • Script 2.4

Lecture 1: Introduction to DTMCs

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • Introduction to DTMCs

1 Readings

  • Script 3.1 and 3.2

Lecture 2: Evolution in Time

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Evolution of DTMCs

1 Videos

  • Evolution in Time

Lecture 3: Transient probabilities

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Compute transient probabilities

1 Videos

  • Transient probabilities

Lecture 4: State classification

    • 1 Videos
    • 1 Readings
    • 1 Assignment
Show info about module content

1 Assignment

  • Classification of DTMC states True or False?

1 Videos

  • State classification

1 Readings

  • Script 3.3

Lecture 5: Steady-state probabilities

    • 1 Videos
    • 2 Assignment
Show info about module content

2 Assignment

  • State classification
  • Steady-state computation

1 Videos

  • Steady-state probabilities

Lecture 1: Syntax of PCTL

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • PCTL Syntax

1 Videos

  • Syntax of PCTL

Lecture 2: Model checking and the Next operator

    • 1 Videos
    • 1 Readings
    • 1 Assignment
Show info about module content

1 Assignment

  • Checking PCTL next

1 Videos

  • Model checking and the Next operator

1 Readings

  • Script: 4.1 and 4.2

Lecture 3: Time-bounded Until

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Test your understanding of PCTL Until

1 Videos

  • Time-bounded Until

Lecture 4: Backwards computation

    • 1 Videos
    • 1 Readings
    • 1 Assignment
Show info about module content

1 Assignment

  • Checking time-bounded until

1 Videos

  • Backwards computation

1 Readings

  • Script: 4.3.1 and 4.3.2

Lecture 5: Unbounded Until

    • 1 Videos
    • 1 Readings
    • 2 Assignment
Show info about module content

2 Assignment

  • Checking unbounded until
  • Test your understanding of PCTL

1 Videos

  • Unbounded Until

1 Readings

  • Script 4.3.3

Lecture 1: Definition of a CTMC

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • Definition of a CTMC

1 Readings

  • Script: 5.1 and 5.2

Lecture 2: Generator matrix

    • 1 Videos
    • 2 Assignment
Show info about module content

2 Assignment

  • Generator matrix
  • Test your understanding of CTMCs

1 Videos

  • Generator matrix

Lecture 3: Steady-state probabilities

    • 1 Videos
    • 2 Assignment
Show info about module content

2 Assignment

  • Steady state probability in CTMCs
  • Identifying BSCCs

1 Videos

  • Steady-state probabilities

Lecture 4: Example - Triple Modular Redundancy

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • Triple Modular Redundancy

1 Readings

  • Script: 5.3

Lecture 5: Uniformization

    • 1 Videos
    • 2 Assignment
Show info about module content

2 Assignment

  • Test your understanding of Uniformisation
  • Uniformisation

1 Videos

  • Uniformisation

Lecture 1: Syntax and semantics

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Assembly line

1 Videos

  • Model checking CSL

Lecture 2: Time-bounded next

    • 1 Videos
    • 1 Readings
    • 1 Assignment
Show info about module content

1 Assignment

  • Test your understanding of CSL (I)

1 Videos

  • Model checking and Time-bounded next

1 Readings

  • Script: 6.1

Lecture 3: Steady-state

    • 1 Videos
    • 2 Assignment
Show info about module content

2 Assignment

  • Steady state and next
  • Test your understanding of CSL (II)

1 Videos

  • Model checking the steady-state operator

Lecture 4: Time-bounded Until

    • 1 Videos
    • 1 Readings
    • 2 Assignment
Show info about module content

2 Assignment

  • Time bounded until in CSL
  • Test your understanding of CSL (III)

1 Videos

  • Time-bounded Until

1 Readings

  • Script: 6.2

Lecture 5: An application

    • 1 Videos
Show info about module content

1 Videos

  • An application

Auto Summary

Dive into the world of quantitative model checking with this comprehensive course designed for IT and computer science professionals. As the integration of ICT in embedded systems, communication protocols, and transportation systems grows, the reliability of software becomes paramount. This course, led by experienced instructors on Coursera, focuses on building and analyzing models of real systems to ensure dependability and performance. Learners will explore the creation of state transition systems and delve into Discrete-time and Continuous-time Markov chains, essential for modeling complex systems. The course emphasizes the qualitative evaluation of these models through formal verification methods. Key learning objectives include expressing dependability properties for various transition systems, computing the evolution of Markov chains over time, and verifying state properties. Spanning 1080 minutes, this professional-level course offers a deep dive into efficient computational algorithms for quantitative model checking. Subscriptions are available under the Starter plan, making it accessible for those looking to enhance their expertise in this critical area of IT and computer science. Ideal for professionals seeking to bolster their skills in software reliability and dependability, this course provides the tools and knowledge needed to excel in the field.

Anne Remke
Instructor

Anne Remke