頁籤選單縮合
題名 | A New Technique for Behavior and Temporal Analysis of Timed Petri Nets=即時型派翠網模型之行為分析與時序驗證的技術 |
---|---|
作者姓名(中文) | 黃其泮; 何正信; | 書刊名 | 中國工程學刊 |
卷期 | 20:5 1997.09[民86.09] |
頁次 | 頁481-492 |
分類號 | 448.5 |
關鍵詞 | 即時型派翠網; 觸發序列圖; 行為分析; 時序驗證; Real time petri nets; Firing sequence graphs; Behavior analysis; Temporal verification; |
語文 | 英文(English) |
中文摘要 | 我們提出一個觸發序列圖的技術,用於分析由即時型派翠網描模的即時系統的運 作行為,以及驗證它的時序限制。觸發序列圖的技術使用即時型派翠網的局部結構,以局部 累積的機械化程序來推導觸發序列。在觸發序列推導上與派翠網語言技術相比,本技術可以 降低人的參與程度;與可達樹技術相比,可緩和狀態空間劇脹的問題。由觸發序列圖推導出之 觸發序列,含有詳細的觸發型態來提供豐富的觸發程序資訊,得據以有效地轉換觸發序列成 時序傳遞式來執行即時系統的各式時序驗證,包括動作觸發、執行期限、事件回應與觸發週 期等時限的時序驗證。基於以上的特色,觸發序列圖的技術在系統評估上要比傳統的派翠網語 言、可達樹、關聯矩陣、訊標轉移、或延伸狀態圖等技術要來得好。 |
英文摘要 | The Firing Sequence Graph (FSG) technique is proposed as a new technique to do behavior analysis and temporal verification of a system modeled by the real-time Petrinet model. It employs simple mechanical procedures to do analysis to reduce the involvement of human beings during firing sequence derivation. It derives firing sequences from local configurations by local sequence accumulation to alleviate the state-space explosion problem. It contains more transition sequencing information in a firing sequence. It allows the efficient derivation of temporal propagation expressions to do various temporal verification, including triggering, deadline, response, and period time constraints check against what the user specifies. All these features make the technique work better in system evaluation than traditional Petrinet languages, reachability tree analysis, incidence matrix technique. marking transition, or state graph technique. |
本系統之摘要資訊系依該期刊論文摘要之資訊為主。