1 Self-explaining Digital Systems
17
There are no other possible output assignments (again skipping the initial output
value):
AX(AG((speed_left[7:0]=255 ∧ speed_right[7:0]=255
∧ direction_right=fwd ∧ direction_left=fwd)
∨ ( ((direction_right=bwd ∧ direction_left=fwd)
∨ ( direction_right=fwd ∧ direction_left=bwd))
∧ speed_left[7:0]=5 ∧ speed_right[7:0]=5 )
∨ (direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=245 ∧ speed_right[7:0]=255)
∨ (direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=255 ∧ speed_right[7:0]=245)))
Check 2 This check is trivial for the main module since each explanation immediately refers to preceding modules and requirements only, but not to an internal
state.
Check 3 Whenever we transition from one action to another, a new explanation
is produced. Indeed we prove that certain output values also imply a certain action
encoded in the explanation, i.e., the ←-direction of the properties in Check 1. This
implies that a transition also causes a new explanation.
1.5 Future Extensions
The proposed formalization of self-explanation has some limitations that may be
waived. Moreover, in a practical setting automation is needed to add self-explanation
to an existing system.
1.5.1 Extending Explanations
Currently, an action is defined to be a variable assignment. In practice, more
complex actions may be of interest, e.g., to perform a burst access to a communication resource. Appropriate extensions are possible by allowing for a more general
specification of an action, e.g., in terms of a formal property language that describes
conditional sequential traces.
We propose completeness and well-formedness as basic criteria for self-explanation. Further properties of interest are aspects like determinism or consistency
with an environment model. The systems considered here are limited to generating
explanations for themselves and out of the available view onto the environment
which is largely unknown to the system. If the system itself incorporates a more
detailed model of the environment, the expected impact on the environment can
also be incorporated into the explanations. This provides an even deeper insight for
17
There are no other possible output assignments (again skipping the initial output
value):
AX(AG((speed_left[7:0]=255 ∧ speed_right[7:0]=255
∧ direction_right=fwd ∧ direction_left=fwd)
∨ ( ((direction_right=bwd ∧ direction_left=fwd)
∨ ( direction_right=fwd ∧ direction_left=bwd))
∧ speed_left[7:0]=5 ∧ speed_right[7:0]=5 )
∨ (direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=245 ∧ speed_right[7:0]=255)
∨ (direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=255 ∧ speed_right[7:0]=245)))
Check 2 This check is trivial for the main module since each explanation immediately refers to preceding modules and requirements only, but not to an internal
state.
Check 3 Whenever we transition from one action to another, a new explanation
is produced. Indeed we prove that certain output values also imply a certain action
encoded in the explanation, i.e., the ←-direction of the properties in Check 1. This
implies that a transition also causes a new explanation.
1.5 Future Extensions
The proposed formalization of self-explanation has some limitations that may be
waived. Moreover, in a practical setting automation is needed to add self-explanation
to an existing system.
1.5.1 Extending Explanations
Currently, an action is defined to be a variable assignment. In practice, more
complex actions may be of interest, e.g., to perform a burst access to a communication resource. Appropriate extensions are possible by allowing for a more general
specification of an action, e.g., in terms of a formal property language that describes
conditional sequential traces.
We propose completeness and well-formedness as basic criteria for self-explanation. Further properties of interest are aspects like determinism or consistency
with an environment model. The systems considered here are limited to generating
explanations for themselves and out of the available view onto the environment
which is largely unknown to the system. If the system itself incorporates a more
detailed model of the environment, the expected impact on the environment can
also be incorporated into the explanations. This provides an even deeper insight for