Formal Modeling and Analysis for Interactive Hybrid Systems - Bass, Ellen; Feigh, Karen; Gunter, Elsa; Rushby, John (Electronic Communications of the EASST, 2011)
An effective strategy for discovering certain kinds of automationsurprise and other problems in interactive systems is to build modelsof the participating (automated and human) agents and then explore allreachable states of the composed system looking for divergencesbetween mental states and those of the automation. Various kinds ofmodel checking provide ways to automate this approach when the agentscan be modeled as discrete automata. But when some of the agents arecontinuous dynamical systems (e.g., airplanes), the composed model isa hybrid (i.e., mixed continuous and discrete) system and these arenotoriously hard to analyze.We describe an approach for very abstract modeling of hybrid systemsusing relational approximations and their automated analysis usinginfinite bounded model checking supported by an SMT solver. Whencounterexamples are found, we describe how additional constraints canbe supplied to direct counterexamples toward plausible scenarios thatcan be confirmed in high-fidelity simulation. The approach isillustrated though application to a known (and now corrected)human-automation interaction problem in Airbus aircraft.