[1]刘杰,阳小华,刘华,等.基于微分动态逻辑的数字化反应堆控制系统建模与验证方法[J].中国安全生产科学技术,2015,11(5):40-44.[doi:10.11731/j.issn.1673-193x.2015.05.006]
LIU Jie,YANG Xiao-hua,LIU Hua,et al.Study on modeling and verification methods of digital reactor control system based on differential dynamic logic[J].JOURNAL OF SAFETY SCIENCE AND TECHNOLOGY,2015,11(5):40-44.[doi:10.11731/j.issn.1673-193x.2015.05.006]
点击复制
基于微分动态逻辑的数字化反应堆控制系统建模与验证方法
LIU Jie,YANG Xiao-hua,LIU Hua,et al.Study on modeling and verification methods of digital reactor control system based on differential dynamic logic[J].JOURNAL OF SAFETY SCIENCE AND TECHNOLOGY,2015,11(5):40-44.[doi:10.11731/j.issn.1673-193x.2015.05.006]
《中国安全生产科学技术》[ISSN:1673-193X/CN:11-5335/TB]
- 卷:
- 11
- 期数:
- 2015年5期
- 页码:
- 40-44
- 栏目:
- 学术论著
- 出版日期:
- 2015-05-30
文章信息/Info
- Title:
- Study on modeling and verification methods of digital reactor control system based on differential dynamic logic
- 关键词:
- 混成系统; 微分动态逻辑; 数字化反应堆控制系统; 建模与安全性验证
- Keywords:
- hybrid system; differential dynamic logic; digital reactor control system; modeling and safety verification
- 分类号:
- X946
- 文献标志码:
- A
- 摘要:
- 核电数字化仪系统既涉及反应堆随时间变化的物理动态演化过程，又涉及计算机的离散控制过程，属于典型的实时混成系统。微分动态逻辑是近年在混成系统验证领域的新方法。提出以微分动态逻辑为基础的构建反应堆控制系统安全验证模型方法，验证反应堆控制系统中离散化的逻辑控制与反应堆连续性的物理连续变化过程之间的相互作用能否保证反应堆安全需求，从而提高数字化反应堆控制系统设计的安全性。
- Abstract:
- Digital reactor control system is a typical real-time hybrid system involving the physical dynamic evolution process of reactor against time and the discrete control process of computer. Differential dynamic logic is a new theory for hybrid system verification. A new method to construct safety verification model of digital reactor control system based on differential dynamic logic was put forward, so as to verify whether the interaction between discrete logic control in reactor control system and the physical continuous change process of reactor continuity can guarantee the safety requirement of reactor. It improves the safety properties of design on digital reactor control system.
参考文献/References:
［1］Schaft AVD, Schumacher H. An Introduction to Hybrid Dynamical System［M］. London: Spring-Verlag, 2000
［2］卜磊,解定宝. 混成系统形式化验证［J］.软件学报, 2014,25(2):219-233
BU Lei, XIE Ding-bao. Formal verification of hybrid system［J］. Journal of Software, 2014,25(2):219-233
［3］Platzer A. Differential dynamic logic for hybrid systems［J］. Journal of Automated Reasoning, 2008, 41(2): 143-189
［4］Platzer A. Logical analysis of hybrid systems: proving theorems for complex dynamics［M］. Springer Publishing Company, Incorporated, 2010
［5］Platzer A. The complete proof theory of hybrid systems［C］//Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science. IEEE Computer Society, 2012: 541-550
［6］钱磊, 郁文生. 基于微分动态逻辑的铁路道口控制分析［J］. 计算机科学, 2013, 40(10): 231-234
QIAN Lei, YU Wen-sheng. Modeling and analysis of railway crossing based on differential dynamic logic［J］. Computer Science, 2013, 40(10):231-234
［7］刘金涛, 唐涛, 赵林, 等. 基于微分动态逻辑的无线闭塞中心交接协议建模与验证［J］. 中国铁道科学, 2012, 33(5): 98-104
LIU Jin-tao, TANG Tao, ZHAO Lin, et al. Modeling and verification of radio block center handover protocol based on differential dynamic logic［J］. China Railway Science, 2012, 33(5): 98-104
［8］Platzer A, Quesel J D. KeYmaera: A hybrid theorem prover for hybrid systems (system description)［M］//Automated Reasoning. Springer Berlin Heidelberg, 2008: 171-178
［9］张建民. 核反应堆控制［M］. 西安：西安交通大学出版社, 2002
［10］刘杰, 阳小华, 余童兰,等. 基于 STAMP 模型的核动力蒸汽发生器水位控制系统安全性分析［J］. 中国安全生产科学技术, 2014, 10(5): 78-83
LIU Jie, YANG Xiao-Hua, YU Tong-lan, et al. STAMP model and safety analysis of control system for level of steam generator［J］. Journal of Safety Science and Technology, 2014, 10(5): 78-83
［11］Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems［J］. Theoretical computer science, 1995, 138(1): 3-34
相似文献/References:
备注/Memo
- 备注/Memo:
- 湖南省普通高等学校科学研究（重点）资助项目（11A105）；中国核动力研究设计院核反应堆系统设计技术重点实验室资助（HT-YK-04-2015002）
