東華大學圖書館 |

語系: 繁體中文

說明(常見問題)

回圖書館首頁

手機版館藏查詢

登入

回首頁

切換: 標籤 | MARC模式 | ISBD

Algorithms and Data Structures for E...

Zhang, Yingying.

FindBook

Google Book

Amazon

博客來

Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems.

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems./
作者:	Zhang, Yingying.
面頁冊數:	72 p.
附註:	Source: Masters Abstracts International, Volume: 52-01.
Contained By:	Masters Abstracts International52-01(E).
標題:	Computer engineering. -
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=1539501
ISBN:	9781303150326

Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems.
Zhang, Yingying.

Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems. - 72 p.

Source: Masters Abstracts International, Volume: 52-01.

Thesis (M.S.Cp.)--University of South Florida, 2013.

This thesis presents a framework to verify asynchronous real-time systems based on model checking. These systems are modeled by using a common modeling formalism named Labeled Petri-nets(LPNs).

ISBN: 9781303150326Subjects--Topical Terms:

621879
Computer engineering.

Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems.
LDR:02653nmm a2200301 4500 001 2069799
005 20160524150659.5
008 170521s2013 ||||||||||||||||| ||eng d
020 $a 9781303150326
035 $a (MiAaPQ)AAI1539501
035 $a AAI1539501
040 $a MiAaPQ $c MiAaPQ
100 1 $a Zhang, Yingying. $3 1975814
245 1 0 $a Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems.
300 $a 72 p.
500 $a Source: Masters Abstracts International, Volume: 52-01.
500 $a Adviser: Hao Zheng.
502 $a Thesis (M.S.Cp.)--University of South Florida, 2013.
520 $a This thesis presents a framework to verify asynchronous real-time systems based on model checking. These systems are modeled by using a common modeling formalism named Labeled Petri-nets(LPNs).
520 $a In order to verify the real-time systems algorithmically, the zone-based timing analysis method is used for LPNs. It searches the state space with timing information (represented by zones). When there is a high degree of concurrency in the model, firing concurrent enabled transitions in different order may result in different zones, and these zones may be combined without affecting the verification result. Since the zone-based method could not deal with this problem efficiently, the POSET timing analysis method is adopted for LPNs. It separates concurrency from causality and generates an exactly one zone for a single state. But it needs to maintain an extra POSET matrix for each state. In order to save time and memory, an improved zone-based timing analysis method is introduced by integrating above two methods. It searches the state space with zones but eliminates the use of the POSET matrix, which generates the same result as with the POSET method. To illustrate these methods, a circuit example is used throughout the thesis.
520 $a Since the state space generated is usually very large, a graph data structure named multi-value decision diagrams (MDDs) is implemented to store the zones compactly. In order to share common clock value of different zones, two zone encoding methods are described: direct encoding and minimal constraint encoding. They ignore the unnecessary information in zones thus reduce the length of the integer tuples. The effectiveness of these two encoding methods is demonstrated by experimental result of the circuit example.
590 $a School code: 0206.
650 4 $a Computer engineering. $3 621879
650 4 $a Computer science. $3 523869
690 $a 0464
690 $a 0984
710 2 $a University of South Florida. $b Engineering. $3 1680322
773 0 $t Masters Abstracts International $g 52-01(E).
790 $a 0206
791 $a M.S.Cp.
792 $a 2013
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=1539501