Information Technology Reference
In-Depth Information
context),
c
(p) is added separately in the BNF specification, via q, and every w can either
be x or q. Every y represents a complex statement as a formula with conjunction and
implication such that y can be either w or
⊥
, where w is some requirement in a context
propositions and
refers to logical inconsistency. We can then rewrite
φ
as a complex
statement consists of either w or
k
⊥
(
y
)
(
y
)
or
c
.
Definition 6.
Consequence relation of Techne in context:
Let
Π
⊆L
SAS
,
φ
∈L
SAS
,
and
z
∈{
φ,
⊥}
, then:
1.
Π
|
cτ
φ
if
φ
∈
Π
,or
(
i
=1
2.
Π
|
cτ
z
if
∀
1
≤
i
≤
n
,
Π
|
cτ
φ
i
and
k
φ
i
→
z
)
∈
Π
.
The consequence relation
|
cτ
is sound w.r.t. standard entailment in propositional logic.
It deduces only positive statement by being paraconsistent, thus all admissible candi-
date solutions are found via paraconsistent and non-monotonic reasoning. Reasoning
is paraconsistent because an inconsistent
Δ
or
C
should not allow us to conclude the
satisfaction of all requirements therein; it is non-monotonic in that prior conclusions
drawn from a
Δ
or a
C
may be retracted after new requirements are introduced.
We also need a function that tells us which contexts a requirement applies to.
Definition 7.
Contextualization function:
Let
C
be the set of all contexts.
C
:
℘
(
L
SAS
)
(where
℘
returns the powerset) is called the contextualization function that
for a given set of formulas returns the set of contexts to which these formulas apply to.
By “apply to”, we mean that
C
−→
℘
(
C
)
∈C
(
φ
)
iff the following conditions are satisfied:
1.
C, φ
, i.e.,
φ
is not inconsistent with context
C
,
2.
C
is such that
|
τ
⊥
∃
X
⊆
Δ
such that
C, X
|
τ
φ
, i.e., the context
C
together with some
requirements
X
from
Δ
lets us deduce
φ
.
Several remarks are in order. Firstly, with
L
SAS
, we now have a new sort for expressions
that are members of a set that defines a context. Recall that we defined an instance
C
of
Context
as a set of information, so that now
L
SAS
tells us that one member of that set can
either be a proposition
p
, denoted
c
(
p
)
, or can be a formula with implication, denoted
(
y
)
c
in the
BNF
specification. E.g., if the engineer assumes that the stakeholders wants
that her goal
g
for “arrive at destination” be satisfied both in the context
C
1
in which
the context proposition “
c
(
p
)
(
q
)
: flight is on time” holds (i.e.,
c
(
q
)
∈
C
1
), and in the
context
C
2
in which the context proposition “
c
(
r
)
: flight is delayed but not more than
5 hours” holds (i.e.,
c
.
Secondly, observe that the
BNF
specification lets us write formulas in which we com-
bine context propositions and requirements, e.g.:
k
(
r
)
∈
C
2
), then
C
1
∈C
(
(
p
))
and
C
1
∈C
(
(
p
))
g
g
(
p
)
∧
(
q
)
→⊥
, which the require-
c
ments engineer can use to state that the domain assumption
k
that was communicated
by the stakeholder does not hold in contexts in which the context proposition
c
(
p
)
holds.
Since we can combine context formulas and requirements, we can state very useful
relations, such as that some requirements conflict with some contexts, by saying that
these requirements are inconsistent with some of the context formulas in these contexts.
As an aside, rules that connect requirements and context formulas need not be specified
in a definite way by the requirements engineer. It is also possible to learn them by
asking feedback to the user i.e. a SAS at runtime can perform this task. For example,
(
q
)
