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

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

1、虛擬企業建模
1.1　虛擬企業模型
　　虛擬企業是一組企業的臨時組織或聯盟，其目的是通過聯合的成本與技術開拓適應快速變化的市場。建立具有指導意義的虛擬企業模型，以模型為驅動，實現虛擬企業信息系統，是當前解決虛擬企業集成問題普遍認可的方法。因此，建立虛擬企業模型，尤其是建立企業生產過程與經營過程模型，是分析企業過程，進而有效的組建虛擬企業系統的必需。

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

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