Model-based compositional verification approaches and tools development for cyber-physical systems

dc.contributor.advisor Ratnesh Kumar
dc.contributor.author Ren, Hao
dc.contributor.department Electrical and Computer Engineering
dc.date 2018-08-11T12:47:38.000
dc.date.accessioned 2020-06-30T03:11:08Z
dc.date.available 2020-06-30T03:11:08Z
dc.date.copyright Tue May 01 00:00:00 UTC 2018
dc.date.embargo 2001-01-01
dc.date.issued 2018-01-01
dc.description.abstract <p>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.</p> <p>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.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/etd/16444/
dc.identifier.articleid 7451
dc.identifier.contextkey 12331484
dc.identifier.doi https://doi.org/10.31274/etd-180810-6074
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/16444
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/30627
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/etd/16444/Ren_iastate_0097E_17241.pdf|||Fri Jan 14 21:00:28 UTC 2022
dc.subject.disciplines Electrical and Electronics
dc.subject.keywords Compositional reasoning
dc.subject.keywords Cyber-physical system
dc.subject.keywords Formal verification
dc.subject.keywords Quantifier elimination
dc.subject.keywords Reachability analysis
dc.title Model-based compositional verification approaches and tools development for cyber-physical systems
dc.type article
dc.type.genre dissertation
dspace.entity.type Publication
relation.isOrgUnitOfPublication a75a044c-d11e-44cd-af4f-dab1d83339ff
thesis.degree.discipline Electrical Engineering
thesis.degree.level dissertation
thesis.degree.name Doctor of Philosophy
File
Original bundle
Now showing 1 - 1 of 1
Name:
Ren_iastate_0097E_17241.pdf
Size:
2 MB
Format:
Adobe Portable Document Format
Description: