Abstract
Order-reduction is a standard automated approximation technique for computer-aided design, analysis, and simulation of many classes of systems, from circuits to buildings. To be used as a sound abstraction for formal verification, a measure of the similarity of behavior must be formalized and computed, which we develop in a computational way for a class of asymptotic stable linear systems as the main contributions of this paper. We have implemented the order-reduction as a sound abstraction process through a source-to-source model transformation in the HyST tool and use SpaceEx to compute sets of reachable states to verify properties of the full-order system through analysis of the reduced-order system. Our experimental results suggest systems with thousand of state variables can be reduced to systems with tens of state variables such that the order-reduction overapproximation error is small enough to prove or disprove safety properties of interest using current reachability analysis tools. Our results illustrate this approach is effective in tackling the state-space explosion problem for verification of high-dimensional linear systems.
Original language | English (US) |
---|---|
Pages (from-to) | 443-461 |
Number of pages | 19 |
Journal | Discrete Event Dynamic Systems: Theory and Applications |
Volume | 27 |
Issue number | 2 |
DOIs | |
State | Published - Jun 1 2017 |
Externally published | Yes |
Keywords
- Abstraction
- Model reduction
- Order reduction
- Reachability analysis
- Verification
ASJC Scopus subject areas
- Control and Systems Engineering
- Modeling and Simulation
- Electrical and Electronic Engineering