%0 Journal Article
%T New Approaches for Model Checking<br>模型检测新技术研究
%A RONG Mei ZHANG Guang-Quan
%A <br>戎玫
%A 张广泉
%J 计算机科学
%D 2003
%I 
%X Model checking is an algorithmic verification technique that checks automatically whether a given finite state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space explosion problem. In this paper, several important approaches have been proposed for dealing with the state explosion problem. Such approaches are symbolic, abstraction, partial.order reduction, compositional reasoning, etc. Then,a number of way are proposed for verifying real.time and hybrid systems using model checking. At last, several approaches combining model checking and other verification techniques or mathematical methods are considered.
%K Model checking
%K State explosion
%K Symbolic model checking
%K Abstraction
%K Partial-order reduction
%K Compositional reasoning
%K Real-time system
%K Hybrid system<br>软件开发
%K 软件可靠性
%K 形式化方法原则
%K 软件系统
%K 演绎推理
%K 模型检测
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=AA68817BCF550FD3&yid=D43C4A19B2EE3C0A&vid=340AC2BF8E7AB4FD&iid=94C357A881DFC066&sid=331211A5F5616413&eid=DBF54A8E2A721A6D&journal_id=1002-137X&journal_name=计算机科学&referenced_num=16&reference_num=15