首页    期刊浏览 2024年12月04日 星期三
登录注册

文章基本信息

  • 标题:Formal Modeling and Analysis for Interactive Hybrid Systems
  • 本地全文:下载
  • 作者:Ellen J Bass ; Karen M Feigh ; Elsa Gunter
  • 期刊名称:Electronic Communications of the EASST
  • 电子版ISSN:1863-2122
  • 出版年度:2011
  • 卷号:45
  • 语种:English
  • 出版社:European Association of Software Science and Technology (EASST)
  • 摘要: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.
国家哲学社会科学文献中心版权所有