[發(fā)明專利]分析基于狀態(tài)的系統(tǒng)模型的方法和設備

無效

• 申請?zhí)枺?/td>: 99804553.5
• 申請日: 1999-03-26
• 公開（公告）號: CN1295686A
• 公開（公告）日: 2001-05-16
• 發(fā)明（設計）人: 亨里克·里爾伯格;亨里克·豪爾加德;約恩·伯·林德－尼爾森;亨里克·雷夫·安德森;金·古德斯特蘭德·拉爾森;卡爾·杰林·克里斯托福森;格爾德·伯爾曼
• 申請（專利權）人: IAR系統(tǒng)有限公司
• 主分類號: G06F11/00
• 分類號: G06F11/00;G06F17/50
• 代理公司: 中國國際貿易促進委員會專利商標事務所
• 代理人: 張維

本發(fā)明涉及分析基于狀態(tài)的系統(tǒng)模型的方法，該系統(tǒng)模型包括獨立的權利要求1、11和29中陳述的一組自動機。

考慮到市場的許多產品部分包含的軟件量不斷增長，并且所述部分中產品越來越多地傾向于僅由包含的軟件，而不是所用硬件的性能差別來區(qū)分，一般的軟件設計在錯誤識別和消除以及短期開發(fā)期限方面將會提出更高的要求。

相關的許多例子之一可以體現在汽車工業(yè)。即使批量生產的汽車包括的專用微處理器的數量也不斷增長。這些微處理器可以例如專用于控制ABS、燃料噴射、燈光控制、不同類型的監(jiān)控、熱控制、安全系統(tǒng)等等，許多不同的子系統(tǒng)經常必須通過常用協(xié)議來控制。

顯然，軟件控制單元的大規(guī)模出現導致了系統(tǒng)設計者的困境，因為總攬每個單元可能狀態(tài)的每一方面相當困難，當然，跟蹤所有使用的子系統(tǒng)間的協(xié)同作用更為復雜。應當提到的另一困難在于，大多數子系統(tǒng)由不同開發(fā)者或者開發(fā)小組設計，這些子系統(tǒng)之間的接口難以控制，因為沒有為開發(fā)者提供有效的工具來對這種大型系統(tǒng)進行必要的分析，甚至沒有對單個單元進行分析。

這會導致代價高昂并且非常重要的產品開發(fā)和發(fā)布時間的延遲。更為重要的是，一些產品甚至在包含固有的隱藏錯誤時就投入市場，這些錯誤在特定的未知條件下會被觸發(fā)。

在安全性極為重要的系統(tǒng)中，這個問題當然非常嚴重，在這種系統(tǒng)中，一個故障甚至可能會對涉及該故障的人員造成傷害。

測試這類故障的一種方法是在生產設備之前，通過符號模型檢查來檢查其邏輯。該技術在分析和驗證硬件系統(tǒng)中非常有效。但是，模型檢查對其它類型的并發(fā)系統(tǒng)，例如軟件系統(tǒng)而言是否是一個有效的工具尚未確定。

符號模型檢查的效果可能并不突出的一個理由是，軟件系統(tǒng)比硬件大，并且結構更不規(guī)則。例如，驗證大型軟件系統(tǒng)所報告的許多結果是用于線性結構，例如棧或管道，在表示成所謂的ROBDD，減序二進制判決圖時，已知其轉移關系的大小隨著系統(tǒng)的大小線性增長。

另一方案在美國專利第5，465，216中描述，其中描述了一種自動設計驗證方法。所描述的方法基本上承認了形式驗證存在“狀態(tài)爆炸問題”的缺陷，進一步得出各大系統(tǒng)的形式驗證超出了目前形式驗證技術的能力的結論。因此，上述專利描述了一種分解和減少系統(tǒng)模型的方式，而不是處理驗證方法的方式。因此，描述的方法的缺陷在于，可能可得到的結果僅是部分性的，而不是詳盡的。

基于上述ROBDD的一種更有希望的系統(tǒng)也利用了系統(tǒng)的結構，它由W.Lee等人在Tearing?based?automatic?abstraction?for?CTL?modelchecking給出，發(fā)表在1996年IEEE/ACM?International?Conferenceon?Computer-Aided?Design上，第76-81頁，San?Jose，CA，1996IEEE?Comput.Soc.Press。這種技術使用了分區(qū)轉移關系，利用貪婪啟發(fā)方法選擇轉移關系的子集。對選擇的每一子集而言，進行完整的定點遞歸。如果在這種遞歸之后無法證明公式，則選擇更大的子集。如果公式非法，則只有在構造了完整的轉移關系時(或者內存或時間用盡時)，算法才終止。這種技術的缺陷在于，如果系統(tǒng)僅具有單個初始狀態(tài)，就象嵌入軟件系統(tǒng)的一般情況那樣，那么它對剩余的每個自動機都實施涉及定點遞歸貪婪策略。貪婪策略減少到選擇任意自動機，從而涉及外部的定點遞歸。

本發(fā)明滿足形式驗證和利用未減系統(tǒng)模型的需求，提供了一種在基于各大型狀態(tài)的系統(tǒng)模型中執(zhí)行理論模型“破損測試”的可能性。此外，所述模型的分析和驗證可以在非減模型中實現的比率比現有技術分析和驗證工具高得多。

如果分析基于狀態(tài)的系統(tǒng)模型的方法，前述系統(tǒng)模型包括一組自動機(M1，…Mn)，每個所述自動機包括至少一個可能的狀態(tài)(pS1Mi，…，pSkMi)，在任一時刻，每個自動機都處于其組成狀態(tài)之一，

所述自動機(M1，…Mn)的動態(tài)行為由各自動機(M1，…Mn)的所述狀態(tài)之間的預定轉移，以及所述自動機(M1，…Mn)之間的相關性(D)來定義，

啟動所述自動機(M1，…Mn)的至少一個自動機狀態(tài)的初始集合(F)，

啟動表示自動機(MI)子集狀態(tài)條件的自動機狀態(tài)目標集合(A)，

重復以下步驟，直至分析得到肯定終止和/或如果自動機(MI)的子集包括所有所述自動機(M1，…Mn)，

為目標集(A)擴展一組狀態(tài)，這些狀態(tài)通過轉移可以到達前一目標集(A)，而與沒有包含在(MI)中的自動機無關，