Goal-conflict detection based on temporal satisfiability checking
File(s)
Accepted version
Author(s)
Degiovanni, R
Ricci, N
Alrajeh, D
Castro, P
Aguirre, N
Type
Conference Paper
Abstract
Goal-oriented requirements engineering approaches propose
capturing how a system should behave through the speci ca-
tion of high-level goals, from which requirements can then
be systematically derived. Goals may however admit subtle
situations that make them diverge, i.e., not be satis able
as a whole under speci c circumstances feasible within the
domain, called
boundary conditions
. While previous work al-
lows one to identify boundary conditions for con icting goals
written in LTL, it does so through a pattern-based approach,
that supports a limited set of patterns, and only produces
pre-determined formulations of boundary conditions.
We present a novel automated approach to compute bound-
ary conditions for general classes of con icting goals expressed
in LTL, using a tableaux-based LTL satis ability procedure.
A tableau for an LTL formula is a nite representation of
all
its satisfying models, which we process to produce boundary
conditions that violate the formula, indicating divergence
situations. We show that our technique can automatically
produce boundary conditions that are more general than
those obtainable through existing previous pattern-based
approaches, and can also generate boundary conditions for
goals that are not captured by these patterns.
capturing how a system should behave through the speci ca-
tion of high-level goals, from which requirements can then
be systematically derived. Goals may however admit subtle
situations that make them diverge, i.e., not be satis able
as a whole under speci c circumstances feasible within the
domain, called
boundary conditions
. While previous work al-
lows one to identify boundary conditions for con icting goals
written in LTL, it does so through a pattern-based approach,
that supports a limited set of patterns, and only produces
pre-determined formulations of boundary conditions.
We present a novel automated approach to compute bound-
ary conditions for general classes of con icting goals expressed
in LTL, using a tableaux-based LTL satis ability procedure.
A tableau for an LTL formula is a nite representation of
all
its satisfying models, which we process to produce boundary
conditions that violate the formula, indicating divergence
situations. We show that our technique can automatically
produce boundary conditions that are more general than
those obtainable through existing previous pattern-based
approaches, and can also generate boundary conditions for
goals that are not captured by these patterns.
Date Issued
2016-10-06
Date Acceptance
2016-07-21
Citation
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016, pp.507-518
ISBN
978-1-4503-3845-5
Publisher
ACM / IEEE
Start Page
507
End Page
518
Journal / Book Title
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering
Copyright Statement
© 2016 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ASE 2016, http://doi.acm.org/10.1145/2970276.2970349
Source
IEEE/ACM International Conference on Automated Software Engineering
Publication Status
Published
Start Date
2016-09-03
Finish Date
2016-09-07
Coverage Spatial
Singapore