[Avrora] Questions regarding AVRora
regehr at cs.utah.edu
Wed Mar 25 10:42:48 PDT 2009
Although I don't have answers to most of your questions, this is great to
see. I hope you'll contribute some checking work back to Avrora.
I have a student who is working on model checking TinyOS applications, but
much low-level code is abstracted away in our approach. It would be very
interesting to compare and contrast this approach with your assembly-level
work at some point.
> 3) We cannot model time due to the very high number of states
> encountered in model checking. Hence, if we were to use the AVRora, we
> would need to remove cycle-accuracy. How difficult do you estimate would
> this be?
Since time is only visible to an AVR program when it reads a
time-dependent device register, the cycle accuracy should not get in your
way at all.
Obviously you'll need to be clever to deal with programs that perform
interesting computations based on values that come from timer registers.
> 4) How difficult is fetching and restoring the entire state of the
> simulated microcontroller? The reason for this is that after each
> instruction execution step or an interrupt, we need to store system
> states in our state space, and restore them later from there. The AVRora
> documentation indicates that it is based on a thoroughly object-oriented
> design. I assume that if this is the case, fetch/restore might be
I strongly doubt that this poses significant problems.
> 5) For instruction execution, we would need to extend the simulator by
> symbolic execution. This means that a register may hold not only values
> 0...255 but also something such as 0n10nn00. This would indicate that
> bits 2, 3 and 6 are nondeterministic. In your opinion, how difficult
> would it be to adapt AVRora such that it supports such things?
I believe Avrora already includes bitwise domain representations and
transfer functions in its stack depth estimator. You'll need to dig into
the code to find out more.
Also, please consider using our bitwise domain transfer functions for AVR
These are likely to be more correct and more precise than whatever you
write by hand! Bastian and I chatted about this in 2007 but I never
followed up. Currently our transfer functions are in C but translating to
Java would be easy. If you will use the results, I'll do the translation.
You should consider adding abstract domains that are more expressive than
0/1/unknown bits. For example, intervals and bounded-size value sets will
give you good results for some kinds of code where the bitwise approach
explodes. The problem is that no domain is uniformly best: you'll need to
support several different ones and adaptively switch between them.
More information about the Avrora