東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Model-based Compositional Verificati...

Ren, Hao.

Linked to FindBook

Google Book

Amazon

博客來

Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems./
Author:	Ren, Hao.
Published:	Ann Arbor : ProQuest Dissertations & Theses, : 2018,
Description:	105 p.
Notes:	Source: Dissertation Abstracts International, Volume: 79-11(E), Section: B.
Contained By:	Dissertation Abstracts International79-11B(E).
Subject:	Electrical engineering. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10789047
ISBN:	9780438077003

Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems.
Ren, Hao.

Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems. - Ann Arbor : ProQuest Dissertations & Theses, 2018 - 105 p.

Source: Dissertation Abstracts International, Volume: 79-11(E), Section: B.

Thesis (Ph.D.)--Iowa State University, 2018.

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.

ISBN: 9780438077003Subjects--Topical Terms:

649834
Electrical engineering.

Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems.
LDR:03172nmm a2200301 4500 001 2200219
005 20181214130635.5
008 201008s2018 ||||||||||||||||| ||eng d
020 $a 9780438077003
035 $a (MiAaPQ)AAI10789047
035 $a (MiAaPQ)iastate:17241
035 $a AAI10789047
040 $a MiAaPQ $c MiAaPQ
100 1 $a Ren, Hao. $3 2131708
245 1 0 $a Model-based Compositional Verification Approaches and Tools Development for Cyber-physical Systems.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2018
300 $a 105 p.
500 $a Source: Dissertation Abstracts International, Volume: 79-11(E), Section: B.
500 $a Adviser: Ratnesh Kumar.
502 $a Thesis (Ph.D.)--Iowa State University, 2018.
520 $a 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.
520 $a 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.
590 $a School code: 0097.
650 4 $a Electrical engineering. $3 649834
690 $a 0544
710 2 $a Iowa State University. $b Electrical and Computer Engineering. $3 1018524
773 0 $t Dissertation Abstracts International $g 79-11B(E).
790 $a 0097
791 $a Ph.D.
792 $a 2018
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10789047