首页> 外文会议>Software engineering and formal methods >A Cognitive Framework Based on Rewriting Logic for the Analysis of Interactive Systems
【24h】

A Cognitive Framework Based on Rewriting Logic for the Analysis of Interactive Systems

机译:基于重写逻辑的交互式系统分析认知框架

获取原文
获取原文并翻译 | 示例

摘要

Interactive systems may appear to work correctly and safely when analysed in isolation from the human environment in which they are supposed to work. In fact, the same cognitive skills that enable humans to perform complex tasks may also become the source of critical errors in the interaction with systems and devices designed as supports for such tasks. It is thus essential to verify the desired properties of an interactive system using a model that not only includes a user-centered description of the task, but also incorporates a representation of human cognitive processes within the task execution. In this paper we consider automatic and deliberate cognitive processes in combination with the use of the Short Term Memory (STM), and provide a formal notation to model the set of basic tasks that a human component (user or operator) has to carry out to accomplish a goal by interacting with an interface. The semantics of the notation is given in terms of a cognitive framework that makes use of rules driven by the basic tasks to rewrite both the system state and the STM until all necessary tasks have been completed. Potential human errors are then detected using model checking. Our notation, which is implemented using the MAUDE rewrite system, and our formal verification methodology are finally illustrated by two case studies: a user of an Automatic Teller Machine (ATM) and an operator of an Air Traffic Control (ATC) system.
机译:如果将交互式系统与应该在其中工作的人类环境隔离开来进行分析,则它们似乎可以正确,安全地工作。实际上,使人类能够执行复杂任务的相同认知技能也可能成为与旨在支持此类任务的系统和设备进行交互时严重错误的来源。因此,至关重要的是使用一种模型来验证交互式系统的所需属性,该模型不仅包括以用户为中心的任务描述,而且还将人类认知过程的表示纳入任务执行过程中。在本文中,我们结合使用短期记忆(STM)来考虑自动和故意的认知过程,并提供正式的符号来建模人类组件(用户或操作员)必须执行的一组基本任务通过与界面交互来实现目标。该符号的语义是根据认知框架给出的,该认知框架利用基本任务驱动的规则来重写系统状态和STM,直到完成所有必要任务为止。然后使用模型检查来检测潜在的人为错误。最后,我们通过两个案例研究来说明我们使用MAUDE重写系统实现的符号和我们的正式验证方法:自动柜员机(ATM)的用户和空中交通管制(ATC)系统的操作员。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号