基于时间自动机的道岔自动控制研究
来源期刊：控制工程2004年第S2期
论文作者：周清雷 姬莉霞
文章页码：146 - 149
关键词：时间自动机;道岔;UPPAAL;实时系统;
摘 要：实时系统由于受时间约束,设计和验证具有很高的挑战性。用多个时间自动机来规范模拟道岔自动控制系统,给出了一种自动化的道岔控制模型(TTCQ),并采用UPPAAL作为模型验证工具,证明了该模型具有安全性、有效性和可控性。所采用的方法避免了积的等价类状态空间的爆炸,减少了验证的搜索空间,为铁路交通提供了一种可行的、安全的、智能的控制机制。
周清雷，姬莉霞
摘 要：实时系统由于受时间约束,设计和验证具有很高的挑战性。用多个时间自动机来规范模拟道岔自动控制系统,给出了一种自动化的道岔控制模型(TTCQ),并采用UPPAAL作为模型验证工具,证明了该模型具有安全性、有效性和可控性。所采用的方法避免了积的等价类状态空间的爆炸,减少了验证的搜索空间,为铁路交通提供了一种可行的、安全的、智能的控制机制。
关键词：时间自动机;道岔;UPPAAL;实时系统;
