Safety and Reachability Verification
| Autor: | Alex Devonport, Pierre-Jean Meyer, Murat Arcak |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Set (abstract data type)
Current (mathematics) Computer science Control theory Reachability TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science The Intersect Computation Component (UML) Sample (statistics) Time range Computer Science::Formal Languages and Automata Theory |
| Zdroj: | SpringerBriefs in Electrical and Computer Engineering ISBN: 9783030651091 |
| Popis: | In this chapter, we use reachability analysis to address the problem of verifying safety (to avoid a given set of unsafe states) and reachability specifications (to reach a given target set in finite time). A reachability specification is verified by computing a reachable set over-approximation and checking if it is contained entirely inside the target set. To evaluate a safety specification, we compute an approximation to the reachable tube over a given time range by computing reachable set over-approximations at a set of sample times. The safety specification is then satisfied if the approximation of the reachable tube does not intersect with the unsafe set. We use several of the methods in this book to compute the reachable set over-approximations and to compare their performance in terms of tightness and computation time. We first consider a safety specification for a tunnel diode oscillator which assures that the current through a sensitive component remains below a safe level. Then, we consider both a safety and a reachability specification for a quadrotor model, to verify if a given control policy safely brings the quadrotor to a specified height while avoiding large fluctuations. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|