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 oher 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.
timed automata TLA real-time system formal method model checking
Tang Zheng-yi Li Jun-tao Peng Chang-gen Li Xiang
College of Computer Science and Information Guizhou university Guiyang, China College of Science Guizhou university Guiyang, China
国际会议
太原
英文
514-517
2010-10-22（万方平台首次上网日期，不代表论文的发表时间）