黎 明 唐朝霞

（湖南科技學(xué)院，湖南 永州 425199）

軟件體系結(jié)構(gòu)形式化方法的適用性考察

黎 明 唐朝霞

（湖南科技學(xué)院，湖南 永州 425199）

論文以一個銷售管理系統(tǒng)形式化建模為例，考察了采用形式化方法的適用性原則并探討了存在的問題。通過遵循試驗(yàn)證明，所提議的規(guī)則可以促進(jìn)模型的簡化、強(qiáng)化抽象概念的提取和明確抽象模型與具體模型的區(qū)別。在下一步工作中，需要討論開發(fā)過程多階段的形式化描述以及如何關(guān)聯(lián)多階段模型。

VDM-SL；需求定義；形式化方法；軟件體系結(jié)構(gòu)；形式化描述

0 引 言

為了解決軟件危機(jī)、減少軟件開發(fā)的成本費(fèi)用，人們提出了兩類解決方法：一類是采用工程化方法來組織管理軟件開發(fā)過程，即軟件工程方法。其中面向?qū)ο蠹夹g(shù)以及基于面向?qū)ο蠹夹g(shù)的軟件架構(gòu)開發(fā)流程是能較好控制成本的手段之一。一類是深入研究軟件開發(fā)過程的規(guī)律，建立嚴(yán)密的數(shù)學(xué)理論，以指導(dǎo)軟件開發(fā)實(shí)踐。第一類方法中面向?qū)ο蠓椒ǖ能浖軜?gòu)能夠描述出需求、設(shè)計以及實(shí)現(xiàn)等不同抽象水平的軟件構(gòu)造，但是，在現(xiàn)階段還不能夠很好地表達(dá)抽象水平不同的構(gòu)造層次以及不同構(gòu)造元素之間的關(guān)系。

A.Hall提出了使用基于形式化方法的軟件體系結(jié)構(gòu)的描述方法，可以準(zhǔn)確地確定軟件的構(gòu)造元素間關(guān)系[1]。使用形式化方法進(jìn)行軟件開發(fā)的有用性，在 A.Hall的文獻(xiàn)中詳細(xì)地進(jìn)行了說明。但是為了在實(shí)際的軟件開發(fā)項(xiàng)目中使用形式化方法，還有必要討論形式化方法時要注意的策略與基本原則。

本論文通過一個商品銷售管理系統(tǒng)的實(shí)例，考察了基于形式化描述方法的描述模型和形式化方法的適用規(guī)則。

1 VDM-SL簡介

形式化系統(tǒng)中最具有代表性的方法是 VDM(Vienna Development Method)方法，基本思想是運(yùn)用抽象數(shù)據(jù)類型、數(shù)學(xué)概念和符號來定義軟件開發(fā)中的運(yùn)算和函數(shù)功能。在高層次的抽象模型上進(jìn)行功能描述，能夠讓開發(fā)者獲得對系統(tǒng)的深刻理解并能早期發(fā)現(xiàn)和避免實(shí)現(xiàn)細(xì)節(jié)錯誤的傳遞[2]。

VDM抽象層次高、語法嚴(yán)格，文法數(shù)學(xué)邏輯性強(qiáng)，它的核心元素為其標(biāo)準(zhǔn)化語言 VDM-SL。VDM-SL由一套數(shù)學(xué)表示系統(tǒng)和基于謂詞邏輯、集合理論的推理規(guī)則組成，基于抽象數(shù)據(jù)建模，用抽象模型描述計算功能；并且可以采用Hoare風(fēng)格斷言描述推理規(guī)則。具有最少知識和簡單準(zhǔn)確的特點(diǎn)。已被廣泛用于語言定義、需求分析和體系結(jié)構(gòu)模型定義等領(lǐng)域[3]。

2 基于VDM-SL的描述模型和原則

由于上述VDM-SL的優(yōu)點(diǎn)并且在國內(nèi)有過較多的實(shí)際軟件開發(fā)事例，本文決定采用VDM進(jìn)行形式化描述，所預(yù)想的模型如圖1所示。形式化模型需要描述需求定義、設(shè)計、實(shí)現(xiàn)的各層次；需要描述邏輯模型和物理模型之間存在關(guān)系；并且需求與設(shè)計、設(shè)計和實(shí)現(xiàn)等不同開發(fā)過程之間的關(guān)聯(lián)關(guān)系也需要在模型中得到體現(xiàn)[4]。

