Model-checking fair dense-time systems with propositions and events
Journal
International Journal on Software Tools for Technology Transfer
Journal Volume
17
Journal Issue
2
Pages
223-243
Date Issued
2015
Author(s)
Abstract
We propose a temporal logic, (Formula Presented.), for the flexible specification of distributed real-time systems with constraints involving events, propositions, and fairness. We then present algorithms for model-checking (Formula Presented.) formulas and a speed-up technique for refuting certain formulas. Finally, we report the implementation and experiment of the ideas in our tool, RED 8.
Type
journal article