%0 Journal Article
%T Optimization Technique for Shared Variables in Real-time System Model-Checking<br>实时系统的模型检验中针对共享变量的优化技术
%A ZHOU Xiu-Yi
%A ZHAO Jian-Hua
%A LI Xuan-dong
%A ZHENG Guo-liang
%A <br>周修毅
%A 赵建华
%A 李宣东
%A 郑国梁
%J 计算机科学
%D 2005
%I 
%X Real-time systems are often modeled as timed automaton networks, which are parallel compositions of timed automata. Those timed automata interact with each other through shared variables and/or communication chan- nels. In the literate, symbolic states with different shared variable valuations in automaton networks are treated as distinct ones. Therefore, shared variables are also one of the causes of state-space explosion. We present the notion of the compatibility relationship between different shared variable valuations in this paper. Using this compatibility relationship can reduce the amount of states that need exploring in the reachability analysis algorithm of timed au- tomaton networks. In this paper, we describe two algorithms: one that detects compact shared variable valuations and the other more powerful one that detects this compatibility relationship further. These two algorithms result in an enhanced reachability analysis algorithm. The experiment results show that our technioque improves the space-effi- ciency of reachability analysis significantly.
%K Model checking
%K Timed automata
%K Formal method<br>实时系统
%K 变量
%K 共享
%K 优化技术
%K 模型检验
%K 时间自动机
%K 状态空间爆炸
%K 分析算法
%K 兼容性
%K 增强算法
%K 空间效率
%K 可达性
%K 网络
%K 符号化
%K 检测
%K 交互
%K 遍历
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=2E5AEAB597DEAA3B&yid=2DD7160C83D0ACED&vid=9971A5E270697F23&iid=DF92D298D3FF1E6E&sid=23104246A5FCFCEF&eid=E0F6F365E4766526&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=7