К содержимому
learnspaceYOUR NEXT CHAPTER
ПРОСТРАНСТВО ОБУЧЕНИЯ
ГлавнаяКаталог курсовМоё обучениеCoursera

Знания без границ

Учитесь у лучших университетов и компаний мира.

Открыть Coursera
Интеграция
Пространство университета
Моё пространствоСтраница курса
↵
ЯЛичный кабинетСтудент
© 2026 LearnSpaceКаждый день — возможность узнать больше.Помощь
Quantitative Formal Modeling and Worst-Case Performance Analysis · LearnSpace
Назад в каталог
courseraПрограммирование

Quantitative Formal Modeling and Worst-Case Performance Analysis

Курс от 28DIGITAL
Продвинутый≈ 17.4 чАнглийский
О курсеНавыкиПрограммаПреподаватели

О курсе

Welcome to "Quantitative Formal Modeling and Worst-Case Performance Analysis," an intellectually stimulating course designed to hone your abstract thinking skills in the realm of theoretical computer science. This course invites you to dive deep into the world of token production and consumption, a foundational approach to system behaviour. Master the art of mathematically formalizing these concepts through prefix orders and counting functions. Get hands-on with Petri-nets, explore the nuances of timing, and delve into the scheduling intricacies of token systems. You'll even learn to conduct worst-case performance analysis on single-rate dataflow graphs, examining key metrics like throughput, latency, and buffering. Why the focus on small examples rather than industrial-size systems? The aim here is twofold: First, we strive to cultivate your ability to think abstractly and mathematically about modelling and performance—a vital skill for tackling any future challenges in this field. Second, while dataflow techniques are indeed industry-applicable, this course serves as an essential primer that focuses on single-rate dataflow, the cornerstone of more advanced dataflow techniques. And here's a bonus: this course forms part of the esteemed Quantitative Evaluation of Embedded Systems (QEES) curriculum offered under the aegis of the EIT-Digital University and the Dutch 3TU consortium. While the examination for QEES is more advanced, this course perfectly mirrors its initial three-week content, offering you a robust academic experience online. Ready to sharpen your abstract thinking and delve into the fascinating world of formal modelling? Enroll now to secure your spot.

Навыки, которые вы освоите

Graph TheoryModel Evaluation

Программа курса

5 модулей · 79 учебных материалов

01Introduction2 материалов

Introduction

IntroductionВидеоSome suggested reading materialЧтение
02Modeling systems as token consumption/production systems20 материалов

Drawing consumption/production models

A single picture tells more than a thousand wordsВидео

Учитесь у экспертов

Dr.ir. Pieter Cuijpers

Assistant Professor

Anne Remke

Prof. dr.

Quantitative Formal Modeling and Worst-Case Performance Analysis
В каталоге вашей программы

Инвестируйте в себя

Новые знания — в удобное для вас время.

Начать на Coursera

Обучение откроется на Coursera
в новой вкладке

Обучение на Coursera

≈ 17.4 ч

5 модулей

Язык: Английский

Субтитры: Арабский, Французский, Украинский, Китайский (Китай), Греческий, Итальянский, Бразильский португальский, Нидерландский, Корейский, Немецкий, Русский, Тайский, Индонезийский, Шведский, Турецкий, Испанский, Хинди, Японский, Казахский, Польский

Часть программы вашего университета
Consumption and production of tokensВидео
Always ask yourself...Чтение
Modeling an intensive care unitВидео
Modeling a wireless LAN radioВидео
Modeling and refining an industrial robotВидео
Basic modeling ideasЗадание
Modeling Warehouse 13Задание
Pick your own systemВидео

Petri-nets and dataflow graphs

Classes of Petri-netsВидеоCausality, choice and concurrency (modeling patterns)ВидеоModeling featuresЗадание

Refinement

Refinement of consumption/production systemsВидеоThe refinement of the robot.ЧтениеDefinition of refinementЗаданиеWhich is a refinement of which?ЗаданиеInterpreting pictures for performance analysisВидео

A peer-reviewed modeling assignment

Draw your own modelВидеоDraw your own modelВзаимная проверкаToolingЧтение
03Syntax and semantics24 материалов

Warning: prepare for some set theory!

Warning: prepare for some set theory!ВидеоFlags and Fitch style proofsЧтение

Syntax and semantics

Syntax and semanticsВидео

Formalizing pictures as bipartite graphs

The basicsВидеоExtensionsВидеоBipartite graphsЗадание

Formalizing behaviors as a prefix orders

Prefix ordersВидеоExercise on prefix ordersВидеоProof that flows form a prefix orderВидеоSlides of the proofЧтение

Formalizing interpretations as functions

Formalizing interpretations as functionsВидеоCounting is order preservingВидеоThinking about observation functionsЗаданиеIsomorphismЗадание

Formalizing the Petri-nets interpretation

Formalizing the Petri-net interpretationВидеоProof that the number of tokens in a single-rate dataflow cycle is constantВидеоSlides of the proofЧтениеSummarize!Задание

Formalizing time and scheduling

Formalizing timingВидеоExercise: Formalize best-case response timesЧтениеFormalizing eager schedulingВидеоFormalizing periodic schedulingВидеоAbout the next quiz.ЧтениеFormalizing performance propertiesЗадание
04Performance analysis27 материалов

Running example

Running exampleВидео

Throughput and the maximum cycle mean

Throughput is bounded by 1/MCMВидеоProof - aВидеоProof - bВидеоProof - cВидеоProof - dВидеоProof - eВидеоProof - fВидеоProof - gВидеоProof - hВидеоProof - iВидеоProof - jВидеоSlides of the proofЧтениеSummarize!ЗаданиеThe throughput bound is tightВидеоCalculating the MCM and worst-case throughputЗаданиеAlternative proof in synchronization and linearityЧтение

Periodic scheduling

Periodic scheduling of a dataflow graphВидеоCalculate some periodic schedulesЗадание

Latency analysis

Latency analysis of a periodic scheduleВидеоLatency analysis of an eager scheduleВидеоThe formal definition of latencyВидеоThe boot-up time of a dataflow graphВидеоOptimizing latency estimates w.r.t. boot-up timeВидеоCalculating optimal periodic schedules and their latenciesЗадание

Buffering

Buffering and backpressureВидеоCalculating suitable buffer sizesЗадание
05One final example6 материалов

One final example

One final exampleВидео2015 Assignment on dataflow modeling.ЧтениеAdditional dataflow exercisesЧтениеExample of an exam at masters level (without solutions)ЧтениеAnother example of an exam (with solutions)ЧтениеMaterial created by fellow studentsЧтение