Compositional bounded reachability using time partitioning and abstraction

Green, Jeremy

Permalink

https://hdl.handle.net/2142/34351 Copy

Description

Title

Compositional bounded reachability using time partitioning and abstraction

Author(s)

Green, Jeremy

Issue Date

2012-09-18T21:12:45Z

Director of Research (if dissertation) or Advisor (if thesis)

Mitra, Sayan

Department of Study

Electrical & Computer Eng

Discipline

Electrical & Computer Engr

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

M.S.

Degree Level

Thesis

Keyword(s)

• bounded reachability
• decomposition
• composition
• hybrid system
• abstraction
• safety verification

Abstract

Automatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction.

Graduation Semester

2012-08

Permalink

http://hdl.handle.net/2142/34351

Copyright and License Information

Copyright 2012 Jeremy Green

Owning Collections