以下論述主要聚焦于軟件體系結(jié)構(gòu)的輸入部分：需求的描述，按照以下的原則使用VDM-SL來進(jìn)行構(gòu)建。

(1) 抽象模型 VDM-SL中使用類型（types）和函數(shù)（functions）進(jìn)行描述。

(2) 具體模型 在抽象模型的基礎(chǔ)上追加值的方式進(jìn)行描述。

在抽象模型的描述中，只抽取了類型和函數(shù)對系統(tǒng)進(jìn)行描述，這樣做的目的是能使開發(fā)者在描述需求時不用考慮物理系統(tǒng)結(jié)構(gòu)，促進(jìn)系統(tǒng)的抽象化過程，可以不用糾結(jié)于過多的描述方法。另外，具體模型采用在抽象模型的基礎(chǔ)上，將具體的數(shù)據(jù)作為值來進(jìn)行定義。

圖1 體系結(jié)構(gòu)的形式化描述模型

3 基于形式化方法的銷售管理系統(tǒng)的描述

銷售管理系統(tǒng)管理包含銷售商品的信息以及銷售金額等銷售數(shù)據(jù)，為了方便信息傳遞，對銷售數(shù)據(jù)的格式進(jìn)行了規(guī)定。在本部分的內(nèi)容中，使用形式化方法，針對銷售數(shù)據(jù)中的部分記錄的需求進(jìn)行了定義。

3.1 抽象模型

銷售管理系統(tǒng)所涉及的抽象概念使用抽象模型進(jìn)行描述，相關(guān)記錄中的詳細(xì)信息使用具體模型來進(jìn)行描述。通過分析需求對象，以商品、分類、單價、銷售記錄、銷售數(shù)量統(tǒng)計、銷售金額統(tǒng)計的概念來表示需求內(nèi)容。為了能描述這些概念，我們定義了以下的類型。

單價概念中，又分為現(xiàn)金銷售的單價和會員卡銷售的單價兩種。 本文在具體模型中使用如下的方式進(jìn)行定義。values

銷售數(shù)額統(tǒng)計和銷售金額統(tǒng)計概念也會有相同的問題，單價的定義同樣也作為相關(guān)統(tǒng)計定義的對象。由于銷售數(shù)額統(tǒng)計中有多個統(tǒng)計對象，因此將統(tǒng)計對象作為參數(shù)定義為相應(yīng)的統(tǒng)計函數(shù)。

上述的單價的描述中，將現(xiàn)金銷售單價和會員卡銷售單價兩個概念統(tǒng)一定義為單價表，使得現(xiàn)金銷售單價和會員卡銷售單價中的相同概念可以提取并抽象化。另外，含有多個統(tǒng)計對象的銷售數(shù)額的統(tǒng)計，定義為銷售數(shù)統(tǒng)計表函數(shù)，捕捉了其中的參數(shù)化概念并進(jìn)行了抽象化。通過使用數(shù)據(jù)和操作的抽象化，將10個記錄中含有的概念抽象為6個概念，實(shí)現(xiàn)了簡單、明確的表達(dá)。

3.2 具體模型

具體模型階段，明確從抽象模型中生成記錄的基本概念。本文案例中的具體模型的描述規(guī)則如下：

（1）所有的記錄當(dāng)中，所含有的構(gòu)成記錄商品的序列號都是相同的。

（2）在具體模型中定義商品和分類等編碼化的相關(guān)信息。

如下定義，采用商品列表來描述商品序列，用記錄生成函數(shù)來構(gòu)造商品記錄。

通過定義記錄生成函數(shù)，明確了具體模型生成記錄的接口。記錄生成函數(shù)明確了抽象模型中必要信息的構(gòu)造，對抽象模型的進(jìn)一步細(xì)化工作有較大的影響。另外，在具體模型的描述中，將與抽象模型中共有的類型、值、函數(shù)等概念進(jìn)行細(xì)化和具體化，讓兩種模型得到連接，也可以在具體模型中找到對應(yīng)的抽象模型，盡量避免需求過度或者需求誤解。

4 形式化方法適用的效果和課題

4.1 形式化方法適用的效果

在上述構(gòu)建需求的過程中，本文認(rèn)為采用形式化方法可以得到以下的效果。

(1)使用VDM-SL的類型和函數(shù)定義所有的概念，這是進(jìn)行概念整理的一種有效的手段。

