Real-Time Model Checking is Really Simple
13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods |
It is easy to write and verify real-time specifications with existing languages and methods; one just represents time as an ordinary variable and expresses timing requirements with special timer variables. The resulting specifications can be verified with an ordinary model checker. This basic idea and some less obvious details are explained, and results are presented for two examples.
This is an abridged version of [155], containing only the material on model checking.