Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 2015
- Accession Number
- AD1006472
Entities
People
- Stanley Bak
- Taylor T. Johnson
Organizations
- Rome Laboratory