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.