基于ＵｐｐａａＩ的時延Ｐｅｔｒｉ網(wǎng)到時間自動機等價模型驗證
2005-04-29 00:00:00周清雷王靜
計算機應用研究 2005年6期
摘 要：時延Petri網(wǎng)和時間自動機都可以有效地對實時系統(tǒng)的行為進行模擬和性能分析。利用時延Petri網(wǎng)到時間自動機等價轉(zhuǎn)換算法(簡記作TPN-to—TA轉(zhuǎn)換)，將一個描述實時系統(tǒng)的時延Petri網(wǎng)模型轉(zhuǎn)換成與其語義等價的一組時間自動機模型。使用時間自動機中成熟的模型驗證工具Uppaal對此時延Petri網(wǎng)的模型進行驗證。
關鍵詞：時延Petri網(wǎng)；時間自動機；TPN-to—TA轉(zhuǎn)換；Uppaal
中圖法分類號：TP301．1
文獻標識碼：A
文章編號：1001—3695(2005)06—0064—03
