一句话:利用反应式综合的可实现性提出更强的边界条件定义,显著减少目标冲突分析中需人工处理的边界条件。
需求规格中的目标冲突常通过边界条件来刻画,但已有自动识别方法产生的边界条件过多,且边界条件本身的定义过弱。本文提出“不可避免边界条件”(UBCs),借助反应式综合中的可实现性概念强化边界条件定义,从而筛选出真正不可回避的冲突条件。实验表明,UBCs 能非平凡地减少现有技术产生的边界条件数量。论文还将 UBCs 与反应式综合中用于反馈不可实现规格的概念(如反策略和不可实现核)联系起来,并展示其能为修复不可实现规格提供有针对性反馈。
Boundary conditions express situations under which requirements specifications conflict. They are used within a broader conflict management process to produce less idealized specifications. Several approaches have been proposed to identify boundary conditions automatically. Some introduce a prioritization criteria to reduce the number of boundary conditions presented to an engineer. However, identifying the few, relevant boundary conditions remains an open challenge. In this paper, we argue that one of the problems of the state of the art is with the definition of boundary condition itselfit is too weak. We propose a stronger definition which we refer to as Unavoidable Boundary Conditions (UBCs), which utilizes the notion of realizability in reactive synthesis. We show experimentally that UBCs non-trivially reduce the number of conditions produced by existing boundary condition identification techniques. We also relate UBCs to existing concepts in reactive synthesis used to provide feedback for unrealizable specifications (including counter-strategies and unrealizable cores). We then show that UBCs provide a targeted form of feedback for repairing unrealizable specifications.