軟件體系結(jié)構(gòu)形式化方法
時(shí)間：2024-01-21 22:35:01 | 來(lái)源：信息時(shí)代
時(shí)間：2024-01-21 22:35:01 來(lái)源：信息時(shí)代
軟件體系結(jié)構(gòu)形式化方法是指在嚴(yán)格的數(shù)學(xué)基礎(chǔ)（邏輯、代數(shù)、自動(dòng)機(jī)、圖論等）之上建立的軟件開(kāi)發(fā)方法，它是數(shù)學(xué)上的綜合、分析技術(shù)的應(yīng)用，用于開(kāi)發(fā)計(jì)算機(jī)控制的系統(tǒng)。它可提供一個(gè)用于模型設(shè)計(jì)和分析的嚴(yán)格而有效的途徑。其主要目的是克服自然語(yǔ)言、圖表等非形式化方法描述體系結(jié)構(gòu)存在的不足。由于形式化方法能在早起發(fā)現(xiàn)系統(tǒng)中的不一致、歧義、不完全和錯(cuò)誤，目前己被證明是一種行之有效的減少設(shè)計(jì)錯(cuò)誤的方法，是提高軟件系統(tǒng)可信度的重要途徑。開(kāi)始的時(shí)候，研究人員運(yùn)用形式化方法描述單個(gè)軟件系統(tǒng)的體系結(jié)構(gòu)或者體系結(jié)構(gòu)風(fēng)格。然后，逐步提出運(yùn)用形式化方法描述和分析體系結(jié)構(gòu)的通用模型。根據(jù)對(duì)目標(biāo)軟件系統(tǒng)進(jìn)行說(shuō)明的方式，形式化方法可以分為如下兩種：
1、面向模型的方法。在面向模型的方法中，對(duì)目標(biāo)軟件系統(tǒng)的說(shuō)明是為其構(gòu)造一個(gè)模型，該模型的構(gòu)成成分是一些具有特性的數(shù)據(jù)抽象，如域、元組、集合、序列、包、映射等。
2、面向性質(zhì)的方法。這種方法通過(guò)直接給出目標(biāo)軟件系統(tǒng)的一組特性來(lái)描述目標(biāo)軟件系統(tǒng)，通常是一組目標(biāo)軟件系統(tǒng)必須滿足的形式公理。在面向性質(zhì)的方法中，其形式規(guī)格說(shuō)明僅描述目標(biāo)軟件系統(tǒng)的性質(zhì)，而不涉及實(shí)現(xiàn)方法。
根據(jù)表達(dá)能力，形式化方法大致可分為五類：
1、基于模型的方法。給出系統(tǒng)（程序）狀態(tài)和狀態(tài)變換與操作的顯式但亦是抽象的定義，但對(duì)于并發(fā)沒(méi)有顯式的表示，如基于模型的形式規(guī)約語(yǔ)言Z和VDM。
2、代數(shù)方法。通過(guò)聯(lián)系不同操作間的行為關(guān)系而給出操作的隱式定義，而不定義狀態(tài)，同樣它亦未給出并發(fā)的顯式的表示，如基于性質(zhì)的代數(shù)規(guī)約語(yǔ)言O(shè)BJ， LARCH， CLEAR。
3、過(guò)程代數(shù)方法。給出并發(fā)過(guò)程的一個(gè)顯式模型，并通過(guò)過(guò)程間允許的可觀察的通訊上的限制（約束）來(lái)表示行為，如CSP， CCP。
4、基于邏輯的方法。有很多方法采用邏輯來(lái)描述系統(tǒng)的特性，包括程序允許的低級(jí)規(guī)范和系統(tǒng)時(shí)間行為的規(guī)范，如時(shí)態(tài)邏輯。
5、基于網(wǎng)絡(luò)的方法。根據(jù)網(wǎng)絡(luò)中數(shù)據(jù)流顯式地給出系統(tǒng)的并發(fā)模型，包括數(shù)據(jù)在網(wǎng)中從一個(gè)結(jié)點(diǎn)流向另一個(gè)結(jié)點(diǎn)的條件。如Petri網(wǎng)、謂詞變換網(wǎng)。
形式化方法的研究和應(yīng)用己有30多年的歷史。最初的產(chǎn)生是由Dikstra和Hoare在程序難驗(yàn)證方面的工作中和Scott，Strachey以及其他學(xué)者在程序語(yǔ)義方面的工作基礎(chǔ)上發(fā)展起來(lái)的。
在軟件開(kāi)發(fā)過(guò)程中，用戶需求的規(guī)格說(shuō)明（體系結(jié)構(gòu)描述）非常重要，其使用者包括用戶、系統(tǒng)分析員、設(shè)計(jì)與編程人員、測(cè)試人員和驗(yàn)收人員。規(guī)格說(shuō)明對(duì)這些人員來(lái)說(shuō)是一個(gè)可靠的參照點(diǎn)；系統(tǒng)分析員接受用戶的需求，產(chǎn)生目標(biāo)軟件系統(tǒng)的規(guī)格說(shuō)明；設(shè)計(jì)與編程人員根據(jù)規(guī)格說(shuō)明，進(jìn)行模塊設(shè)計(jì)并產(chǎn)生最終程序代碼；測(cè)試人員和驗(yàn)收人員驗(yàn)證最終程序代碼是否滿足規(guī)格說(shuō)明。
-
網(wǎng)站
-
營(yíng)銷
-
設(shè)計(jì)
-
運(yùn)營(yíng)
-
優(yōu)化
-
效率
-
專注
-
電商
-
方案
-
推廣
微信公眾號(hào)
版權(quán)所有? 億企邦 1997-2025 保留一切法律許可權(quán)利。
在線咨詢