Abstraction of Formal Models in Real-Time System Verification
Date Issued
2004
Date
2004
Author(s)
Wang, Szu-Yi
DOI
en-US
Abstract
抽象化技術在驗證的過程中扮演了可能非常重要的角色。隨著安全、正確系統的需求增加，自動驗證技術的研究也就重要了起來。模型檢驗是一個有效用來自動偵測有限狀態系統是否符合其功能要求的方法。然而過程中狀態空間的迅速膨脹卻限制了其可應用的領域。抽象化的技術就是用來解決這樣一個問題的方法。給定一個系統，抽象化的技巧把它對到了另一個有著較小可能狀態空間的模型去。我們顯示了使用區間分析的方法對變數值域做抽象的結果大致上是有效的減少了狀態數量。另外，一些抽象化的基本原理也被列了出來。
Abstraction is probably the most important technique for verification. As the systems needed to convince their correctness increase, automated verification becomes a more important research. Model checking is an efficient methodology for automatically deciding if a finite state program satisfies its specification. However, state space explosion limits the applicability of it. Abstraction provides one solution to fix this problem. For a given concrete program, abstraction is a mapping such that a smaller model would obtain. We show the consequence that using interval analysis for variable abstraction may be useful to reduce much state spaces. Some principles of abstraction interpretation are also read here.
Subjects
正規模型
抽象化
formal model
abstraction
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-93-R91921027-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):ca3fb17e81b759891db5a1e09d2a2a0a