1 Self-explaining Digital Systems
9
Fig. 1.2 Implementation
FU1
EU1
FU2
a
c
t
explanation unit. The explanation unit then provides unique tags for the action to
form an event, merges it with the cause, and stores the resulting explanation. Other
functional units query the explanation unit to associate incoming data with an event
and its explanation. This information must then be passed jointly while processing
the data to provide the causes for an action. Figure 1.2 illustrates this. Functional
unit FU1 executes an action a passed to functional unit FU2. The cause c of a is
stored in explanation unit EU1 that provides a unique tag t. FU2 refers to the event
(a, t) to derive causes for its own actions.
For this step we rely on the designer to enhance the implementation with
functionality to pass causes and drive explanation units by adding appropriate code.
The designer also decides whether actions are defined in terms of existing variables
of the design or whether new variables are introduced to allow for abstraction.
1.3.3 Verification and Validation
Validating and verifying the semantics of the explanations requires consistency
checks with the actual design and observing whether explanations fit the actual
behavior in the environment. This is difficult to automate as a precise environment
model is required. However, given a digital system we can analyze whether it is
self-explaining according to Definition 1.6. This analysis can either be applied to
validate an execution trace or to formally verify self-explanation of a system. The
analysis proceeds in the following steps:
1. Check whether the set of observable actions is complete (see Definition 1.4).
Without any abstraction in the explanations any change in output values must
be an action. If abstraction is used, the output values corresponding to each
observable action must be precisely specified.
2. Check whether the explanations are well-formed (see Definition 1.3).
A directed graph is built containing all explanations where nodes represent events
and incoming edges start at the causes. If there is a node in the graph without
predecessors, this node must represent an input action or a requirement.
3. Check whether the explanations are complete (see Definition 1.5).
Upon the first occurrence of output values belonging to a particular action an
explanation must be produced by the system.
9
Fig. 1.2 Implementation
FU1
EU1
FU2
a
c
t
explanation unit. The explanation unit then provides unique tags for the action to
form an event, merges it with the cause, and stores the resulting explanation. Other
functional units query the explanation unit to associate incoming data with an event
and its explanation. This information must then be passed jointly while processing
the data to provide the causes for an action. Figure 1.2 illustrates this. Functional
unit FU1 executes an action a passed to functional unit FU2. The cause c of a is
stored in explanation unit EU1 that provides a unique tag t. FU2 refers to the event
(a, t) to derive causes for its own actions.
For this step we rely on the designer to enhance the implementation with
functionality to pass causes and drive explanation units by adding appropriate code.
The designer also decides whether actions are defined in terms of existing variables
of the design or whether new variables are introduced to allow for abstraction.
1.3.3 Verification and Validation
Validating and verifying the semantics of the explanations requires consistency
checks with the actual design and observing whether explanations fit the actual
behavior in the environment. This is difficult to automate as a precise environment
model is required. However, given a digital system we can analyze whether it is
self-explaining according to Definition 1.6. This analysis can either be applied to
validate an execution trace or to formally verify self-explanation of a system. The
analysis proceeds in the following steps:
1. Check whether the set of observable actions is complete (see Definition 1.4).
Without any abstraction in the explanations any change in output values must
be an action. If abstraction is used, the output values corresponding to each
observable action must be precisely specified.
2. Check whether the explanations are well-formed (see Definition 1.3).
A directed graph is built containing all explanations where nodes represent events
and incoming edges start at the causes. If there is a node in the graph without
predecessors, this node must represent an input action or a requirement.
3. Check whether the explanations are complete (see Definition 1.5).
Upon the first occurrence of output values belonging to a particular action an
explanation must be produced by the system.