摘要：為開發(fā)正確、可靠、基于模型驅(qū)動的虛擬企業(yè)信息系統(tǒng)，滿足虛擬企業(yè)對于可伸縮性、可重構(gòu)性、可重用性以及互操作性的要求，在虛擬企業(yè)建模與開發(fā)過程中引入形式化RAISE(工業(yè)軟件工程嚴格方法)，分析了在虛擬企業(yè)組建中應(yīng)用形式化方法的優(yōu)點，討論了RAISE與有著廣泛應(yīng)用的傳統(tǒng)IDEF(集成計算機輔助制造定義方法)的結(jié)合，并給出了運用形式化方法進行虛擬企業(yè)建模的方案。該方法是虛擬企業(yè)建模與實現(xiàn)技術(shù)的重要研究方向。
關(guān)鍵詞：虛擬企業(yè)；企業(yè)模型；形式化方法；工業(yè)軟件工程嚴格方法(RAISE)；集成計算機輔助制造定義方法(IDEF)

　　CIMS的研究與開發(fā)正處于企業(yè)集成階段，虛擬企業(yè)研究正是這一階段的重要研究課題和使能技術(shù)之一。對于虛擬企業(yè)的建立與運作，尤其是在作為其基礎(chǔ)與要素的虛擬企業(yè)模型以及相應(yīng)的信息系統(tǒng)實現(xiàn)問題上，還不存在成熟的理論、方法與規(guī)范。本文應(yīng)用形式化的工業(yè)軟件工程嚴格方法(RAISE)與集成計算機輔助制造定義方法(IDEF)相結(jié)合的手段建立虛擬企業(yè)模型，并探討有關(guān)模型驅(qū)動的系統(tǒng)集成與系統(tǒng)實現(xiàn)問題。

1、虛擬企業(yè)建模
1.1　虛擬企業(yè)模型
　　虛擬企業(yè)是一組企業(yè)的臨時組織或聯(lián)盟，其目的是通過聯(lián)合的成本與技術(shù)開拓適應(yīng)快速變化的市場。建立具有指導(dǎo)意義的虛擬企業(yè)模型，以模型為驅(qū)動，實現(xiàn)虛擬企業(yè)信息系統(tǒng)，是當前解決虛擬企業(yè)集成問題普遍認可的方法。因此，建立虛擬企業(yè)模型，尤其是建立企業(yè)生產(chǎn)過程與經(jīng)營過程模型，是分析企業(yè)過程，進而有效的組建虛擬企業(yè)系統(tǒng)的必需。

1.2　虛擬企業(yè)建模面臨的問題
　　虛擬企業(yè)的集成和企業(yè)模型的構(gòu)建很復(fù)雜，建模需要著重解決以下問題：
1)企業(yè)模型必須能從高層抽象企業(yè)功能、結(jié)構(gòu)、特性，以便企業(yè)級的過程重組；
2)企業(yè)模型必須適應(yīng)動態(tài)虛擬企業(yè)的特點，做到易于重構(gòu)(即有可重構(gòu)性)；
3)可重用性與可伸縮性；
4)建模方法必須簡單易用，這是因為一般企業(yè)，尤其是中小型企業(yè)，不具備專業(yè)的建模人員；
5)企業(yè)建模過程應(yīng)該融合企業(yè)的不同層次，使虛擬企業(yè)涉及的各層次人員能夠廣泛參與。
　　虛擬企業(yè)的復(fù)雜性使得一些單一信息系統(tǒng)中低層次的問題也必須提高到模型(抽象)層次才能解決。這使虛擬企業(yè)建模問題更加復(fù)雜化。以IDEF為代表的傳統(tǒng)企業(yè)建模方法在處理虛擬企業(yè)建模問題上逐漸暴露出自身的某些局限性。為了解決上述問題，增加系統(tǒng)實現(xiàn)的自動化程度、減少系統(tǒng)的不一致性，更快、更好、更可靠的實現(xiàn)虛擬企業(yè)系統(tǒng)，嘗試在企業(yè)模型建立與系統(tǒng)實現(xiàn)的過程中引入形式化方法作為傳統(tǒng)建模方法的補充。

2、形式化方法
2.1　形式化方法與疑問
　　作為一種以數(shù)學(xué)邏輯為基礎(chǔ)的方法，形式化方法以其嚴密性越來越受到眾多領(lǐng)域的重視，尤其是在安全性和可靠性作為關(guān)鍵問題的系統(tǒng)，如核電站、航空航天、鐵路運輸系統(tǒng)中得到了較為廣泛的應(yīng)用。但是對于形式化方法在工業(yè)領(lǐng)域的實際應(yīng)用問題，在學(xué)術(shù)界和工程界，尤其是在系統(tǒng)開發(fā)人員當中，還存在著相當多的疑問。
　　1990年，J.A.Hall回答了有關(guān)形式化方法的7個疑問。這7個疑問是：
1)該方法可否保證軟件系統(tǒng)的完美無缺；
2)它處理的只是程序正確性的證明；
3)它只適用于安全第一的系統(tǒng)；
4)它需要專業(yè)的數(shù)學(xué)知識；
5)它增加系統(tǒng)開發(fā)的成本；
6)用戶無法接受它；
7)無法應(yīng)用于大型的實際系統(tǒng)。
　　J.A.Hall對這7個問題的回答是：形式化方法不能保證系統(tǒng)的完美無缺，也并不能減少系統(tǒng)所需的測試。用戶不能認為它是萬能的(疑問1)。形式化方法不僅僅局限于對程序正確性的證明，也不是只適用于安全第一的系統(tǒng)。它在眾多非安全第一的系統(tǒng)中的成功應(yīng)用足以說明這一點(疑問2～3)。許多復(fù)雜問題的簡單形式化描述，以及若干項目的成功運作反駁了有關(guān)形式化方法需要專業(yè)的數(shù)學(xué)知識(疑問4)，而且必將增加系統(tǒng)成本的說法(疑問5)。最終用戶以及非專業(yè)人員在系統(tǒng)開發(fā)中的廣泛參與說明了用戶對該方法的認可(疑問6)。它在幾個大型實際系統(tǒng)中成功應(yīng)用已經(jīng)引起了廣泛的關(guān)注，也否定了形式化方法無法應(yīng)用于大型實際系統(tǒng)的說法(疑問7)。
　　1995年，JonathanP.Bowen進一步回答了隨著計算科學(xué)的發(fā)展，有關(guān)形式化方法的新疑問。
8)該方法延遲開發(fā)進程；
9)它缺乏支持工具；
10)它將代替?zhèn)鹘y(tǒng)的工程設(shè)計方法；
11)只適用于軟件設(shè)計；
12)實際上并不需要它；
13)它缺乏支持；
14)該方法的熱衷人員只使用形式化方法。
　　JonathanP.Bowen對這7個問題的