這個老師真的好

一個周能夠看到他三次

一看就是實在的老師

recording在teams外面錄制比較合適的，保證gbdr

為什么需要

動機

今年怎么學(xué)習(xí)這個課程

增加

查找

我們需要一些implementations

如果已經(jīng)有了

能不能有不完全的信息

你怎么去查找這個信息

現(xiàn)在我們有這樣的問題

natural language 是有一些模糊性的

我們需要做一些更加嚴謹?shù)南到y(tǒng)

barber類似一個計算機科學(xué)家

為什么需要formal method

我們需要證明這個系統(tǒng)是真的正確的

用數(shù)學(xué)的方法來解釋這個事情是對的

我們?nèi)康臇|西都是數(shù)學(xué)的

我們用數(shù)學(xué)的方法做設(shè)計和檢測

我們用正確的邏輯來分析

我們有清晰的semantic來分析

在這里

我們沒有不清楚的點

我們能夠拿到一個specification，直接去做這個東西，我們有一些自動化的工具

有一些系統(tǒng)是比較多復(fù)雜的，而且有些系統(tǒng)的很重要

比如說工業(yè)控制軟件

發(fā)電站的控制

通信系統(tǒng)

航天系統(tǒng)

我們要保證我們這個系統(tǒng)是正確的，能夠做我們希望做的事情

我們希望她們的不要崩，崩了就壞了

business critical system很重要，不能崩

instil灌輸

給了一個做code checking的很好的方法

我們可以寫specification

我們可以看這個button

可以從你給的需求，變成一個比較合適的方法

之后用一些系統(tǒng)的方法來接受這個系統(tǒng)

我們可以用這個系統(tǒng)來做需求到正式的需求的轉(zhuǎn)化

最后我們來實踐這個系統(tǒng)

直到我們這個系統(tǒng)能夠足夠的被大家所認可和接受

直到我們對于這個系統(tǒng)的認可是足夠的，是能夠被接受的

這個老師不錯

上課互動鏈接

z變換：經(jīng)典一級模型檢測，理論的東西

暫時的邏輯：concurrent dynamic distributed

模型檢驗：verification

小的program的specification

模型檢測是有很多工具

z就是一個transform function

get a new name

輸入，做一些事情，輸出

這些都能夠做一些transformation

這是一些

這些符號好奇怪

反應(yīng)系統(tǒng)和暫時邏輯

就是引入了很多的暫時的邏輯

有很多的東西是在不斷的輸入和輸出

暫時的邏輯，用來去做這個的建模

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

每一個周都有一個作業(yè)

兩個class test 選擇題

一個final examination 大題，4個大題，1：z+1：+2：model checking

每個周一有課件的上傳，英國的晚上十點，

總結(jié)

以上是生活随笔為你收集整理的comp313 formal methods lec1的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。