| 基于时间自动机的道岔自动控制研究 |
| |
| 引用本文： | 周清雷,姬莉霞.基于时间自动机的道岔自动控制研究[J].控制工程,2004(Z2). |
| |
| 作者姓名： | 周清雷 姬莉霞 |
| |
| 作者单位： | 郑州大学信息工程学院，郑州大学信息工程学院 河南郑州450052信息工程大学信息工程学院，河南郑州450002，河南郑州450052 |
| |
| 摘 要： | 实时系统由于受时间约束,设计和验证具有很高的挑战性。用多个时间自动机来规范模拟道岔自动控制系统,给出了一种自动化的道岔控制模型(TTCQ),并采用UPPAAL作为模型验证工具,证明了该模型具有安全性、有效性和可控性。所采用的方法避免了积的等价类状态空间的爆炸,减少了验证的搜索空间,为铁路交通提供了一种可行的、安全的、智能的控制机制。
|
| 关 键 词： | 时间自动机 道岔 UPPAAL 实时系统 |
On Automatic Turnout Control Based on Timed Automata |
| |
| ZHOU Qing-lei,JI Li-xia.On Automatic Turnout Control Based on Timed Automata[J].Control Engineering of China,2004(Z2). |
| |
| Authors: | ZHOU Qing-lei JI Li-xia |
| |
| Abstract: | Because the real-time system is constrained by time, to design and verify it is a high challenge. Several timed automata are used to model an automatic turnout control system and an automatic control model of a turnout (TTCQ) is presented. UPPAAL is adopted to carry out the on-the-fly testing and it is proved that TTCQ has such characteristics as safety, efficiency and control. The method mentioned avoids the equivalent state explosion of the product, reduces the verification search space and provides a feasible, safe and intelligent control mechanism. |
| |
| Keywords: | timed automata turnout UPPAAL real-time system |
| 本文献已被 CNKI 等数据库收录！ |
|
