The specification and verification of Real-Time system based on the temporal logic of action

Real-Time system is the safety-critical system. Its safety should be ensured by the formal method. The different formal method has different advantages and deficiencies, the suitable combination of them can obtain a better effect. This paper introduces the timed automata and the temporal logic of action(TLA). The former is the modeling tool of Real-Time system, the other is a logic which has a strong ability of system description and attribute specification. On this basis, we research the method of using TLA to describe the Real-Time system which is expressed by timed automata and verify it by an actual example.