It is easy to write and verify real-time specifications with existing languages and methods; one just represents time as an ordinaryvariable. The resulting specifications can be verified with ordinary model checkers. This basic idea and some less obvious details are explained with simple examples.

PDF file

Details