Reasoning about safety of learning-enabled components in autonomous cyber-physical systems
| Autor: | Jyotirmoy V. Deshmukh, Hisahiro Ito, James Kapinski, Cumhur Erkan Tuncali |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
FOS: Computer and information sciences
0209 industrial biotechnology Level set (data structures) Linear programming Artificial neural network Computer Science - Artificial Intelligence Computer science Cyber-physical system Control engineering Systems and Control (eess.SY) 02 engineering and technology Solver Certificate Set (abstract data type) Artificial Intelligence (cs.AI) 020901 industrial engineering & automation 68N30 65G20 93C85 68T99 Satisfiability modulo theories FOS: Electrical engineering electronic engineering information engineering 0202 electrical engineering electronic engineering information engineering Computer Science - Systems and Control 020201 artificial intelligence & image processing |
| Zdroj: | DAC |
| DOI: | 10.1145/3195970.3199852 |
| Popis: | We present a simulation-based approach for generating barrier certificate functions for safety verification of cyber-physical systems (CPS) that contain neural network-based controllers. A linear programming solver is utilized to find a candidate generator function from a set of simulation traces obtained by randomly selecting initial states for the CPS model. A level set of the generator function is then selected to act as a barrier certificate for the system, meaning it demonstrates that no unsafe system states are reachable from a given set of initial states. The barrier certificate properties are verified with an SMT solver. This approach is demonstrated on a case study in which a Dubins car model of an autonomous vehicle is controlled by a neural network to follow a given path. Invited paper in conference: Design Automation Conference (DAC) 2018 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|