自動化DMARF系統(tǒng)的形式化需求規(guī)范及性質驗證.pdf

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

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

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