您现在的位置是：首页 > 技术资料 > 基于TSSM的城市轨道交通CBTC区域控制器建模与验证

推荐星级：

基于TSSM的城市轨道交通CBTC区域控制器建模与验证

更新时间：2019-12-26 10:11:31 大小：1001K 上传用户：xiaohei1810 查看TA发布的资源 标签：tssm cbtc 区域控制器 下载积分：1分评价赚积分（如何评价?）打赏收藏评论(0) 举报

资料介绍

针对安全状态机缺乏时间描述能力的缺点,利用反应式系统的同步设计方法,提出了时间安全状态机TSSM(timed safe state machine)建模方法,定义了弱变迁和同步变迁语法,建立了城市轨道交通ZC(zone controller)系统模型.首先,分析了ZC系统的运行环境、工作原理和功能需求,根据ZC反应式系统的特点,利用TSSM在SCADE(safety critical application development environment)中建立了ZC系统列车管理、ZC控制、MA计算和队列管理子模型;其次,通过ZC系统的TSSM网络模型,分析了子模型间的交互信息;最后,采用Lustre语言对ZC系统的安全特性进行了形式化描述,并利用Design Verifier模型检测工具,结合数据流验证了ZC系统的功能和性能需要.研究结果表明,ZC系统TSSM模型的安全性和受限活性均为有效,ZC系统完全满足预期的安全需求.

部分文件列表

文件名	大小
基于TSSM的城市轨道交通CBTC区域控制器建模与验证.pdf	1001K

立即下载

【关注B站账户领20积分】

部分页面预览

（完整内容请下载后查看）

第50卷第1期

西南交通大学学报

OF SOUTHⅥ倔ST

V01．50

No．1

2015年2月

Feb．2015

JOURNAL

JIAOTONG UNIVERSITY

文章编号：0258．2724(2015)叭JD027J09

DOI：10．3969／j．issn．0258-2724．2015．01．005

基于TSSM的城市轨道交通

CBTC区域控制器建模与验证

李

正

耀，

陈荣武，

郭

进，

(西南交通大学信息科学与技术学院，四川成都610031)

孔令晶，

周

摘要：针对安全状态机缺乏时间描述能力的缺点，利用反应式系统的同步设计方法，提出了时间安全状态机

s小state

偈SM(timed

machine)建模方法，定义了弱变迁和同步变迁语法，建立了城市轨道交通ZC(zone

controUer)系统模型．首先，分析了zC系统的运行环境、工作原理和功能需求，根据zC反应式系统的特点，利用

偈sM在sCADE(s如ty critical印plication devel叩ment enviro啪ent)中建立了zC系统列车管理、zC控制、MA计

算和队列管理子模型；其次，通过zc系统的TSsM网络模型，分析了子模型间的交互信息；最后，采用Lus吨语

言对zc系统的安全特性进行了形式化描述，并利用Des咖VeriIier模型检测工具，结合数据流验证了zC系统的

功能和性能需要．研究结果表明，zC系统TSsM模型的安全性和受限活性均为有效，zc系统完全满足预期的安

全需求．

关键词：区域控制器；时间安全状态机；建模；高安全性应用开发环境；验证；模型检测

中图分类号：11P393；u283

文献标志码：A

and Vermcation 0f TSSM-B蹴d

ModeUng

CBTC ZoI伧ControUer for Urban Rail

Tr踟磷t

U_Y∞．CHEN

GUo

ZHoU

Rong∞u，

J流，KoNG‰ 西讥g，

Zkng

Inf0册ation Science and

61003

(School

Technology，S0uthWest

l，Chi舱)

Jiaotong Unive鹅遗，Chengdll

s疵state machine lacks time

based on the

s也state

Abst阳ct：

pmpeny，a髑SM(timed

machine)modeling

weak呦sition

model for urbaIl mil

method was

and

method of reactive

synchronous design

presented

system．The

tE吼sition were

t}Ie

defined，and

ZC(zone contmller)

synchronized

system

transit was

established．

and functional

of ZC

First，the

operation enVironment，principle

requirements

were

and

to the ZC fbatures of reactiVe

the train

analyzed，

according

systems，

m粕agement，

calculation and

sub-models of ZC

queue management

deVelopment enVironment)．Then

were built _usingTSSM in

tlle 7ISSM nemork model

features of

contr01，MA

system

critical

