4
G. Fey and R. Drechsler
Understanding why some task cannot be solved is more difficult. Proofs [13, 35],
unsatisfiable cores [30], or Craig-interpolants [15] provide natural explanations.
Proofs provide a natural explanation why something is not possible [13, 35];
unsatisfiable cores [30] (in particular, if all minimal unsatisfiable cores are available [20]) provide a cause for unsatisfiability; Craig-interpolants focus on the
interface between parts of the system to provide a cause; for design debugging
interpolants [15] and particularly sequence interpolants provide a stepwise explanation [37] converging to unsatisfiability.
Understanding complex programs is a tedious task requiring tool support [34].
One example is the analysis of data-flow in programs and of root causes for
certain output. Static [33] and dynamic [17] slicing show how specific data has
been produced by a program. This can, e.g., be used for debugging [36]. Dynamic
dependency graphs track the behavior, e.g., to extract formal properties [24].
Debugging circuits is hard due to the lack of observability into a chip. Trace
buffers provide an opportunity to record internal signals [6]. The careful selection of
signals [23] and their processing allows to reconstruct longer traces. The abstraction
level of trace buffers is exactly at the bit-level implementation of the digital system.
Restricted storage capacity limits the recorded history and number of signals being
traced. Coupling with software extensions allows to much more accurately pin point
time windows for recording [21].
Verification and in particular formal verification requires a deep understanding
of a system’s functionality. Model checking [4] is a well-established and automated
approach for formal verification. Typically, logic languages like Linear Temporal
Logic (LTL), Computation Tree Logic (CTL), or System Verilog Assertions (SVA)
are used to express properties that are then verified. Today’s verification languages
like System Verilog Assertions (SVA) are more expressive to allow for “nicer”
formulation of properties. These properties summarize the functionality of a design
in a different way and thus explain the behavior. Verification methodology [1, 2]
ensures that properties capture an abstraction rather than the technical details of an
implementation.
Beyond pure design time verification is the idea of proof carrying code to allow
for a simplified online verification before execution [29].
Self-awareness of computing systems [16] on various levels has been proposed
as a concept to improve online adaption and optimization. Application areas range
from hardware level to coordination of production processes, e.g., [28, 32]. The
information extracted for self-awareness relates to explanation usually focused
towards a specific optimization goal.
While all these aspects relate to explanation, self-explanation has been rarely
discussed. For organic computing, self-explanation has been postulated as a useful
concept for increasing acceptance by users [27]. The human-oriented aspect has
intensively been studied in intelligent human computer interfaces and support systems [25]. Self-explanation has also been proposed for software systems although
limited to the narrow domain of agent-based software [8] and mainly been studied
in the form of ontologies for information retrieval [9]. Expert systems as one very
relevant domain in artificial intelligence formalize and reason on knowledge within a
G. Fey and R. Drechsler
Understanding why some task cannot be solved is more difficult. Proofs [13, 35],
unsatisfiable cores [30], or Craig-interpolants [15] provide natural explanations.
Proofs provide a natural explanation why something is not possible [13, 35];
unsatisfiable cores [30] (in particular, if all minimal unsatisfiable cores are available [20]) provide a cause for unsatisfiability; Craig-interpolants focus on the
interface between parts of the system to provide a cause; for design debugging
interpolants [15] and particularly sequence interpolants provide a stepwise explanation [37] converging to unsatisfiability.
Understanding complex programs is a tedious task requiring tool support [34].
One example is the analysis of data-flow in programs and of root causes for
certain output. Static [33] and dynamic [17] slicing show how specific data has
been produced by a program. This can, e.g., be used for debugging [36]. Dynamic
dependency graphs track the behavior, e.g., to extract formal properties [24].
Debugging circuits is hard due to the lack of observability into a chip. Trace
buffers provide an opportunity to record internal signals [6]. The careful selection of
signals [23] and their processing allows to reconstruct longer traces. The abstraction
level of trace buffers is exactly at the bit-level implementation of the digital system.
Restricted storage capacity limits the recorded history and number of signals being
traced. Coupling with software extensions allows to much more accurately pin point
time windows for recording [21].
Verification and in particular formal verification requires a deep understanding
of a system’s functionality. Model checking [4] is a well-established and automated
approach for formal verification. Typically, logic languages like Linear Temporal
Logic (LTL), Computation Tree Logic (CTL), or System Verilog Assertions (SVA)
are used to express properties that are then verified. Today’s verification languages
like System Verilog Assertions (SVA) are more expressive to allow for “nicer”
formulation of properties. These properties summarize the functionality of a design
in a different way and thus explain the behavior. Verification methodology [1, 2]
ensures that properties capture an abstraction rather than the technical details of an
implementation.
Beyond pure design time verification is the idea of proof carrying code to allow
for a simplified online verification before execution [29].
Self-awareness of computing systems [16] on various levels has been proposed
as a concept to improve online adaption and optimization. Application areas range
from hardware level to coordination of production processes, e.g., [28, 32]. The
information extracted for self-awareness relates to explanation usually focused
towards a specific optimization goal.
While all these aspects relate to explanation, self-explanation has been rarely
discussed. For organic computing, self-explanation has been postulated as a useful
concept for increasing acceptance by users [27]. The human-oriented aspect has
intensively been studied in intelligent human computer interfaces and support systems [25]. Self-explanation has also been proposed for software systems although
limited to the narrow domain of agent-based software [8] and mainly been studied
in the form of ontologies for information retrieval [9]. Expert systems as one very
relevant domain in artificial intelligence formalize and reason on knowledge within a