Formal Modeling and Analysis for Interactive Hybrid Systems
Ellen J. Bass (Systems and Information Engineering, University of Virginia),
Karen M. Feigh (School of Aerospace Engineering, Georgia Institute of
Technology),
Elsa Gunter (Department of Computer Science,
University of Illinois, Urbana-Champaign), and
John Rushby
4th International Workshop on Formal Methods for Interactive Systems:
FMIS 2011, Limerick, Ireland, 21 June 2011
Abstract
An effective strategy for discovering certain kinds of automation
surprise and other problems in interactive systems is to build models
of the participating (automated and human) agents and then explore all
reachable states of the composed system looking for divergences
between mental states and those of the automation. Various kinds of
model checking provide ways to automate this approach when the agents
can be modeled as discrete automata. But when some of the agents are
continuous dynamical systems (e.g., airplanes), the composed model is
a hybrid (i.e., mixed continuous and discrete) system and these are
notoriously hard to analyze.
We describe an approach for very abstract modeling of hybrid systems
using relational approximations and their automated analysis using
infinite bounded model checking supported by an SMT solver. When
counterexamples are found, we describe how additional constraints can
be supplied to direct counterexamples toward plausible scenarios that
can be confirmed in high-fidelity simulation. The approach is
illustrated though application to a known (and now corrected)
human-automation interaction problem in Airbus aircraft.
PDF
Slides
PDF
BibTeX Entry
@INPROCEEDINGS{Bass-etal:FMIS11,
AUTHOR = {Ellen J. Bass and Karen M. Feigh and Elsa Gunter
and John Rushby},
TITLE = {Formal Modeling and Analysis for Interactive Hybrid Systems},
BOOKTITLE = {Fourth International Workshop on Formal Methods for
Interactive Systems: {FMIS 2011}},
publisher = {},
SERIES = {Electronic Communications of the EASST},
VOLUME = 45,
YEAR = 2011,
ADDRESS = {Limerick, Ireland},
MONTH = jun
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page