During the Spring '07 semester I TAed for Dr. Mok's course "Dependable Real-Time Systems".
The course was part of the professional MSE program on Software Engineering at UT, Austin.
I volunteered to implement a model checker based on RTCTL, a system of temporal logic, described in
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.
The code has been successfully used by ~30 students in the class on their assignments.
I implemented it in Java, that was a "requirement" by the instructor to facilitate code distribution.
Additionally, I used BYACC/J, Java based version of YACC for the parser.
The whole project took roughly a long weekend to design, code and debug.
A (very lean) .ppt file describing how to use the model checker can be found as an attachment below.
The source code can be available for qualified applicants :)
Comments and criticism are both welcome.