SCADE(safety

application

tIlrough

intemction info丌Ilation between the踟b· models

zC，the

w鹊aIIalyzed．Finally，me

safety

ZC are

the functional and

are examined

Lustre，and

fo瑚aUy expressed

data now in

perfbnnance requirements

Verifier．1'Ile resuh demonstrates the

of出e bounded liveness and

validity

satisfies the functional and

nlnning

Design

that

ofthe TSSM

shows

completely

model，which

s如ty pmperties

requirements．

s如ty

1【ey啪柑s：zC；，I筠M；modeling；SCADE；v商fication；model checkiIlg

咖in

基于通信的列车控制系统(communicatioIls· based

control，CBTC)是城市轨道交通列车运行控

收稿日期：2014旬l-2l

基金项目：中国铁路总公司科技研究开发计划资助项目(2012x007一D)；中国铁路总公司科技研究开发计划重大课题(2012x003一A)

作者简介：李耀(1985一)，男，博士研究生，研究方向为安全苛求系统的安全性，E· mail：1iy∞j78@163．com

引文格式：李耀，陈荣武，郭进，等．基于1ssM的城市轨道交通cBTC区域控制器建模与验证[J]．西南交通大学学报，2015，50(1)：

27-35．

万方数据

西

南

交

通

大

报

第50卷

学

制系统的发展方向，当前已成为大密度城市轨道交

通系统的优选方案．CBTC系统具有安全、高效、平

稳及组织灵活等优点．近年来，北京、上海、广州、深

圳、南京、武汉、沈阳、成都等城市已陆续开通了

CBTC轨道交通系统．

与TA、Petri—Net等建模方法相比，具有分层结构、

优先级抢占及并发控制三大特性，善于处理复杂的

逻辑关系．SSM是FsM(finite．state machine)的扩

展，拥有强变迁、弱变迁及同步变迁3种状态转移

方式，每个变迁都具有相应的优先级，特别是同一

个状态有多条出发变迁时，sSM能够很好地控制状

态转移行为，同时sSM支持状态嵌套．图1(a)和

图l(b)分别为同一个系统的TA模型图和SSM模

型图，当有故障发生时，两者都需要立即从当前状

态进入到故障状态，由于TA是平坦的，SSM具有层

次性，TA向故障状态转移的行为不如SSM“经济”．

CBTC包括地面设备及车载设备两部分，区域

控制器(zone controller，zc)是地面设备的核心．

zC是典型的安全苛求系统，如果ZC系统控制逻

辑存在潜在的缺陷，极可能导致cBTC系统在运行

中失效，造成人员伤亡、重大财产损失及环境破坏

等灾难性的后果．对zC系统逻辑结构进行分析研

究，验证zC功能的安全性、正确性和完整性关系

到列车运行的安全和效率，具有重要意义．

近年来很多学者对zc系统进行了仿真、建模

和验证．西南交通大学轨道交通控制实验室建立了

完整的CBTC仿真平台，能够模拟列车的整个运行

过程．文献[1．5]采用时间自动机(timed automata，

TA)、UML(unified modeling larIguage)和Petri—Net

对zc系统进行了建模分析．自动机不具备层次性

和模块性，变迁行为复杂，容易造成状态混乱和空

间爆炸，难以对复杂系统建模，uML和Petri—Net在

系统安全行为分析上存在缺陷．

(a)TA模型

本文分析了zC系统的工作特点，将ZC视为

一个反应式系统，选择对该系统具有很强建模能力

的安全状态机(s如state machine，SSM)为ZC系

统进行建模分析．zC系统中存在大量的时间约束，

系统的正常工作必须满足特定的时钟条件，时钟特

性的验证也是zC系统安全性保障的重要措施之

一，然而sSM缺乏时间表述能力，不能描述及验证

系统的时间特性，故仅依靠SSM不能建模ZC的时

间特性．本文在SSM的基础上提出了时间安全状

s也state

态机(timed

machine，髑SM)，并重新定义

(b)SSM模型

了弱变迁和同步变迁，同时在高安全性应用开发环

图1 TA与ssM对比

betwe髓TA柚d SSM

cTitical

Fig．1 Compdson

境(明fety

developn屺nl en、，immnent，

apphcation

sCADE)中构建了zC系统的偈SM网络模型，描述

了zC的功能结构、时间特性及与环境的交互情

况，最后验证了zC系统的安全特性．

SCADE支持SSM的建模、仿真及形式化验证，

为sSM的应用提供了支持．scADE以Lus讹为基

础，是法国爱斯特尔技术公司运用基于模型的方式

为高安全性系统提供的完整的解决方案．SCADE

在安全苛求系统领域开发中使用十分广泛，空中列

车、巴黎地铁、ANsALDO等项目开发都使用了

scADE，实践表明ScADE能够极大地提高产品开

发的效率和质量．

时间安全状态机TSSM

1．1安全状态机SSM

ssM以同步语言Esterel为基础，由Statecharts

和ARGOS发展而来，是一种可视化的建模方法，

具有严格的形式化语义【64J．SSM以完全确定的方

式处理系统行为，避免了模糊性及二义性等问题，

时间是反应式系统中十分重要的属性．由于反

应式系统不停地与环境交互，系统要正确地执行预

万方数据

全部评论(0)

暂无评论

评论赚积分>>

上传资源上传优质资源有赏金

最新上传

打赏
30日榜单

21ic小能手打赏10.00元 3天前

资料：STM32F103C8T6对应的流水灯程序
21ic小能手打赏10.00元 3天前

资料：五站小车呼叫停站汇川PLC 触摸屏及数字孪生场景
21ic小能手打赏10.00元 3天前

资料：40个Arduino编程学习例程合集，Arduino程序设计基础实验说明文档
sdqdjqk 打赏1.00元 3天前

资料：单机版DLT645-RS485抄表
21ic小能手打赏10.00元 3天前

资料：AI 数字生活盒（AI Digital Life Box）项目
wisdomlin 打赏1.00元 3天前

资料：JRC4558封装DIP8 电子元器件首鼎集成电路IC
21ic小能手打赏10.00元 3天前

资料：开源无线麦克风（Open-Source Wireless Microphone）项目
799902619 打赏1.00元 3天前

资料：新立新龙软件
21ic小能手打赏10.00元 3天前

资料：FLPowerPro 专业开源电源供应器项目
21ic小能手打赏10.00元 3天前

资料：ESP 智能电动牙刷（ESP Toothbrush）项目资料包
21ic小能手打赏10.00元 3天前

资料：65535 阶高精度数字电位器项目
21ic小能手打赏10.00元 3天前

资料：ESP32 迷你墨水屏 MP3 播放器项目
21ic小能手打赏10.00元 3天前

资料：ESP Box 3 摇杆版（ESP Box 3 Joystick Edition）项目
21ic小能手打赏10.00元 3天前

资料：改进型 Exlink 多功能调试器（分离叠板）项目
21ic小能手打赏10.00元 3天前

资料：迷你音频稳压器（Mini Audio Regulator）项目
21ic小能手打赏10.00元 3天前

资料：Tuya T5 智能像素灯（Tuya T5 Pixels）项目
21ic小能手打赏10.00元 3天前

资料：基于 STM32 的多传感器物联网采集板项目总结
21ic小能手打赏10.00元 3天前

资料：ESP32 最小系统板（ESP32 Minimal System Board）项目
21ic小能手打赏10.00元 3天前

资料：5.8GHz FPV 图传模块项目
21ic小能手打赏10.00元 3天前

资料：智谱开源AutoGLM
21ic下载打赏310.00元 3天前

用户：jh0355

21ic下载打赏310.00元 3天前

用户：zhengdai
21ic下载打赏310.00元 3天前

用户：gsy幸运
21ic下载打赏230.00元 3天前

用户：小猫做电路
21ic下载打赏210.00元 3天前

用户：w178191520
21ic下载打赏60.00元 3天前

用户：jh03551
21ic下载打赏90.00元 3天前

用户：铁蛋锅
21ic下载打赏80.00元 3天前

用户：xzxbybd
21ic下载打赏60.00元 3天前

用户：kk1957135547
21ic下载打赏60.00元 3天前

用户：w1966891335
21ic下载打赏60.00元 3天前

用户：w993263495
21ic下载打赏60.00元 3天前

用户：sun2152
21ic下载打赏60.00元 3天前

用户：xuzhen1
21ic下载打赏60.00元 3天前

用户：liao6
21ic下载打赏70.00元 3天前

用户：liqiang9090
21ic下载打赏70.00元 3天前

用户：mulanhk
21ic下载打赏20.00元 3天前

用户：x15580286248
21ic下载打赏30.00元 3天前

用户：玉落彼岸
21ic下载打赏5.00元 3天前

用户：hnygpx
21ic下载打赏10.00元 3天前

用户：vikey_zhu

基于TSSM的城市轨道交通CBTC区域控制器建模与验证

资料介绍

部分文件列表

部分页面预览

相关下载

全部评论(0)

热门标签

最新上传

热门下载

资料专题

推荐下载

专栏首页