神經(jīng)內(nèi)分泌復(fù)雜系統(tǒng)的形式化研究.pdf

1、目前軟件工業(yè)界面臨著產(chǎn)品功能越來越復(fù)雜的壓力。軟件工程的一個(gè)主要目標(biāo)就是在軟件復(fù)雜性增加的情況下仍能構(gòu)造正確可靠的系統(tǒng)，達(dá)到這一目標(biāo)的途徑之一是形式化方法。形式化方法是一種用于規(guī)范、設(shè)計(jì)和驗(yàn)證計(jì)算機(jī)系統(tǒng)的軟件開發(fā)方法，它建立在嚴(yán)格的數(shù)學(xué)基礎(chǔ)之上，使開發(fā)的模型得到證明，可以有效提高軟件的可靠性。 需求獲取是軟件開發(fā)過程中最為困難也是最為重要的部分。已有的需求獲取方法例如訪談法、問卷法、觀察法和用戶資料研究法等，這些都是簡單的方法，

2、但這些方法的效果與項(xiàng)目的風(fēng)險(xiǎn)是成反比的。對于一般系統(tǒng)的需求它們會產(chǎn)生很多的錯(cuò)誤，復(fù)雜的系統(tǒng)它們更是無能為力。因此，迫切需要更加科學(xué)的方法來研究復(fù)雜系統(tǒng)，論文提出用復(fù)雜網(wǎng)絡(luò)的度相關(guān)特性作為需求獲取的方法。復(fù)雜網(wǎng)絡(luò)就是對大量現(xiàn)實(shí)世界真實(shí)復(fù)雜系統(tǒng)的一種理想簡化描述，相關(guān)性有可能帶來復(fù)雜系統(tǒng)理論的新突破。 在獲取了系統(tǒng)的需求后再用形式化B方法進(jìn)行描述，以提高系統(tǒng)的可靠性，但是，B不是面向?qū)ο蠖腔趯ο蟮牟⑶褺需求規(guī)格說明的可讀性差?？?/p>

3、讀性差阻礙了在規(guī)格校驗(yàn)時(shí)用戶的介入。而統(tǒng)一建模語言(UMI)已成為面向?qū)ο筌浖到y(tǒng)中描述分析和設(shè)計(jì)階段模型的標(biāo)準(zhǔn)化記法。但UML缺乏精確的語義，因此對模型難以進(jìn)行一致性檢查和正確性分析，成為基于UML技術(shù)的嚴(yán)重缺陷。 針對以上問題，本文提出了形式化B方法到UML類圖的轉(zhuǎn)換思想，將形式化B方法轉(zhuǎn)換后的UML類圖更好地用于面向?qū)ο蟮能浖_發(fā)中。其中B方法作為數(shù)學(xué)基礎(chǔ)；UML作為支持建模語言，其圖形表示直觀易理解；將UML與形式化語言

4、的的準(zhǔn)確性、一致性結(jié)合起來，為模型的正確性證明、轉(zhuǎn)換及一致性檢查提供有力的理論方法。 主要做了以下方面的工作： 1、對現(xiàn)有的需求獲取的方法進(jìn)行了歸納總結(jié)，提出用復(fù)雜網(wǎng)絡(luò)的度相關(guān)特性作為復(fù)雜系統(tǒng)需求獲取的方法。 2、通過用復(fù)雜網(wǎng)絡(luò)對神經(jīng)內(nèi)分泌復(fù)雜系統(tǒng)的研究，得到了這個(gè)系統(tǒng)的一些統(tǒng)計(jì)特性和部分重要細(xì)胞及介質(zhì)。 3、使用研究得到的結(jié)果對神經(jīng)內(nèi)分泌復(fù)雜系統(tǒng)進(jìn)行形式化B描述，然后用ProB工具對得到的B規(guī)格說明進(jìn)行