Unavoidable boundary conditions: a control perspective on goal conflicts
File(s)
Accepted version
Author(s)
Cirelli, Francisco
Alrajeh, Dalal
Uchitel, Sebastian
Type
Conference Paper
Abstract
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 itself—it 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.
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 itself—it 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.
Date Issued
2025
Date Acceptance
2024-07-02
Citation
Proceedings of the International Conference on Software Engineering, 2025, pp.380-391
ISBN
979-8-3315-0569-1
ISSN
1558-1225
Publisher
ACM / IEEE
Start Page
380
End Page
391
Journal / Book Title
Proceedings of the International Conference on Software Engineering
Copyright Statement
Copyright © 2025 IEEE. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Identifier
https://www.computer.org/csdl/proceedings-article/icse/2025/056900a380/215aWMI6maI
Source
2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)
Publication Status
Published
Start Date
2025-04-30
Finish Date
2025-05-03
Coverage Spatial
Ottawa, ON, Canada
Date Publish Online
2025