Formal Verification Framework for Safety of Real-Time System based on Timed Automata Model in PVS

Q. Xu and H. Miao (PRC)

Keywords

real-time system, timed automata, formal verification,specification, PVS

Abstract

Based on the analysis for the specification for the real time system, we develop a formal verification framework for the real-time system using Timed Automata theory in PVS (Prototype Verification System). In this framework, some operations about timed automata can be carried out, and the safety specifications can be verified. Meanwhile, a safety property and a bounded response property are successfully verified for a typical real-time system in this verification framework.

Important Links:



Go Back