comp313 formal methods lec1
这个老师真的好
一个周能够看到他三次
一看就是实在的老师
recording在teams外面录制比较合适的，保证gbdr
为什么需要
动机
今年怎么学习这个课程
增加
查找
我们需要一些implementations
如果已经有了
能不能有不完全的信息
你怎么去查找这个信息
现在我们有这样的问题
natural language 是有一些模糊性的
我们需要做一些更加严谨的系统
barber类似一个计算机科学家
为什么需要formal method
我们需要证明这个系统是真的正确的
用数学的方法来解释这个事情是对的
我们全部的东西都是数学的
我们用数学的方法做设计和检测
我们用正确的逻辑来分析
我们有清晰的semantic来分析
在这里
我们没有不清楚的点
我们能够拿到一个specification，直接去做这个东西，我们有一些自动化的工具
有一些系统是比较多复杂的，而且有些系统的很重要
比如说工业控制软件
发电站的控制
通信系统
航天系统
我们要保证我们这个系统是正确的，能够做我们希望做的事情
我们希望她们的不要崩，崩了就坏了
business critical system很重要，不能崩
instil灌输
给了一个做code checking的很好的方法
我们可以写specification
我们可以看这个button
可以从你给的需求，变成一个比较合适的方法
之后用一些系统的方法来接受这个系统
我们可以用这个系统来做需求到正式的需求的转化
最后我们来实践这个系统
直到我们这个系统能够足够的被大家所认可和接受
直到我们对于这个系统的认可是足够的，是能够被接受的
这个老师不错
上课互动链接
z变换：经典一级模型检测，理论的东西
暂时的逻辑：concurrent dynamic distributed
模型检验：verification
小的program的specification
模型检测是有很多工具
z就是一个transform function
get a new name
输入，做一些事情，输出
这些都能够做一些transformation
这是一些
这些符号好奇怪
反应系统和暂时逻辑
就是引入了很多的暂时的逻辑
有很多的东西是在不断的输入和输出
暂时的逻辑，用来去做这个的建模
promela
如果被occopied
这个
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered). PROMELA models can be analyzed with the SPIN model checker, to verify that the modeled system produces the desired behavior. An implementation verified with Isabelle/HOL is also available, as part of the Computer Aided Verification of Automata project.[1] Files written in Promela traditionally have a .pml file extension.
finite state program是一个program的检验
temporal spefication这个是一系列的输入
这里有
model checking猛
没有tutorials
每一个周都有一个作业
两个class test 选择题
一个final examination 大题，4个大题，1：z+1：+2：model checking
每个周一有课件的上传，英国的晚上十点，
总结
以上是生活随笔为你收集整理的comp313 formal methods lec1的全部内容，希望文章能够帮你解决所遇到的问题。
- 上一篇： github的watch和star的位置
- 下一篇： use stacks能够把很多相似的文件