這個老師真的好

一個周能夠看到他三次

一看就是實在的老師

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的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。