Coho : a verification tool for circuit verification by reachability analysis
COHO is a verification tool for systems modeled by nonlinear ordinary differential equations (ODEs). Verification is performed using reachability analysis. The reachable space is represented by projectagons which are the polyhedron described by their projection onto two dimensional subspace. COHO ap...
Main Author: | |
---|---|
Language: | English |
Published: |
2010
|
Online Access: | http://hdl.handle.net/2429/18181 |
id |
ndltd-UBC-oai-circle.library.ubc.ca-2429-18181 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-UBC-oai-circle.library.ubc.ca-2429-181812018-01-05T17:39:21Z Coho : a verification tool for circuit verification by reachability analysis Coho : a verification tool for circuit verification by reachability analysis Yan, Chao COHO is a verification tool for systems modeled by nonlinear ordinary differential equations (ODEs). Verification is performed using reachability analysis. The reachable space is represented by projectagons which are the polyhedron described by their projection onto two dimensional subspace. COHO approximates nonlinear ODEs with linear differential inclusions to compute the reachable state. We re-engineer the COHO system to provide a robust implementation with a clear interface and well-organized structure. We demonstrate the soundness and robustness of our approach by applying it to several examples, including a three dimensional, non-linear systems for which previous version of COHO failed due to numerical stability problems. The correctness of COHO strongly depends on the accuracy, efficiency and robustness of the linear program solver that is used throughout the analysis. Our COHO linear program solver is implemented by integrating the Simplex algorithm with interval arithmetic based on the framework set up by Laza [Laz01]. For highly ill-conditioned problems, an approximation that is very close to the optimal result is computed by our algorithm. This results in a very small error bound that allows COHO to successfully verify interesting examples. This thesis also presents an algorithm to solve the problem of projecting the feasible region of a linear program onto two dimensional subspaces. This algorithm uses the COHO linear program solver for efficiency and accuracy. We derive an analytical upper bound for the error and present experimental results to show that the errors are negligible in practice. Science, Faculty of Computer Science, Department of Graduate 2010-01-16T16:24:39Z 2010-01-16T16:24:39Z 2006 2006-11 Text Thesis/Dissertation http://hdl.handle.net/2429/18181 eng For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
collection |
NDLTD |
language |
English |
sources |
NDLTD |
description |
COHO is a verification tool for systems modeled by nonlinear ordinary differential equations (ODEs). Verification is performed using reachability analysis. The reachable space is represented by projectagons which are the polyhedron described by their projection onto two dimensional subspace. COHO approximates nonlinear ODEs with linear differential inclusions to compute the reachable state. We re-engineer the COHO system to provide a robust implementation with a clear interface and well-organized structure. We demonstrate the soundness and robustness of our approach by applying it to several examples, including a three dimensional, non-linear systems for which previous version of COHO failed due to numerical stability problems. The correctness of COHO strongly depends on the accuracy, efficiency and robustness of the linear program solver that is used throughout the analysis. Our COHO linear program solver is implemented by integrating the Simplex algorithm with interval arithmetic based on the framework set up by Laza [Laz01]. For highly ill-conditioned problems, an approximation that is very close to the optimal result is computed by our algorithm. This results in a very small error bound that allows COHO to successfully verify interesting examples. This thesis also presents an algorithm to solve the problem of projecting the feasible region of a linear program onto two dimensional subspaces. This algorithm uses the COHO linear program solver for efficiency and accuracy. We derive an analytical upper bound for the error and present experimental results to show that the errors are negligible in practice. === Science, Faculty of === Computer Science, Department of === Graduate |
author |
Yan, Chao |
spellingShingle |
Yan, Chao Coho : a verification tool for circuit verification by reachability analysis |
author_facet |
Yan, Chao |
author_sort |
Yan, Chao |
title |
Coho : a verification tool for circuit verification by reachability analysis |
title_short |
Coho : a verification tool for circuit verification by reachability analysis |
title_full |
Coho : a verification tool for circuit verification by reachability analysis |
title_fullStr |
Coho : a verification tool for circuit verification by reachability analysis |
title_full_unstemmed |
Coho : a verification tool for circuit verification by reachability analysis |
title_sort |
coho : a verification tool for circuit verification by reachability analysis |
publishDate |
2010 |
url |
http://hdl.handle.net/2429/18181 |
work_keys_str_mv |
AT yanchao cohoaverificationtoolforcircuitverificationbyreachabilityanalysis |
_version_ |
1718590750200954880 |