(2)使用形式化方法手段可以在一定程度上避免因?yàn)閭€人理解差異，而造成需求定義的偏差。

(3)使用形式化描述方法，不能指望能將所需要表述的需求進(jìn)行完全詳盡的描述。

(4)通過摸索更加通用的類型和函數(shù)，在抽象化過程中進(jìn)一步發(fā)現(xiàn)可以合并的抽象級別較高的概念。

(5)使用形式化方法進(jìn)行定義模型時，我們必須對系統(tǒng)的全局概念比較清楚，可以促進(jìn)開發(fā)者把握系統(tǒng)需求的整體概念。

4.2 抽象化方法的方針

通過上述的事例，我們可以得到以下抽象化方法的方針：

(1)省略非重要概念的具體描述：在抽象化過程中，概念過多會讓模型復(fù)雜化，因此可以使用token,undefined字段簡化模型。

(2)同一概念用一個類型來定義：如在單價概念定義的例子中，找出可以通用的類型來進(jìn)行描述，促進(jìn)模型的互操作性，避免相同概念的不同描述產(chǎn)生的歧義。

(3)抽象出可以參數(shù)化的函數(shù)：如記錄生成函數(shù)的例子中，將記錄生成概念中的相關(guān)處理模塊化，將個數(shù)參數(shù)化，定義出參數(shù)化函數(shù)。

(4)抽取通用化的函數(shù)：如銷售數(shù)統(tǒng)計表函數(shù)的例子中，根據(jù)功能的共同部分抽選出通用部分，定義為函數(shù)，提高抽象化程度。

4.3 形式化方法適用的課題

使用形式化方法描述需求還存在以下的課題：

(1)存在使用自然語言可以很簡單地進(jìn)行描述，但使用形式化會變得復(fù)雜的場景。

(2)存在使用形式化的表達(dá)使得需求難以理解的場景。

以上的問題，主要是由于缺少在各種場景中的形式化描述實(shí)例，因此，能夠公開在實(shí)際開發(fā)現(xiàn)場中使用形式化方法描述需求的案例的相關(guān)信息是解決上述問題的重點(diǎn)。

在具體的開發(fā)實(shí)例中為了描述需求，使用圖比較多，而VDM-SL中，雖然可以使用解釋器執(zhí)行已經(jīng)具體化的形式化描述，但還沒有解析和生成圖的功能。如果可以將解釋器執(zhí)行時的數(shù)據(jù)、數(shù)學(xué)模型圖示化，這樣就可以做到執(zhí)行的可視化，對形式化語言的需求描述理解有更好的支援效果。

5 結(jié)束語

本文通過以使用形式語言VDM-SL來描述銷售管理系統(tǒng)的需求，考察了在開發(fā)中采用形式化方法的原則以及還存在的課題。通過遵循形式化方法描述的規(guī)則，可以促進(jìn)模型的簡化、強(qiáng)化抽象概念的提取和明確抽象模型和具體模型的區(qū)別。在今后的工作中，進(jìn)一步討論如何在開發(fā)階段，在將需求模型形式化時給出需遵循規(guī)則的提示。 并且關(guān)注設(shè)計階段的形式化描述以及如何銜接需求與設(shè)計之間的關(guān)聯(lián)。

[1]Jim.Woodcock, Peter.Gorm.Larsen, Juan.Bicarrequi.Formal methods:Practice and experience[J].ACM Computing Surveys, 2009,(10):119-126.

[2]曹重華,白似雪,楊錦云.維也納分析方法及其應(yīng)用[J].南昌大學(xué)學(xué)報(理科版),2005,(2):99-102.

[3]齊學(xué)智,陳金水.從形式化式樣出發(fā)的實(shí)時控制軟件開發(fā)[J].工業(yè)控制計算機(jī),2004,(8):28-29.

[4]王昌晶,羅海梅,左正康.基于問題模式的形式化軟件規(guī)格說明生成方法[J].計算機(jī)研究與發(fā)展,2013,(2):352-360.

TP311.5

A

1673-2219（2014）05-0122-03

2013－12－17

2013年永州市科技局科技計劃項(xiàng)目 “學(xué)校信息系統(tǒng)應(yīng)用集成研究”。

黎明（1974－），男，湖南永州人，碩士，講師，主要研究領(lǐng)域?yàn)榉植紝ο笥嬎?，計算機(jī)網(wǎng)絡(luò)，軟件工程。

（責(zé)任編校：劉志壯）