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

無效

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

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

所述自動機(jī)(M1，…Mn)的動態(tài)行為由各自動機(jī)(M1，…Mn)的所述狀態(tài)之間的預(yù)定轉(zhuǎn)移，以及所述自動機(jī)(M1，…Mn)之間的相關(guān)性(D)來定義，

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

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

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

為目標(biāo)集(A)擴(kuò)展一組狀態(tài)，這些狀態(tài)通過轉(zhuǎn)移可以到達(dá)前一目標(biāo)集(A)，而與沒有包含在(MI)中的自動機(jī)無關(guān)，

如果(A)包括初始狀態(tài)集(F)中至少一個自動機(jī)狀態(tài)，則肯定終止，否則為自動機(jī)(MI)的子集擴(kuò)展自動機(jī)(M1，…Mn)的至少一個子集。

2．根據(jù)權(quán)利要求1的基于狀態(tài)的系統(tǒng)模型的分析方法，其中為自動機(jī)(MI)的擴(kuò)展自動機(jī)(M1，…Mn)的至少一個子集的步驟包括為自動機(jī)(MI)的擴(kuò)展自動機(jī)的至少一個子集，前一(MI)與該子集相關(guān)。

3．根據(jù)權(quán)利要求2的基于狀態(tài)的系統(tǒng)模型的分析方法，其中如果在為目標(biāo)集(A)擴(kuò)展一組狀態(tài)的所述步驟之后，(MI)中的自動機(jī)都與(MI)之外的自動機(jī)沒有關(guān)系，則分析否定終止，前述狀態(tài)組可以達(dá)到前一目標(biāo)集(A)，而與沒有包含在(MI)中的自動機(jī)無關(guān)。

4．根據(jù)權(quán)利要求2-3的基于狀態(tài)的系統(tǒng)模型的分析方法，其中如果在為目標(biāo)集(A)擴(kuò)展一組狀態(tài)的所述步驟之后，目標(biāo)集(A)完全包含以前考慮的已經(jīng)得到肯定終止的目標(biāo)集(B)，則分析肯定終止，前述狀態(tài)組可以達(dá)到前一目標(biāo)集(A)，而與沒有包含在(MI)中的自動機(jī)無關(guān)。

5．根據(jù)權(quán)利要求1-4的基于狀態(tài)的系統(tǒng)模型的分析方法，其中如果在為目標(biāo)集(A)擴(kuò)展一組狀態(tài)的所述步驟之后，(MI)中的自動機(jī)都與(MI)之外的自動機(jī)沒有關(guān)系，則向用戶提供一種可視或者可聞指示，前述狀態(tài)組可以達(dá)到前一目標(biāo)集(A)，而與沒有包含在(MI)中的自動機(jī)無關(guān)。

6．根據(jù)權(quán)利要求1-5的基于狀態(tài)的系統(tǒng)模型的分析方法，其中分析應(yīng)用戶請求而終止。

7．根據(jù)權(quán)利要求1-6的基于狀態(tài)的系統(tǒng)模型的分析方法，其中相關(guān)性(D)表示為定向圖。

8．根據(jù)權(quán)利要求1-7的基于狀態(tài)的系統(tǒng)模型的分析方法，其中通過表示相關(guān)性的定向圖的寬度優(yōu)先遍歷來確定自動機(jī)(MI)的增加集合。

9．根據(jù)權(quán)利要求1-8的基于狀態(tài)的系統(tǒng)模型的分析方法，其中將自動機(jī)狀態(tài)集表示成減序二進(jìn)制判決圖(ROBDD)，對這些狀態(tài)的操作實現(xiàn)成對減序二進(jìn)制判決圖(ROBDD)的有效操作。

10．根據(jù)權(quán)利要求1-9的基于狀態(tài)的系統(tǒng)模型的分析方法，其中轉(zhuǎn)移表示成減序二進(jìn)制判決圖(ROBDD)的分區(qū)轉(zhuǎn)移關(guān)系。

11．根據(jù)權(quán)利要求1-10的基于狀態(tài)的系統(tǒng)模型的分析方法，其中狀態(tài)(A)集合由重復(fù)的定點遞歸來動態(tài)計算。