首页 | 官方网站   微博 | 高级检索  
     

联锁逻辑形式化模型检验的研究
引用本文:杜军威,XU Zhong-wei,宋波.联锁逻辑形式化模型检验的研究[J].计算机工程,2007,33(15):33-35.
作者姓名:杜军威  XU Zhong-wei  宋波
作者单位:1. 同济大学电子与信息工程学院,上海,200331;青岛科技大学信息科学技术学院,青岛,266061
2. 上海大学计算机学院,上海,200072
摘    要:利用自动机理论模型检验算法,检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑,有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力,利用该方法对车站联锁逻辑的实际问题进行了性能验证。

关 键 词:有色Petri网  线性时态逻辑  带标签的广义Büchi自动机  联锁逻辑
文章编号:1000-3428(2007)15-0033-03
修稿时间:2006-12-25

Research on Formal Model Checking of Interlocking Logic
DU Jun-wei,XU Zhong-wei,SONG Bo.Research on Formal Model Checking of Interlocking Logic[J].Computer Engineering,2007,33(15):33-35.
Authors:DU Jun-wei  XU Zhong-wei  SONG Bo
Affiliation:(1. School of Electronics & Information Engineering, Tongji University, Shanghai 200331; 2. School of Information Science and Technology , Qingdao University of Science and Technology, Qingdao 266061; 3. School of Computer Science, Shanghai University, Shanghai 200072)
Abstract:A method about automata-theoretic model checking is presented. This method is used to verify the property of color Petri nets(CPN) model of interlocking logic. State space exposition can be solved efficiently by constructing linear-time temporal logic(LTL) with labeled generalized Büchi automaton(LGBA) in model checking. This method improves the analysis and checking of CPN. A practical case of the railway interlocking logic is checked by this method.
Keywords:colored Petri nets  linear-time temporal logic  labeled generalized Btichi automaton  interlocking logic
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《计算机工程》浏览原始摘要信息
点击此处可从《计算机工程》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司    京ICP备09084417号-23

京公网安备 11010802026262号