自動(dòng)化DMARF系統(tǒng)的形式化需求規(guī)范及性質(zhì)驗(yàn)證.pdf

1、現(xiàn)今，計(jì)算機(jī)系統(tǒng)日趨復(fù)雜，對(duì)其進(jìn)行有效的管理變得越來(lái)越困難。隨著人們需要的日益增加，系統(tǒng)中會(huì)同時(shí)存在更多的應(yīng)用軟件，服務(wù)器，存儲(chǔ)器等。要想有效的管理這些要素，確?？煽啃?，系統(tǒng)就需要具有自我管理的功能。
　　 2001年IBM公司提出了自動(dòng)化計(jì)算(Autonomic Computing)的概念。自動(dòng)化計(jì)算主要由幾個(gè)核心組成，自我保護(hù)、自我優(yōu)化、自我配置和自我恢復(fù)。自我保護(hù)，即系統(tǒng)能夠保護(hù)自己，防止外界的惡意襲擊；自我優(yōu)化，即系統(tǒng)能

2、夠自動(dòng)調(diào)度資源，以達(dá)到降低系統(tǒng)運(yùn)行消耗的目的；自我配置，即系統(tǒng)配置能夠自動(dòng)完成，并能根據(jù)需要自動(dòng)調(diào)整，來(lái)適應(yīng)動(dòng)態(tài)變化的運(yùn)行環(huán)境；自我恢復(fù)，即系統(tǒng)能夠自動(dòng)從常規(guī)和意外的故障中恢復(fù)，正常繼續(xù)運(yùn)行。
　　 自動(dòng)化計(jì)算系統(tǒng)通過(guò)嚴(yán)格的控制各個(gè)部分之間的交互來(lái)達(dá)到自治。但是構(gòu)造，控制這些交互十分困難。如何開(kāi)發(fā)一個(gè)具有高預(yù)測(cè)性的，安全可靠的IT系統(tǒng)呢?在這個(gè)問(wèn)題上，我們可以運(yùn)用嚴(yán)格的數(shù)學(xué)技術(shù)--形式化方法。Communicating Sequ

3、ential Processes(CSP)是一種形式化方法。其對(duì)模塊間的通訊進(jìn)行刻畫(huà)，從而模擬整個(gè)系統(tǒng)的性質(zhì)及行為。在描述分布式并發(fā)系統(tǒng)中，起到了很大的積極作用。
　　 本文以分布式聲音識(shí)別系統(tǒng)(DMARF)為實(shí)例，從自保護(hù)，自?xún)?yōu)化，自恢復(fù)三個(gè)方面，利用CSP方法描述其自治性質(zhì)，給出形式化自治需求規(guī)范。從而實(shí)現(xiàn)在分布式聲音識(shí)別系統(tǒng)上，添加一個(gè)自治層，以達(dá)到減少維護(hù)系統(tǒng)的工作量的目的。在此基礎(chǔ)上，運(yùn)用Process Analysi