A Formal Semantics for Brahms
A Formal Semantics for Brahms
复制标题
勃拉姆斯的形式语义学
DOI：
10.1007/978-3-642-22359-4_18
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Michael Fisher
中科院分区：
文献类型：
--
作者：
Richard Stocker;M. Sierhuis;Louise Dennis;C. Dixon;Michael Fisher
计算过程的形式分析现在是一个很成熟的领域。然而，在实际场景中，我们如何正式验证与人类的交互的问题仍然存在。在本文中，我们关注的是解决这个问题。我们的总体目标是为人类代理团队合作提供正式的验证技术，特别是未来太空任务中的宇航员-机器人团队合作以及医疗保健场景中的人机交互。然而，为了进行我们的正式验证，我们必须首先为这个活动提供一些正式的基础。在本文中，我们通过详细介绍勃拉姆斯的正式操作语义来提供这一点，勃拉姆斯是人类代理团队合作的建模/仿真框架，已在NASA中开发并广泛使用。通过建立描述人类-代理团队合作的正式基础，这为我们的总体目标提供了第一步，但也是重要的一步，然后可以引导验证技术。
The formal analysis of computational processes is by now a wellestablished field. However, in practical scenarios, the problem of how we can formally verify interactions with humans still remains. In this paper we are concerned with addressing this problem. Our overall goal is to provide formal verification techniques for human-agent teamwork, particularly astronaut-robot teamwork on future space missions and human-robot interactions in health-care scenarios. However, in order to carry out our formal verification, we must first have some formal basis for this activity. In this paper we provide this by detailing a formal operational semantics for Brahms, a modelling/simulation framework for human-agent teamwork that has been developed and extensively used within NASA. This provides a first, but important, step towards our overall goal by establishing a formal basis for describing human-agent teamwork, which can then lead on to verification techniques.