Combining Symbolic Runtime Enforcers for Cyber-Physical Systems
| Autor: | Björn Andersson, Dionisio de Niz, Sagar Chaki |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Set (abstract data type)
Prioritization 021110 strategic defence & security studies Theoretical computer science Speedup Computer science 0211 other engineering and technologies 0202 electrical engineering electronic engineering information engineering Cyber-physical system 020207 software engineering 02 engineering and technology Formal description Satisfiability |
| Zdroj: | Runtime Verification ISBN: 9783319675305 RV |
| DOI: | 10.1007/978-3-319-67531-2_5 |
| Popis: | The problem of composing multiple, possibly conflicting, runtime enforcers for a cyber-physical system (CPS) is considered. A formal definition of utility-agnostic and utility-maximizing CPS enforcers is presented, followed by an algorithm to combine multiple enforcers, and resolve their conflicts based on a design-time prioritization. To implement this combination in an efficient manner, enforcers are encoded symbolically using SMT formulas, and the combination is reduced to a set of SMT satisfiability and optimization operations. Further performance gains are achieved by using the SMT solvers incrementally. The approach is validated via experiments in an indoor area with Parrot minidrones. The incremental enforcer combination is shown to achieve an order of magnitude speedup, and no deadline misses. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|