%0 Journal Article
%T Model Checking on Duration Properties of Real-time Systems<br>ʵʱϵͳʱ¶ÎÐÔÖʵÄÄ£ÐͼìÑé
%A ÀîÓÂ
%A ÀîÐû¶«
%A Ö£¹úÁº
%J ¼ÆËã»ú¿Æѧ
%D 2002
%I 
%X Model Checking is a widely used technology to verify the design's correctness automatically. Real-time systems' properties include instant properties and duration properties. It is no doubt that checking real-time systems for the latter is much more difficult than the former. This paper introduces the main work on checking some duration properties of real-time systems for decades with comparison, and discusses the future work at last.
%K Model checking
%K Real-time systems
%K Duration property
%K Timed automata<br>ʵʱϵͳ
%K ʱ¶ÎÐÔÖÊ
%K Ä£ÐͼìÑé
%K ¼ÆËã»ú
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=88460264E198EF4E&yid=C3ACC247184A22C1&vid=771469D9D58C34FF&iid=708DD6B15D2464E8&sid=31611641D4BB139F&eid=ED01F5AE50BE09C0&journal_id=1002-137X&journal_name=¼ÆËã»ú¿Æѧ&referenced_num=0&reference_num=18