Very neat, I'd never heard of timed-automata before. I read a bit about it after seeing this comment and can definitely see the appeal in such a project.

I'm fascinated by how timed-automata can be used as models for real-time systems, and how presumably, a model checker used in that context would allow one to verify their behavior. It seems like a very neat connection between CS theory and real-world systems.