| 基于项重写系统的联锁系统模型检测方法研究 |
| |
| 引用本文： | 张舒青,徐中伟,陈祖希.基于项重写系统的联锁系统模型检测方法研究[J].计算机工程与应用,2014,50(3):49-54. |
| |
| 作者姓名： | 张舒青 徐中伟 陈祖希 |
| |
| 作者单位： | 同济大学 电子与信息工程学院，上海 201804 |
| |
| 基金项目： | 国家自然科学基金（No.60674004）；国家高技术研究发展计划（863）（No.2012AA112801）；国家十二五科技支撑项目（No.2011BAG01B03）。 |
| |
| 摘 要： | 模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术，对于验证系统的正确性，具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法，采用基于项重写系统原理的Maude工具语言，对铁路联锁系统的站场进行形式化建模，通过其语法和语义定义各类约束和离散事件，构架联锁系统属性和行为。在模型建立的基础上，对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明，基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发，对开发安全苛求系统和模型检测方法的实际应用提供借鉴。
|
| 关 键 词： | 项重写系统 联锁 Maude语言 安全苛求系统 模型检测 |
Research on modeling and verification methods of interlocking system based on term rewriting system |
| |
| ZHANG Shuqing,XU Zhongwei,CHEN Zuxi.Research on modeling and verification methods of interlocking system based on term rewriting system[J].Computer Engineering and Applications,2014,50(3):49-54. |
| |
| Authors: | ZHANG Shuqing XU Zhongwei CHEN Zuxi |
| |
| Affiliation: | School of Electronics and Information, Tongji University, Shanghai 201804, China |
| |
| Abstract: | |
| |
| Keywords: | Term Rewriting System interlocking system Maude safety-critical system model checking |
| 本文献已被 CNKI 维普 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
