Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization
Air Force Research Laboratory/Information Directorate ROME United States
Pagination or Media Count:
Cyber-physical systems CPS consist of physical entities that obey dynamical laws and interact with software components. A typical CPS implementation includes a discrete controller, where software periodically samples physical state and produces actuation commands according to a real-time schedule. Such a hybrid system can be modeled formally as a hybrid automaton. However, reachability tools to verify specifications for hybrid automata do not perform well on such periodically scheduled models. This is due to a combination of the large number of discrete jumps and the nondeterminism of the exact controller start time. In this paper, we demonstrate this problem and propose a solution, which is a validated abstraction mechanism where every behavior of the original sampled system is contained in the behaviors of a purely continuous system withan additive nondeterministic input. Reachability tools for hybrid automata can better handle such systems. We further improve the analysis by considering local analysis domains. We automate the proposed technique in the Hyst model transformation tool,and demonstrate its effectiveness in a case study analyzing thedesign of a yaw-damper for a jet aircraft.