Information Technology Reference
In-Depth Information
A<>decryption.final
Second, it is verified that the
input
to the
encryption
automaton is the same
as the
output
of the
decryption
automaton:
A[]decryption.final imply encryption.input == decryption.output
7.5
Results and Analysis of Verification
The examples provided in this section have all been verified using Uppaal. One
verification showed that the specification of the first gcd-algorithm did not work
when one of the inputs were zero. In that case, the controller loops without
reaching the state
final
.
Verification of the upper bound on the number of clock cycles and changes
in register values showed that for 8 bit inputs the first algorithm maximally
uses 511 clock cycles and 261 register value changes to calculate the greatest
common divisor, the second algorithm maximally uses 26 clock cycles and 25
register value changes to calculate greatest common divisor. All these upper
bounds are actually least upper bounds, as, for example, 25 clock cycles are
shown, using Uppaal, not to be an upper bound for the number of clock cycles
for the second gcd-algorithm.
Verification of the SDES algorithm showed that for all combinations of plain-
texts and keys, an encryption followed by a decryption yields the original plain-
text. However, it was also verified that not all combinations of plaintexts and
keys had a changed ciphertext after encryption (e.g. plaintext 7 and key 0 gives
ciphertext 7). This of course is a property of the algorithm.
Each of the aforementioned Gezel specifications (i.e. the two different gcd-
and the SDES specifications) has been verified in less than 25 minutes on a SUN
Fire 3800 with 1.2GHz CPUs running Solaris 10. We have not yet done anything
particular to tune the verification.
8Con lu on
We have clarified the semantical domain for the hardware specification language
Gezel. Besides giving a much better understanding of the language itself, a clear
semantical model allows for a seamless transition into automated verification of
hardware specifications. In this way we have related the semantical domain of
Gezel to the timed-automata model and we have experimented with the Up-
paal system, showing the correctness of small, but interesting Gezel examples.
Although functional correctness is of primary importance, we have also consid-
ered the analysis of resource usage which for instance may guide the hardware
designer in choosing the most power ecient algorithm among a set of possible
algorithmic implementations of a given specification.
We are currently using Gezel as a way to introduce software engineering stu-
dents to hardware design and, in particular, to combined hardware/software
codesign needed to deal with the challenges of embedded systems. Clarifying the
Search WWH ::
Custom Search