期刊名称：International Journal of Grid and Distributed Computing
印刷版ISSN：2005-4262
出版年度：2015
卷号：8
期号：1
页码：179-188
DOI：10.14257/ijgdc.2015.8.1.17
出版社：SERSC
摘要：With the continuous increase in the size and complexity of a real-time computer system, the use of formal verification methods in software development is also on the rise. The traditional formal verification method is not fully applicable to the development of actual system life cycle. Therefore, this paper presents a new real-time system verification method, It takes the deadlock timed Büchi automata as the medium, and translates the timed temporal logic into timed communicating sequential process language. The tock event is also joined, which can be directly used for the detection of refinement tool FDR. The method verifies the situation of deadlock. To establish the link between the conventional model checking and refinement model checking can well combine the advantages of both and improves system security and reliability.
