軟件體系結構形式化方法的適用性考察

黎 明 唐朝霞

（湖南科技學院，湖南 永州 425199）

軟件體系結構形式化方法的適用性考察

黎 明 唐朝霞

（湖南科技學院，湖南 永州 425199）

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

VDM-SL；需求定義；形式化方法；軟件體系結構；形式化描述

0 引 言

為了解決軟件危機、減少軟件開發的成本費用，人們提出了兩類解決方法：一類是采用工程化方法來組織管理軟件開發過程，即軟件工程方法。其中面向對象技術以及基于面向對象技術的軟件架構開發流程是能較好控制成本的手段之一。一類是深入研究軟件開發過程的規律，建立嚴密的數學理論，以指導軟件開發實踐。第一類方法中面向對象方法的軟件架構能夠描述出需求、設計以及實現等不同抽象水平的軟件構造，但是，在現階段還不能夠很好地表達抽象水平不同的構造層次以及不同構造元素之間的關系。

A.Hall提出了使用基于形式化方法的軟件體系結構的描述方法，可以準確地確定軟件的構造元素間關系[1]。使用形式化方法進行軟件開發的有用性，在 A.Hall的文獻中詳細地進行了說明。但是為了在實際的軟件開發項目中使用形式化方法，還有必要討論形式化方法時要注意的策略與基本原則。

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

1 VDM-SL簡介

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

VDM抽象層次高、語法嚴格，文法數學邏輯性強，它的核心元素為其標準化語言 VDM-SL。VDM-SL由一套數學表示系統和基于謂詞邏輯、集合理論的推理規則組成，基于抽象數據建模，用抽象模型描述計算功能；并且可以采用Hoare風格斷言描述推理規則。具有最少知識和簡單準確的特點。已被廣泛用于語言定義、需求分析和體系結構模型定義等領域[3]。

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

由于上述VDM-SL的優點并且在國內有過較多的實際軟件開發事例，本文決定采用VDM進行形式化描述，所預想的模型如圖1所示。形式化模型需要描述需求定義、設計、實現的各層次；需要描述邏輯模型和物理模型之間存在關系；并且需求與設計、設計和實現等不同開發過程之間的關聯關系也需要在模型中得到體現[4]。

以下論述主要聚焦于軟件體系結構的輸入部分：需求的描述，按照以下的原則使用VDM-SL來進行構建。

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

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

在抽象模型的描述中，只抽取了類型和函數對系統進行描述，這樣做的目的是能使開發者在描述需求時不用考慮物理系統結構，促進系統的抽象化過程，可以不用糾結于過多的描述方法。另外，具體模型采用在抽象模型的基礎上，將具體的數據作為值來進行定義。

圖1 體系結構的形式化描述模型

3 基于形式化方法的銷售管理系統的描述

銷售管理系統管理包含銷售商品的信息以及銷售金額等銷售數據，為了方便信息傳遞，對銷售數據的格式進行了規定。在本部分的內容中，使用形式化方法，針對銷售數據中的部分記錄的需求進行了定義。

3.1 抽象模型

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

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

銷售數額統計和銷售金額統計概念也會有相同的問題，單價的定義同樣也作為相關統計定義的對象。由于銷售數額統計中有多個統計對象，因此將統計對象作為參數定義為相應的統計函數。

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

3.2 具體模型

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

（1）所有的記錄當中，所含有的構成記錄商品的序列號都是相同的。

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

如下定義，采用商品列表來描述商品序列，用記錄生成函數來構造商品記錄。

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

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

4.1 形式化方法適用的效果

在上述構建需求的過程中，本文認為采用形式化方法可以得到以下的效果。

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

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

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

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

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

4.2 抽象化方法的方針

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

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

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

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

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

4.3 形式化方法適用的課題

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

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

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

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

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

5 結束語

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

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

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

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

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

TP311.5

A

1673-2219（2014）05-0122-03

2013－12－17

2013年永州市科技局科技計劃項目 “學校信息系統應用集成研究”。

黎明（1974－），男，湖南永州人，碩士，講師，主要研究領域為分布對象計算，計算機網絡，軟件工程。

（責任編校：劉志壯）