|
所在平台: Coursera |
课程主页: https://www.coursera.org/learn/system-validation-software-protocols
课程评论:没有评论
课程名称:系统验证(4):软件建模、协议和其他行为 概述:系统验证是研究系统通信和信息处理基础的领域。它通过基于系统行为模型的自动分析,确保系统按预期运行,保证系统的正确性。系统验证技术可以证明错误的缺失,帮助设计结构合理的嵌入式系统行为,从而使系统不仅运行正确,还更容易维护和适应。课程“建模软件、协议和其他行为”展示了形式方法在软件建模和通信协议等方面的强大能力。推荐阅读材料为《建模与分析通信系统》,作者J.F. Groote与M.R. Mousavi,2014年MIT出版社出版。 课程大纲: 1. 高级建模:本节展示如何对简单程序和通信协议的行为进行建模和分析,并引入线性过程的概念,这是一种可将所有行为简化的基本形式。该标准形式是行为分析的重要工具。 2. 建模指导:在这一讲中,您将学习各种建模技术,以帮助将模型的状态空间保持在较小的范围内。
Name:Advanced modelling
Description:We show how the behavior of simple programs and communication protocols can be modelled and analysed. Furthermore, we introduce the notion of a linear process: a simple normal form to which every behavior can be reduced. This normal form is the workhorse when it comes to the analysis of behavior.
Name:Modelling guidelines
Description:In this lecture you see various modelling techniques that can be used to keep the state space of your models small.
System Validation is the field that studies the fundamentals of system communication and information processing. It allows automated analysis based on behavioural models of a system to see if a system works correctly. We want to guarantee that the systems does exactly what it is supposed to do. The techniques put forward in system validation allow to prove the absence of errors. It allows to design embedded system behaviour that is structurally sound and as a side effect enforces you to make the behaviour simple and insightful. This means that the systems are not only behaving correctly, but are also much easier to maintain and adapt. ’Modeling Software Protocols, and other behaviour' demonstrates the power of formal methods in software modelling, communication protocols, and other examples. Reading material. J.F. Groote and M.R. Mousavi. Modeling and analysis of communicating systems. The MIT Press, 2014.