Eylem Seç
Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems
Başlık:
Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems
Yazar:
Ren, Hao, author. (orcid)0000-0001-7101-6120
ISBN:
9780438077003
Yazar Ek Girişi:
Fiziksel Tanımlama:
1 electronic resource (105 pages)
Genel Not:
Source: Dissertation Abstracts International, Volume: 79-11(E), Section: B.
Advisors: Ratnesh Kumar Committee members: Samik Basu; Gianfranco Ciardo; Manimaran Govindarasu; Joseph Zambreno.
Özet:
The model-based design for embedded real-time systems utilizes the veriable reusable components and proper architectures, to deal with the verification scalability problem caused by state-explosion. In this thesis, we address verification approaches for both low-level individual component correctness and high-level system correctness, which are equally important under this scheme. Three prototype tools are developed, implementing our approaches and algorithms accordingly.
For the component-level design-time verification, we developed a symbolic verifier, LhaVrf, for the reachability verification of concurrent linear hybrid systems (LHA). It is unique in translating a hybrid automaton into a transition system that preserves the discrete transition structure, possesses no continuous dynamics, and preserves reachability of discrete states. Afterward, model-checking is interleaved in the counterexample fragment based specification relaxation framework. We next present a simulation-based bounded-horizon reachability analysis approach for the reachability verification of systems modeled by hybrid automata (HA) on a run-time basis. This framework applies a dynamic, on-the-fly, repartition-based error propagation control method with the mild requirement of Lipschitz continuity on the continuous dynamics. The novel features allow state-triggered discrete jumps and provide eventually constant over-approximation error bound for incremental stable dynamics. The above approaches are implemented in our prototype verifier called HS3V. Once the component properties are established, the next thing is to establish the system-level properties through compositional verication. We present our work on the role and integration of quantier elimination (QE) for property composition and verication. In our approach, we derive in a single step, the strongest system property from the given component properties for both time-independent and time-dependent scenarios. The system initial condition can also be composed, which, alongside the strongest system property, are used to verify a postulated system property through induction. The above approaches are implemented in our prototype tool called ReLIC.
Notlar:
School code: 0097
Konu Başlığı:
Tüzel Kişi Ek Girişi:
Mevcut:*
Yer Numarası | Demirbaş Numarası | Shelf Location | Lokasyon / Statüsü / İade Tarihi |
---|---|---|---|
XX(690124.1) | 690124-1001 | Proquest E-Tez Koleksiyonu | Arıyor... |
On Order
Liste seç
Bunu varsayılan liste yap.
Öğeler başarıyla eklendi
Öğeler eklenirken hata oldu. Lütfen tekrar deneyiniz.
:
Select An Item
Data usage warning: You will receive one text message for each title you selected.
Standard text messaging rates apply.