Tautoko is a project that combines test case generation with dynamic specification mining to generate richer and more meaningful specifications.

There is a paper about Tautoko which is accepted for the International Symposium on Software Testing and Analysis 2010. Models referenced in the report are available here.

Right now, you can take a look at the How-To, or download a prototype (yet quite stable) implementation of Tautoko.