Portal de Periódicos da CAPES

Combining Symbolic Runtime Enforcers for Cyber-Physical Systems

2017; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-67531-2_5

1611-3349

Björn Andersson, Sagar Chaki, Dionisio de Niz,

Real-Time Systems Scheduling

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.