Automated goal operationalisation based on interpolation and SAT solving
Automated goal operationalisation based on interpolation and SAT solving
复制标题
DOI：
10.1145/2568225.2568323
复制
发表时间：
2014-05
期刊：
影响因子：
--
通讯作者：
Renzo Degiovanni;Dalal Alrajeh;Nazareno Aguirre;Sebastián Uchitel
中科院分区：
文献类型：
--
作者：
Renzo Degiovanni;Dalal Alrajeh;Nazareno Aguirre;Sebastián Uchitel
在将目标分配给代理商时，已成功执行了目标方法，以启动和详细说明，必须通过适当的启用和触发条件来完善它们的操作：目标运营通常需要工程师的巨大努力。非正式或大多数半自动化，要求工程师在本文中提供帮助是迭代的，能够处理安全目标和特定种类的耐受性目标，并基于插值和SAT解决方案的使用。
Goal oriented methods have been successfully employed for eliciting and elaborating software requirements. When goals are assigned to an agent, they have to be operationalised: the agent’s operations have to be refined, by equipping them with appropriate enabling and triggering conditions, so that the goals are fulfilled. Goal operationalisation generally demands a significant effort of the engineer. Although there exist approaches that tackle this problem, they are either informal or at most semi automated, requiring the engineer to assist in the process. In this paper, we present an approach for goal operationalisation that automatically computes required preconditions and required triggering conditions for operations, so that the resulting operations establish the goals. The process is iterative, is able to deal with safety goals and particular kinds of liveness goals, and is based on the use of interpolation and SAT solving.