课程主页: https://www.coursera.org/learn/quantitative-formal-modeling-1
欢迎参加《定量形式建模与最坏情况性能分析》课程，这是一个旨在锻炼你在理论计算机科学领域中抽象思维能力的极具挑战性的课程。
本课程带领学生深入Token的生产与消费世界，这是理解系统行为的基础性方法。你将掌握如何通过前缀序和计数函数对这些概念进行数学形式化。此外，课程还将涉及Petri网，帮助学生探讨这些系统模型的细微差别。
课程大纲:
介绍
本课程是嵌入式系统混合硕士项目的一部分。
将系统建模为Token消费/生产系统
在这个模块中，你将学习如何绘制Token消费/生产系统的模型，并能够用非正式的方式与他人交流该模型的理解。完成此模块后，你将能够绘制自己的模型，并用一般术语解释它们。同时，你将了解Token消费/生产系统的标准Petri网解释，并能够指出Petri网模型中的特定模式。最后，你将能够将一个消费/生产模型细化为包含足够信息以进行最坏情况性能分析的模型。所有这些都将通过同伴评审作业进行测试。
语法与语义
这一模块将真正训练你的抽象思维能力。完成后你将学习如何将任何动态系统的行为形式化为前缀序，以及如何将消费/生产系统的解释形式化为这样的前缀序上的计数函数。你将了解Petri网解释对这些计数函数施加的某些限制，如何利用这些限制来证明关于Petri网解释的属性，而不需要真正了解该解释本身。最后，模块中将通过识别形式化的正例和反例来实践性能指标的形式化。
性能分析
在此模块中，你将学习如何利用单速数据流图的结构来执行性能指标的最坏情况分析，比如吞吐量、延迟和缓冲。结束后，你将知道如何计算数据流图的最大周期均值，如何为其构建周期性调度，如何优化该调度以分析延迟，以及如何确定缓冲的大小以确保最坏情况分析依然有效。
最后一个例子
在最后一周，我们将讨论一个额外的例子，遵循第一个模块的同伴评审作业的大纲。这是一个小总结，结合到目前为止我们所学的所有内容，并提供一些额外的阅读材料以激发进一步探索的兴趣。
能够理解和掌握本课程的内容将为学生在嵌入式系统及其他相关领域打下坚实的基础。
课程主页: https://www.coursera.org/learn/quantitative-formal-modeling-1