Modeling Predicate Abstraction of Timed Automata in PVS

In this paper, we propose a mechanized framework for formal verification of real-time systems based on predicate abstraction in PVS (Prototype Verification System) based on timed automata model. This framework is composed by two parts: one for modeling the real-time system and its abstract system which is abstracted from concrete time system by predicate abstraction and over-approximation techniques, the other for proving the properties need to be verified with which we can consider that our framework is effective. A finite state property-preserving abstraction of the original system is established in this framework.