跳到主要內容

臺灣博碩士論文加值系統

(44.222.218.145) 您好!臺灣時間:2024/03/04 17:56
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:林聖博
研究生(外文):Lin, Sam S-B
論文名稱:派翠網路與時序邏輯的整合應用
論文名稱(外文):An Integrated Combination of Temporal logic and Petri nets
指導教授:楊鎮華, 李允中
指導教授(外文):Stephen Yang, Jonathan Lee
學位類別:碩士
校院名稱:國立中央大學
系所名稱:資訊工程研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:1998
畢業學年度:86
語文別:中文
論文頁數:75
中文關鍵詞:正規化方法派翠網路時序派翠網路可到達狀態樹邏輯
外文關鍵詞:Formal methodPetri netsTime Petri netsReachability tree logic
相關次數:
  • 被引用被引用:0
  • 點閱點閱:198
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
論文題目: 派翠網路與時序邏輯的整合應用. 論文的目的: 提供一個正規
化的方法以便從時序的觀點來描述及驗證分散式即時系統. 論文的研究方
法: 使用時序派翠網路來模組即時系統. 對於任意的時序派翠網路, 我們
提供了一個決策程序來查核一些小型但是重要的性質類 (這些性質類以可
到達狀態樹邏輯來描述) . 這些性質類包括必然性, 直到性和不變性質
等. 我們整合時序派翠網路和可到達狀態樹邏輯, 並且已經使用 Java
applet完成一個可以進行模組及驗證的工具. 此工具可以透過瀏覽器 (諸
如Necape等) 經由網路來實現. (其IP位址為http://140.115.50.137)
論文的研究內容: 目前派翠網路已經廣泛使用於模組和分析即時系統的同
時性與同步性. 並且可以利用派翠網路模擬系統中的動態行為. 另外可以
由派翠網路上分析很多的行為性質. 但是派翠網路沒有提供任何可以描述
系統中有關抽象化的時序行為, 諸如必然性 (eventually) 和直到性
(until)等等. 因此若單獨使用派翠網路來進行系統驗證的工作時則會有
不足的地方, 所以利用時序邏輯來描述系統中的時序行為以彌補派翠網路
不足的地方. 目前我們已經完成一個模組和驗證的工具, 在論文中, 我們
將含有迴路結構的派翠網路所造成的無限條執行序列對映到有限條的執行
序列, 然後利用有限條的執行序列來進行系統的驗證工作. 一旦有限的基
本執行序列被建立後, 則驗證時所需的複雜度將會大大的減少, 這是因為
原本要驗證的對象為無限多組的執行序列, 如今只需驗證有限組的執行序
列. 在論文中, 可以歸納出系統驗證的步驟如下: 首先利用時序派翠網路
模組系統的規格需求, 接著審查此網路是否具有局限性, 以便確保系統往
後在執行時, 不會產生溢位的情形. 接著建構網路的可到達狀態樹. 在建
構完成後, 利用可到達狀態樹邏輯描述系統中不變的性質, 最後驗證所模
組的網路是否具有用可到達狀態樹邏輯所描述的系統性質. 論文的研究結
果: 經由整合派翠網路和時序邏輯,可以降低分析時的複雜度並且可以提
高描述系統的能力.

In the paper our goal is to provide a formal method for
specifying and verifying distributed real-time systems from the
time perspective. We use time Petri nets to model real-time
systems and use decision procedures to check a small but
important class of properties(specified in reachability tree
logic). The class of properties includes eventually, until, and
invariants. We integrate time Petri nets and reachability tree
logic, and have used Java applet to finish a tool to model and
verify a real-time system. The tool can be implemented through
the WWW server(such as Nescape), its IP address is
http://140.115.50.137.Petri nets are widely used to model and
analyze certain aspects of synchronization and concurrency in
real-time systems. We can use Petri nets to simulate the dynamic
behaviors int a system, and many behavior properties in a system
can be studied with a Petri-net model. But Petri nets are
neither convenient nor powerful enough for representing the
temporal behaviors in a system such as eventually(certain places
must eventually have tokens) and until(certain placeshave tokens
until certain transitions fire). Only use Petri nets to verify a
system specification requirements is not enough, so we use the
temporal logic to represent such abstract temporal behaviors. We
have already finished a tool called NCUPN to model and analysis.
In the paper, we construct a set of finite number firing
sequencesfor a Petri net with the loop structure. Once the
primitives can be constructed, the complexity of verification
can be reduced dramatically because the verification is now
against a finite set instead of an infinite set of firing
sequences. Our verification algorithm is: 1.(Modeling step)
Given a real-time system S, construct the corresponding time
Petri net N; 2.Examine whether N is bounded; 3.Compute the
reachability tree Ts of N; 4.Specify the formulas Ps in RTL that
describes that S must satisfy; 5.Apply the appropriate decision
procedure for Ps. All decision procedures perform an analysis of
the reachability tree Ts. Through the integration, we can reduce
the analysis complexity and increase the expression power with
respect to the "time".

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top