實(shí)時(shí)控制系統(tǒng)軟件開(kāi)發(fā)構(gòu)架研究.pdf

1、在實(shí)時(shí)控制系統(tǒng)中，軟件是控制反饋環(huán)的重要部分。該類軟件中增加了嚴(yán)格的時(shí)間要求，同時(shí)低級(jí)的實(shí)時(shí)技術(shù)須與高級(jí)的程序設(shè)計(jì)、網(wǎng)絡(luò)通信、仿真和控制相結(jié)合。作為控制大型復(fù)雜不確定系統(tǒng)的基礎(chǔ)，系統(tǒng)構(gòu)架分析就處于首要地位。目前，實(shí)時(shí)控制系統(tǒng)的構(gòu)架分析主要依靠經(jīng)驗(yàn)，并借助UML等建模工具。UML雖然可以給系統(tǒng)建立靜態(tài)和動(dòng)態(tài)模型，但是這些模型往往存在二義性，不能真正表述系統(tǒng)需求，并且在描述系統(tǒng)時(shí)間信息方面存在較大困難。 本課題的研究?jī)?nèi)容是將形式化方

2、法CSP、B方法和OCL引入到實(shí)時(shí)控制系統(tǒng)的構(gòu)架分析中。盡管CSP和B方法都是一種較好的形式化方法，可以用于系統(tǒng)構(gòu)架分析。但是，單獨(dú)一種在描述實(shí)時(shí)控制系統(tǒng)構(gòu)架方面都存在不足，如CSP不擅長(zhǎng)對(duì)數(shù)據(jù)和函數(shù)等進(jìn)行定義，而B(niǎo)方法在描述系統(tǒng)并發(fā)控制等方面又存在局限。本文創(chuàng)造性的提出一種新的形式化方法CSP-B的設(shè)計(jì)策略。CSP-B是將形式化方法CSP和B方法集成在一起，集成后的CSP-B通過(guò)在規(guī)格中引入CSP來(lái)保持對(duì)系統(tǒng)的總體結(jié)構(gòu)、控制能力及行為

3、描述等方面的特性；通過(guò)引入B方法來(lái)實(shí)現(xiàn)抽象數(shù)據(jù)結(jié)構(gòu)定義、系統(tǒng)限制以及功能處理等方面的特性。 本文介紹了通訊順序進(jìn)程(CSP)的符號(hào)系統(tǒng)，CSP是一種形式化方法，能嚴(yán)格地表述一個(gè)系統(tǒng)或進(jìn)程執(zhí)行事件的時(shí)序性以及系統(tǒng)之間相互通信的特性。本文也介紹了另一種形式化方法-B方法的形式化定義，B方法支持大部分的軟件過(guò)程：需求分析、規(guī)格說(shuō)明、軟件設(shè)計(jì)、實(shí)現(xiàn)和維護(hù)等。同時(shí)，本文也給出了對(duì)象約束語(yǔ)言(OCL)的使用方法及形式化定義，OCL是一種對(duì)U

4、ML模型進(jìn)行約束描述的形式化語(yǔ)言，允許開(kāi)發(fā)人員創(chuàng)建模型中各個(gè)對(duì)象之間的詳細(xì)約束規(guī)則。 為了驗(yàn)證CSP-B方法的有效性，本文將CSP-B運(yùn)用到具體的實(shí)時(shí)控制系統(tǒng)的架構(gòu)分析當(dāng)中，從而得到CSP-B規(guī)格。由于目前沒(méi)有支持CSP-B方法的有效工具，并且鑒于UML已經(jīng)成為國(guó)內(nèi)軟件開(kāi)發(fā)的事實(shí)工業(yè)標(biāo)準(zhǔn)，所以本文嘗試將CSP-B規(guī)格用UML模型來(lái)表示。由于UML是非形式化的，其模型在某些方面有一定二義性，所以本文將UML模型添加OCL約束以消除