1;3409;0c Real-Time Model Checking Is Really Simple

Real-Time Model Checking Is Really Simple

Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, vol. 3725, 2005
Pages: 162-175DOI: 10.1007/11560548_14



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.