1 Self-explaining Digital Systems
15
Obviously, optimizations in the size required for explanations are possible, e.g.,
by adjusting the number of entries of explanation units per module or by encoding
explanations in fewer bits. But this is not within the scope of this chapter which
focuses on the concept of self-explanation.
1.4.3 Reasoning About Explanations
Having the design enhanced with explanations immediately supports a user or
a designer in understanding the design’s actions. Additionally, consistency of
the explanations and the related actions is an interesting question. Due to the
abstraction, e.g., in case of the driving direction it may not be fully clear what kind
of actions precisely correspond to an explanation. We give some examples how to
clarify this using model checking. We assume that the reader is familiar with model
checking [5] so we do not provide any details for this process.
Considering the main module some facts can be analyzed by model checking,
e.g., if the explanation of the main module says a certain action means moving
“straight,” this should imply that both motors are commanded to move in the same
direction with the same speed. Indeed the simple robot controller always moves
forward at full speed. In CTL this is proven using the formula:
AG( exp[23:20] =straight →
( speed_left[7:0]=255 ∧ speed_right[7:0]=255
∧ direction_right=fwd ∧ direction_left=fwd) )
The 24-bit vector “exp” refers to the explanation of the main module where only
the bits corresponding to the description of the action are selected; the 8-bit vectors
“speed_right” and “speed_left” correspond to the speed for the left and right motor,
respectively; likewise the “direction”-variables.
A similar property proves that “turn” always means opposite directions for the
left and right motor:
AG( exp[23:20]=turn →
( ( direction_right=bwd ∧ direction_left=fwd )
∨( direction_right=fwd ∧ direction_left=bwd )) )
These invariants are relatively simple consistency properties. By making the
case split for all possible valuations of “exp[23:20]” complete and showing that
the consequents partition all possible valuations of the output, completeness of
observable actions for the main module can be checked as proposed in Sect. 1.3.3.
Abstracted reasoning using model checking can be conveniently performed
on top of explanations. Consider the following example: any transition into the
powerstate “low” causes the main module to move to the light using the light
sensor as guidance for the direction unless one of the push-buttons is pressed which
immediately requires to move away from an obstacle. The following property in
15
Obviously, optimizations in the size required for explanations are possible, e.g.,
by adjusting the number of entries of explanation units per module or by encoding
explanations in fewer bits. But this is not within the scope of this chapter which
focuses on the concept of self-explanation.
1.4.3 Reasoning About Explanations
Having the design enhanced with explanations immediately supports a user or
a designer in understanding the design’s actions. Additionally, consistency of
the explanations and the related actions is an interesting question. Due to the
abstraction, e.g., in case of the driving direction it may not be fully clear what kind
of actions precisely correspond to an explanation. We give some examples how to
clarify this using model checking. We assume that the reader is familiar with model
checking [5] so we do not provide any details for this process.
Considering the main module some facts can be analyzed by model checking,
e.g., if the explanation of the main module says a certain action means moving
“straight,” this should imply that both motors are commanded to move in the same
direction with the same speed. Indeed the simple robot controller always moves
forward at full speed. In CTL this is proven using the formula:
AG( exp[23:20] =straight →
( speed_left[7:0]=255 ∧ speed_right[7:0]=255
∧ direction_right=fwd ∧ direction_left=fwd) )
The 24-bit vector “exp” refers to the explanation of the main module where only
the bits corresponding to the description of the action are selected; the 8-bit vectors
“speed_right” and “speed_left” correspond to the speed for the left and right motor,
respectively; likewise the “direction”-variables.
A similar property proves that “turn” always means opposite directions for the
left and right motor:
AG( exp[23:20]=turn →
( ( direction_right=bwd ∧ direction_left=fwd )
∨( direction_right=fwd ∧ direction_left=bwd )) )
These invariants are relatively simple consistency properties. By making the
case split for all possible valuations of “exp[23:20]” complete and showing that
the consequents partition all possible valuations of the output, completeness of
observable actions for the main module can be checked as proposed in Sect. 1.3.3.
Abstracted reasoning using model checking can be conveniently performed
on top of explanations. Consider the following example: any transition into the
powerstate “low” causes the main module to move to the light using the light
sensor as guidance for the direction unless one of the push-buttons is pressed which
immediately requires to move away from an obstacle. The following property in