Article(id=1241719285861634091, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, articleNumber=null, orderNo=9, doi=10.3981/j.issn.2097-0781.2023.01.008, pmid=null, cstr=null, oa=null, hot=null, price=null, onlineType=0, articleFormat=0, articleType=null, articleTypeStr=research-article, receivedDate=1671984000000, receivedDateStr=2022-12-26, revisedDate=1675180800000, revisedDateStr=2023-02-01, acceptedDate=null, acceptedDateStr=null, onlineDate=1679846400000, onlineDateStr=2023-03-27, pubDate=1679241600000, pubDateStr=2023-03-20, doiRegisterDate=null, doiRegisterDateStr=null, onlineIssueDate=1679846400000, onlineIssueDateStr=2023-03-27, onlineJustAcceptDate=null, onlineJustAcceptDateStr=null, onlineFirstDate=null, onlineFirstDateStr=null, sourceXml=null, magXml=null, createTime=1773978547774, creator=sys-migrate, updateTime=1773978547774, updator=sys-migrate, issue=Issue{id=1241719216169079576, tenantId=1146029695717560320, journalId=1146032081894723586, year='2023', volume='2', issue='1', pageStart='5', pageEnd='143', issueExtLink='null', onlineDate='null', pubDate='null', beforeIssueId=null, nextIssueId=null, price=null, status=1, issueComplete=1, articleOrder=1, issueType=-1, specialIssue=1, createTime=1773978531159, creator=sys-migrate, updateTime=1774001248771, updator=13041195026, preIssue=null, nextIssue=null, ext={EN=IssueExt(id=1241814500781916967, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=EN, specialIssueTitle=Science and Technology Foresight, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null), CN=IssueExt(id=1241814500781916968, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=CN, specialIssueTitle=形式化方法与复杂计算系统可信保障, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null)}, issueFiles=null}, startPage=106, endPage=117, ext={EN=ArticleExt(id=1241719291628802105, articleId=1241719285861634091, tenantId=1146029695717560320, journalId=1146032081894723586, language=EN, title=Research Progress and Trend of Formal Methods for Train Control System, columnId=1149656489310208610, journalTitle=Science and Technology Foresight, columnName=Review and Commentary, runingTitle=null, highlight=null, articleAbstract=
The train control system is the core for safe and efficient train operation. China’s current train control technology as a whole has reached the world’s advanced level and is developing toward intelligent and smart technologies. There is an urgent need for forward research and development and design methods supported by independent tool platforms. The formal method is the key to ensuring the correct implementation of the train control system’s functions. This paper first reviews the development process of the train control system and analyzes its characteristics in the computer era. Then, this paper summarizes the application research, progress, and trend of formal methods in train control both in and outside China and compares the differences in research on formal methods for train control. Finally, the development direction of the forward design of the train control system using model-based systems engineering (MBSE) is proposed, and development suggestions are given from the aspects of the system’s forward top-level design, formal technology independence, and talent team training. The efforts are dedicated to obtaining a train control system with powerful functions, comprehensive coverage, and advanced performance.
, correspAuthors=Tao TANG, authorNote=null, correspAuthorsNote=
†
, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=null, magXml=null, pdfUrl=null, pdf=null, pdfFileSize=null, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=null, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=null, mapNumber=null, authorCompany=null, fund=null, authors=null, authorsList=Jidong LÜ, Wanli LU, Tao TANG, Zhengwei LUO), CN=ArticleExt(id=1241719290089492535, articleId=1241719285861634091, tenantId=1146029695717560320, journalId=1146032081894723586, language=CN, title=列车运行控制系统的形式化研究进展与趋势, columnId=1148708266483446458, journalTitle=前瞻科技, columnName=综述与述评, runingTitle=null, highlight=null, articleAbstract=
列车运行控制系统是保障列车安全与高效运行的核心。目前中国列车运行控制技术整体已步入世界先进水平，正在向智能化、智慧化方向发展，迫切需要以自主化工具平台支撑的正向研发设计方法。形式化方法是保障列车运行控制系统功能正确实现的关键。文章首先回顾了列车运行控制系统的发展过程，分析了计算机时代列车运行控制系统的特点;总结了国内外列车运行控制领域形式化的应用研究、取得的进展和趋势，并对比了国内外列车运行控制领域形式化研究的差异;最后提出了采用基于模型的系统工程方法进行列车运行控制系统正向设计的发展方向，并从系统正向顶层设计、形式化技术自主化和人才队伍培养方面给出了发展建议，力求实现功能强大、覆盖全面、性能先进的列车运行控制系统。
, correspAuthors=唐涛, authorNote=null, correspAuthorsNote=
†
, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=s0jzGDwXoVZCtoujNE+6hQ==, magXml=KOSrq6GneUP3zg7NA/qdGA==, pdfUrl=null, pdf=IIebK157tNvzjK7hLwAzkg==, pdfFileSize=2364200, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=d5Dr6DTWM8VJ7o6w2D+a8w==, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=HH0+O6qFFpIhIjfCWbUigA==, mapNumber=null, authorCompany=null, fund=null, authors=
 |
吕继东，教授，博士研究生导师。主要从事列控系统形式化建模、安全验证与测试的基础理论与实际应用等研究。先后主持和参与国家重点基础研究发展计划、国家自然科学基金重点面上项目、国家重点研发计划、北京市自然科学基金等国家级、省部级科研项目20余项。出版专著2部，发表论文60余篇，获授权发明专利10项，获软件著作权10项。获中国铁道学会科学技术奖一等奖1项。电子信箱：jdlv@bjtu.edu.cn。 |
 |
唐涛，教授，博士研究生导师。北京交通大学轨道交通控制与安全国家重点实验室主任，北京市开放实验室“城市轨道交通自动化与控制实验室”主任。主要从事轨道交通列车运行控制等研究。入选新世纪百千万人才工程国家级人才。担任“交通信息工程及控制”国家级重点学科带头人、教育部自动化专业教学指导委员会委员、中国铁道学会理事。获教育部新世纪优秀人才支持计划、铁道部有突出贡献中青年专家、茅以升铁道科技奖和“北京市优秀教师”等荣誉称号。先后主持国家高技术研究发展计划、国家自然科学基金重点、国际合作项目等60余项。出版专著5部，发表论文200余篇，获授权发明专利9项，参与制定国家标准2项、行业规范14项。获国家科学技术进步奖二等奖2项、中国铁道学会科学技术奖一等奖2项、教育部自然科学奖一等奖1项、北京市科学技术进步奖一等奖2项、詹天佑铁道科学技术奖成就奖。电子信箱：ttang@bjtu.edu.cn。 |
, authorsList=吕继东, 卢万里, 唐涛, 罗正伟)}, authors=[Author(id=1241719310763225120, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, orderNo=0, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=jdlv@bjtu.edu.cn, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719310851305507, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719310763225120, language=EN, stringName=Jidong LÜ, firstName=Jidong, middleName=null, lastName=LÜ, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719310901637157, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719310763225120, language=CN, stringName=吕继东, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044, bio={"img":"PUshXYiQMKukgf9YfQX+JQ==","content":"
吕继东，教授，博士研究生导师。主要从事列控系统形式化建模、安全验证与测试的基础理论与实际应用等研究。先后主持和参与国家重点基础研究发展计划、国家自然科学基金重点面上项目、国家重点研发计划、北京市自然科学基金等国家级、省部级科研项目20余项。出版专著2部，发表论文60余篇，获授权发明专利10项，获软件著作权10项。获中国铁道学会科学技术奖一等奖1项。电子信箱：jdlv@bjtu.edu.cn。
"}, bioImg=PUshXYiQMKukgf9YfQX+JQ==, bioContent=
吕继东，教授，博士研究生导师。主要从事列控系统形式化建模、安全验证与测试的基础理论与实际应用等研究。先后主持和参与国家重点基础研究发展计划、国家自然科学基金重点面上项目、国家重点研发计划、北京市自然科学基金等国家级、省部级科研项目20余项。出版专著2部，发表论文60余篇，获授权发明专利10项，获软件著作权10项。获中国铁道学会科学技术奖一等奖1项。电子信箱：jdlv@bjtu.edu.cn。
, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719310587064343, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, xref=null, ext=[AuthorCompanyExt(id=1241719310599647256, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China), AuthorCompanyExt(id=1241719310608035865, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044)])]), Author(id=1241719310968746024, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, orderNo=1, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=null, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719311040049195, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719310968746024, language=EN, stringName=Wanli LU, firstName=Wanli, middleName=null, lastName=LU, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719311132323885, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719310968746024, language=CN, stringName=卢万里, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719310587064343, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, xref=null, ext=[AuthorCompanyExt(id=1241719310599647256, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China), AuthorCompanyExt(id=1241719310608035865, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044)])]), Author(id=1241719311186849839, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, orderNo=2, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=ttang@bjtu.edu.cn, emailSecond=null, emailThird=null, correspondingAuthor=1, authorType=1, ext={EN=AuthorExt(id=1241719311287513138, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719311186849839, language=EN, stringName=Tao TANG, firstName=Tao, middleName=null, lastName=TANG, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
2, †, address=2. State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719311371399219, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719311186849839, language=CN, stringName=唐涛, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
2, †, address=2.北京交通大学轨道交通控制与安全国家重点实验室，北京 100044, bio={"img":"sR1epq7857JTCpr7shIzaw==","content":"
唐涛，教授，博士研究生导师。北京交通大学轨道交通控制与安全国家重点实验室主任，北京市开放实验室“城市轨道交通自动化与控制实验室”主任。主要从事轨道交通列车运行控制等研究。入选新世纪百千万人才工程国家级人才。担任“交通信息工程及控制”国家级重点学科带头人、教育部自动化专业教学指导委员会委员、中国铁道学会理事。获教育部新世纪优秀人才支持计划、铁道部有突出贡献中青年专家、茅以升铁道科技奖和“北京市优秀教师”等荣誉称号。先后主持国家高技术研究发展计划、国家自然科学基金重点、国际合作项目等60余项。出版专著5部，发表论文200余篇，获授权发明专利9项，参与制定国家标准2项、行业规范14项。获国家科学技术进步奖二等奖2项、中国铁道学会科学技术奖一等奖2项、教育部自然科学奖一等奖1项、北京市科学技术进步奖一等奖2项、詹天佑铁道科学技术奖成就奖。电子信箱：ttang@bjtu.edu.cn。
"}, bioImg=sR1epq7857JTCpr7shIzaw==, bioContent=
唐涛，教授，博士研究生导师。北京交通大学轨道交通控制与安全国家重点实验室主任，北京市开放实验室“城市轨道交通自动化与控制实验室”主任。主要从事轨道交通列车运行控制等研究。入选新世纪百千万人才工程国家级人才。担任“交通信息工程及控制”国家级重点学科带头人、教育部自动化专业教学指导委员会委员、中国铁道学会理事。获教育部新世纪优秀人才支持计划、铁道部有突出贡献中青年专家、茅以升铁道科技奖和“北京市优秀教师”等荣誉称号。先后主持国家高技术研究发展计划、国家自然科学基金重点、国际合作项目等60余项。出版专著5部，发表论文200余篇，获授权发明专利9项，参与制定国家标准2项、行业规范14项。获国家科学技术进步奖二等奖2项、中国铁道学会科学技术奖一等奖2项、教育部自然科学奖一等奖1项、北京市科学技术进步奖一等奖2项、詹天佑铁道科学技术奖成就奖。电子信箱：ttang@bjtu.edu.cn。
, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719310670950427, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, xref=null, ext=[AuthorCompanyExt(id=1241719310679339036, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310670950427, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2. State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China), AuthorCompanyExt(id=1241719310687727645, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310670950427, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2.北京交通大学轨道交通控制与安全国家重点实验室，北京 100044)])]), Author(id=1241719311455285302, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, orderNo=3, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=null, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719311534977081, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719311455285302, language=EN, stringName=Zhengwei LUO, firstName=Zhengwei, middleName=null, lastName=LUO, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719311597891643, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, authorId=1241719311455285302, language=CN, stringName=罗正伟, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719310587064343, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, xref=null, ext=[AuthorCompanyExt(id=1241719310599647256, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China), AuthorCompanyExt(id=1241719310608035865, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044)])])], keywords=[Keyword(id=1241719311698554942, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, orderNo=1, keyword=train control system), Keyword(id=1241719311761469504, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, orderNo=2, keyword=formal methods), Keyword(id=1241719311832772673, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, orderNo=3, keyword=model-based development), Keyword(id=1241719311904075842, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, orderNo=4, keyword=requirements specification), Keyword(id=1241719311983767618, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, orderNo=5, keyword=modeling and verification), Keyword(id=1241719312105402435, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, orderNo=1, keyword=列车运行控制系统), Keyword(id=1241719312176705604, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, orderNo=2, keyword=形式化方法), Keyword(id=1241719312248008774, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, orderNo=3, keyword=基于模型的开发), Keyword(id=1241719312327700552, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, orderNo=4, keyword=需求规范), Keyword(id=1241719312394809418, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, orderNo=5, keyword=建模验证)], refs=[Reference(id=1241719315284684909, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2023, volume=55, issue=4, pageStart=1, pageEnd=37, url=null, language=null, rfNumber=[1], rfOrder=0, authorNames=Ferrari A, ter Beek M H, journalName=ACM Computing Surveys, refType=null, unstructuredReference=Ferrari A, ter Beek M H. Formal methods in railways: A systematic mapping study[J].
ACM Computing Surveys,
2023,
55(4): 1-37., articleTitle=Formal methods in railways: A systematic mapping study, refAbstract=null), Reference(id=1241719315355988078, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2012, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[2], rfOrder=1, authorNames=唐涛, journalName=列车运行控制系统, refType=null, unstructuredReference=唐涛.
列车运行控制系统[M]. 北京: 中国铁道出版社,
2012., articleTitle=null, refAbstract=null), Reference(id=1241719315418902640, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2008, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[3], rfOrder=2, authorNames=IEEE Vehicular Technology Society, journalName=Piscataway, refType=null, unstructuredReference=IEEE Vehicular Technology Society.IEEE 1474.3-2008 IEEE recommended practice for Communication-Based Train Control (CBTC) system design and functional allocations[S].
Piscataway: IEEE Press,
2008., articleTitle=null, refAbstract=null), Reference(id=1241719315486011506, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2001, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[4], rfOrder=3, authorNames=CENELEC, EN, journalName=Brussels, refType=null, unstructuredReference=CENELEC. EN 50128-2001 Railway application-com-munications, signaling and processing systems-software for railway control and protection systems[S].
Brussels: CENELEC,
2001., articleTitle=null, refAbstract=null), Reference(id=1241719315548926068, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=1015, pageEnd=1020, url=null, language=null, rfNumber=[5], rfOrder=4, authorNames=Di Claudio M, Fantechi A, Martelli G, journalName=Proceedings of the 17th International IEEE Conference on Intelligent Transportation Systems (ITSC). Piscataway:IEEE Press, 2014, refType=null, unstructuredReference=
Di Claudio M,
Fantechi A,
Martelli G, et al. Model-based development of an automatic train operation component for communication based train control[C]//
Proceedings of the 17th International IEEE Conference on Intelligent Transportation Systems (ITSC). Piscataway:IEEE Press, 2014: 1015-1020., articleTitle=Model-based development of an automatic train operation component for communication based train control, refAbstract=null), Reference(id=1241719315620229238, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2019, volume=37, issue=7, pageStart=62, pageEnd=67, url=null, language=null, rfNumber=[6], rfOrder=5, authorNames=蒋立国, 宋春景, 李响, journalName=科技导报, refType=null, unstructuredReference=蒋立国, 宋春景, 李响. MBSE在核工程设计中的应用[J].
科技导报,
2019,
37(7): 62-67., articleTitle=MBSE在核工程设计中的应用, refAbstract=null), Reference(id=1241719315678949496, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2016, volume=29, issue=5, pageStart=45, pageEnd=48, url=null, language=null, rfNumber=[7], rfOrder=6, authorNames=薛威, 贾超群, 李雯, journalName=电子科技, refType=null, unstructuredReference=薛威, 贾超群, 李雯, 等. 基于MBSE在航空电子通信系统中的应用[J].
电子科技,
2016,
29(5): 45-48., articleTitle=基于MBSE在航空电子通信系统中的应用, refAbstract=null), Reference(id=1241719315741864056, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=1996, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[8], rfOrder=7, authorNames=Abrial J R, Hoare A, journalName=The B-book: Assigning programs to meanings, refType=null, unstructuredReference=
Abrial J R,
Hoare A.
The B-book: Assigning programs to meanings[M]. Cambridge: Cambridge University Press,
1996., articleTitle=null, refAbstract=null), Reference(id=1241719315817361530, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=167, pageEnd=183, url=null, language=null, rfNumber=[9], rfOrder=8, authorNames=Fantechi A, journalName=Counsell S, Núñez M. Proceedings of the 11th International Conference on Software Engineering and Formal Methods, SEFM 2013, refType=null, unstructuredReference=
Fantechi A. Twenty-five years of formal methods and railways: What next?[C]//
Counsell S, Núñez M. Proceedings of the 11th International Conference on Software Engineering and Formal Methods, SEFM 2013. Cham: Springer,
2014: 167-183., articleTitle=Twenty-five years of formal methods and railways: What next?, refAbstract=null), Reference(id=1241719315884470395, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=1992, volume=null, issue=null, pageStart=199, pageEnd=213, url=null, language=null, rfNumber=[10], rfOrder=9, authorNames=DaSilva C, Dehbonei B, Mejia F, journalName=Proceedings of the IFIP TC6/WG6.1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE ’92, refType=null, unstructuredReference=
DaSilva C,
Dehbonei B,
Mejia F. Formal specification in the development of industrial applications: Subway speed control system[C]//
Proceedings of the IFIP TC6/WG6.1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE ’92. North-Holland: DBLP,
1992: 199-213., articleTitle=Formal specification in the development of industrial applications: Subway speed control system, refAbstract=null), Reference(id=1241719315947384957, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=1998, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[11], rfOrder=10, authorNames=CENELEC, EN, journalName=Brussels, refType=null, unstructuredReference=CENELEC. EN 50128-1998 Railway applications: Software for railway control and protection systems[S].
Brussels: CENELEC,
1998., articleTitle=null, refAbstract=null), Reference(id=1241719316018688127, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=10.1016/S0022-3093(02)00949-3, pmid=null, pmcid=null, year=2003, volume=303, issue=2, pageStart=253, pageEnd=261, url=https://linkinghub.elsevier.com/retrieve/pii/S0022309302009493, language=null, rfNumber=[12], rfOrder=11, authorNames=Bjørner D, journalName=Journal of Non-Crystalline Solids, refType=null, unstructuredReference=
Bjørner D. New results and trends in formal techniques for the development of software for transportation systems[J].
Journal of Non-Crystalline Solids,
2003,
303(2): 253-261., articleTitle=New results and trends in formal techniques for the development of software for transportation systems, refAbstract=null), Reference(id=1241719316089991297, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=10.1002/iis2.2014.24.issue-1, pmid=null, pmcid=null, year=2014, volume=24, issue=1, pageStart=551, pageEnd=569, url=http://doi.wiley.com/10.1002/iis2.2014.24.issue-1, language=null, rfNumber=[13], rfOrder=12, authorNames=Laporte C Y, Houde R, Marvin J, journalName=INCOSE International Symposium, refType=null, unstructuredReference=
Laporte C Y,
Houde R,
Marvin J. 6.4.2 systems engineering international standards and support tools for very small enterprises[J].
INCOSE International Symposium,
2014,
24(1): 551-569., articleTitle=6.4.2 systems engineering international standards and support tools for very small enterprises, refAbstract=null), Reference(id=1241719316169683075, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2012, volume=33, issue=5, pageStart=91, pageEnd=97, url=null, language=null, rfNumber=[14], rfOrder=13, authorNames=吕继东, 李开成, 唐涛, journalName=中国铁道科学, refType=null, unstructuredReference=吕继东, 李开成, 唐涛, 等. 基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法[J].
中国铁道科学,
2012,
33(5): 91-97., articleTitle=基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法, refAbstract=null), Reference(id=1241719316253569157, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=262, pageEnd=280, url=null, language=null, rfNumber=[15], rfOrder=14, authorNames=Zou L, Lü J D, Wang S L, journalName=null, refType=null, unstructuredReference=
Zou L,
Lü J D,
Wang S L, et al. Verifying Chinese train control system under a combined scenario by theorem proving[C]//Cohen E, Rybalchenko A. Proceedings of the Working Conference on Verified Software:Theories, Tools, and Experiments. Berlin, Heidelberg: Springer,
2014: 262-280., articleTitle=Verifying Chinese train control system under a combined scenario by theorem proving, refAbstract=null), Reference(id=1241719316316483719, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2019, volume=41, issue=9, pageStart=128, pageEnd=null, url=null, language=null, rfNumber=[16], rfOrder=15, authorNames=null, journalName=铁道学报, refType=null, unstructuredReference=北京交通大学轨道交通领域主要成果[J].
铁道学报,
2019,
41(9): 128., articleTitle=北京交通大学轨道交通领域主要成果, refAbstract=null), Reference(id=1241719316387786889, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=308, pageEnd=318, url=null, language=null, rfNumber=[17], rfOrder=16, authorNames=Chen X H, Zhong Z W, Jin Z, journalName=Proceedings of the 2019 IEEE 27th International Requirements Engineering Conference (RE, refType=null, unstructuredReference=
Chen X H,
Zhong Z W,
Jin Z, et al. Automating consistency verification of safety requirements for railway interlocking systems[C]//
Proceedings of the 2019 IEEE 27th International Requirements Engineering Conference (RE 2019). Piscataway:IEEE Press, 2019: 308-318., articleTitle=Automating consistency verification of safety requirements for railway interlocking systems, refAbstract=null), Reference(id=1241719316446507147, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2020, volume=31, issue=5, pageStart=1374, pageEnd=1391, url=null, language=null, rfNumber=[18], rfOrder=17, authorNames=刘筱珊, 袁正恒, 陈小红, journalName=软件学报, refType=null, unstructuredReference=刘筱珊, 袁正恒, 陈小红, 等. 区域控制器的安全需求建模与自动验证[J].
软件学报,
2020,
31(5): 1374-1391., articleTitle=区域控制器的安全需求建模与自动验证, refAbstract=null), Reference(id=1241719316505227405, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2011, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[19], rfOrder=18, authorNames=李雷, journalName=基于SCADE的CBTC区域控制器软件测试方法研究, refType=null, unstructuredReference=李雷.
基于SCADE的CBTC区域控制器软件测试方法研究[D]. 北京: 北京交通大学,
2011., articleTitle=null, refAbstract=null), Reference(id=1241719316584919183, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=2718, pageEnd=2723, url=null, language=null, rfNumber=[20], rfOrder=19, authorNames=Wang H F, Ning B, Chen T, journalName=Proceedings of the 2018 21st International Conference on Intelligent Transportation Systems (ITSC). Piscataway:IEEE Press, 2018, refType=null, unstructuredReference=
Wang H F,
Ning B,
Chen T, et al. Route safety verification of train control system by FTA modeling in SCADE[C]//
Proceedings of the 2018 21st International Conference on Intelligent Transportation Systems (ITSC). Piscataway:IEEE Press, 2018: 2718-2723., articleTitle=Route safety verification of train control system by FTA modeling in SCADE, refAbstract=null), Reference(id=1241719316643639441, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2021, volume=13, issue=3, pageStart=45, pageEnd=57, url=null, language=null, rfNumber=[21], rfOrder=20, authorNames=Zhang Y, Wang H F, Chai M, journalName=IEEE Intelligent Transportation Systems Magazine, refType=null, unstructuredReference=
Zhang Y,
Wang H F,
Chai M, et al. Novel graph-based train control data verification method for Chinese train control system[J].
IEEE Intelligent Transportation Systems Magazine,
2021,
13(3): 45-57., articleTitle=Novel graph-based train control data verification method for Chinese train control system, refAbstract=null), Reference(id=1241719316714942611, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2012, volume=15, issue=3, pageStart=41, pageEnd=44, url=null, language=null, rfNumber=[22], rfOrder=21, authorNames=王倩倩, 张勇, journalName=城市轨道交通研究, refType=null, unstructuredReference=王倩倩, 张勇. UML建模技术在轨道交通CTCS-3级列车控制系统测试案例生成中的应用[J].
城市轨道交通研究,
2012,
15(3): 41-44., articleTitle=UML建模技术在轨道交通CTCS-3级列车控制系统测试案例生成中的应用, refAbstract=null), Reference(id=1241719316782051477, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2015, volume=50, issue=5, pageStart=917, pageEnd=927, url=null, language=null, rfNumber=[23], rfOrder=22, authorNames=吕继东, 朱晓琳, 李开成, journalName=西南交通大学学报, refType=null, unstructuredReference=吕继东, 朱晓琳, 李开成, 等. 基于模型的CTCS-3级列控系统测试案例自动生成方法[J].
西南交通大学学报,
2015,
50(5): 917-927., articleTitle=基于模型的CTCS-3级列控系统测试案例自动生成方法, refAbstract=null), Reference(id=1241719316853354647, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2012, volume=34, issue=5, pageStart=70, pageEnd=80, url=null, language=null, rfNumber=[24], rfOrder=23, authorNames=赵显琼, 郑伟, 唐涛, journalName=铁道学报, refType=null, unstructuredReference=赵显琼, 郑伟, 唐涛. 一种基于模型的形式化测试序列自动生成方法及在ETCS-2中的应用[J].
铁道学报,
2012,
34(5): 70-80., articleTitle=一种基于模型的形式化测试序列自动生成方法及在ETCS-2中的应用, refAbstract=null), Reference(id=1241719316924657817, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2011, volume=47, issue=12, pageStart=4, pageEnd=7, url=null, language=null, rfNumber=[25], rfOrder=24, authorNames=刘雨, 唐涛, 李开成, journalName=铁道通信信号, refType=null, unstructuredReference=刘雨, 唐涛, 李开成, 等. CTCS-3级列控车载设备实验室互联互通测试方法[J].
铁道通信信号,
2011,
47(12): 4-7., articleTitle=CTCS-3级列控车载设备实验室互联互通测试方法, refAbstract=null), Reference(id=1241719317008543899, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=10.1007/s11431-011-4562-2, pmid=null, pmcid=null, year=2011, volume=54, issue=11, pageStart=3078, pageEnd=3090, url=http://link.springer.com/10.1007/s11431-011-4562-2, language=null, rfNumber=[26], rfOrder=25, authorNames=Zhang Y, Tang T, Li K P, journalName=Science China Technological Sciences, refType=null, unstructuredReference=
Zhang Y,
Tang T,
Li K P, et al. Formal verification of safety protocol in train control system[J].
Science China Technological Sciences,
2011,
54(11): 3078-3090., articleTitle=Formal verification of safety protocol in train control system, refAbstract=null), Reference(id=1241719318069702813, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2013, volume=35, issue=6, pageStart=53, pageEnd=58, url=null, language=null, rfNumber=[27], rfOrder=26, authorNames=梁茨, 郑伟, 李开成, journalName=铁道学报, refType=null, unstructuredReference=梁茨, 郑伟, 李开成, 等. 基于路径优化算法的测试序列自动生成及验证[J].
铁道学报,
2013,
35(6): 53-58., articleTitle=基于路径优化算法的测试序列自动生成及验证, refAbstract=null), Reference(id=1241719318149394591, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2015, volume=26, issue=2, pageStart=269, pageEnd=278, url=null, language=null, rfNumber=[28], rfOrder=27, authorNames=陈鑫, 姜鹏, 张一帆, journalName=软件学报, refType=null, unstructuredReference=陈鑫, 姜鹏, 张一帆, 等. 一种面向列车控制系统中安全攸关场景的测试用例自动生成方法[J].
软件学报,
2015,
26(2): 269-278., articleTitle=一种面向列车控制系统中安全攸关场景的测试用例自动生成方法, refAbstract=null), Reference(id=1241719318212309153, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2016, volume=38, issue=1, pageStart=54, pageEnd=64, url=null, language=null, rfNumber=[29], rfOrder=28, authorNames=吕继东, 朱晓琳, 王海峰, journalName=铁道学报, refType=null, unstructuredReference=吕继东, 朱晓琳, 王海峰, 等. 基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究[J].
铁道学报,
2016,
38(1): 54-64., articleTitle=基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究, refAbstract=null), Reference(id=1241719318292000931, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[30], rfOrder=29, authorNames=郭昊男, journalName=新型列控系统车载ATP安全功能在线测试研究, refType=null, unstructuredReference=郭昊男.
新型列控系统车载ATP安全功能在线测试研究[D]. 北京: 北京交通大学,
2019., articleTitle=null, refAbstract=null), Reference(id=1241719318363304101, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=2020, volume=55, issue=5, pageStart=937, pageEnd=945, url=null, language=null, rfNumber=[31], rfOrder=30, authorNames=魏柏全, 吕继东, 陈柯行, journalName=西南交通大学学报, refType=null, unstructuredReference=魏柏全, 吕继东, 陈柯行, 等. 基于TAIO变异的CTCS-3列控系统测试案例生成方法[J].
西南交通大学学报,
2020,
55(5): 937-945., articleTitle=基于TAIO变异的CTCS-3列控系统测试案例生成方法, refAbstract=null), Reference(id=1241719318422024359, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=3951, pageEnd=3956, url=null, language=null, rfNumber=[32], rfOrder=31, authorNames=Gao J J, Lü J D, Chai M, journalName=Proceedings of the 2021 IEEE International Intelligent Transportation Systems Conference (ITSC). Piscataway:IEEE Press, 2021, refType=null, unstructuredReference=
Gao J J,
Lü J D,
Chai M, et al. Train resources conflict detection of NGTC based on probabilistic timed automata[C]//
Proceedings of the 2021 IEEE International Intelligent Transportation Systems Conference (ITSC). Piscataway:IEEE Press, 2021: 3951-3956., articleTitle=Train resources conflict detection of NGTC based on probabilistic timed automata, refAbstract=null)], funds=[Fund(id=1241719315087552616, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, awardId=52272329, language=CN, fundingSource=国家自然科学基金(52272329), fundOrder=null, country=null), Fund(id=1241719315158855786, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, awardId=L201004, language=CN, fundingSource=北京市自然科学基金(L201004), fundOrder=null, country=null)], companyList=[AuthorCompany(id=1241719310587064343, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, xref=null, ext=[AuthorCompanyExt(id=1241719310599647256, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China), AuthorCompanyExt(id=1241719310608035865, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310587064343, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044)]), AuthorCompany(id=1241719310670950427, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, xref=null, ext=[AuthorCompanyExt(id=1241719310679339036, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310670950427, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2. State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China), AuthorCompanyExt(id=1241719310687727645, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, companyId=1241719310670950427, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2.北京交通大学轨道交通控制与安全国家重点实验室，北京 100044)])], figs=[ArticleFig(id=1241719312508055629, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=dqEi30txX28+EYZ5ns+jbA==, figureFileBig=d5Dr6DTWM8VJ7o6w2D+a8w==, tableContent=null), ArticleFig(id=1241719313976062031, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=图1, caption=
列控系统发展趋势, figureFileSmall=dqEi30txX28+EYZ5ns+jbA==, figureFileBig=d5Dr6DTWM8VJ7o6w2D+a8w==, tableContent=null), ArticleFig(id=1241719314169000018, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=YbaFMFUI9vBl2gLSWqVWLQ==, figureFileBig=WOfs9sKdP7qS62BBfJ6ZXA==, tableContent=null), ArticleFig(id=1241719314231914578, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=图2, caption=
形式化语言应用占比 TA：Timed Automata，时间自动机;DSL：Domain-Specific Language，领域特定语言;Statechart：状态迁移图。
, figureFileSmall=YbaFMFUI9vBl2gLSWqVWLQ==, figureFileBig=WOfs9sKdP7qS62BBfJ6ZXA==, tableContent=null), ArticleFig(id=1241719314299023444, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=La2uGK8SoyEm7TR1BQRqWA==, figureFileBig=psSsQrKAS8Hd8rzqLJnk+A==, tableContent=null), ArticleFig(id=1241719314361938006, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=图3, caption=
形式化相关技术应用占比, figureFileSmall=La2uGK8SoyEm7TR1BQRqWA==, figureFileBig=psSsQrKAS8Hd8rzqLJnk+A==, tableContent=null), ArticleFig(id=1241719314433241176, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=/ro5I5QtrqHPjJvDeSXKbw==, figureFileBig=WC/58DKN2JZ6IJGw98QYFw==, tableContent=null), ArticleFig(id=1241719314512932954, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=图4, caption=
列控系统工程研制模式演化, figureFileSmall=/ro5I5QtrqHPjJvDeSXKbw==, figureFileBig=WC/58DKN2JZ6IJGw98QYFw==, tableContent=null), ArticleFig(id=1241719314592624732, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=null, figureFileBig=null, tableContent=
| 软件开发活动 | SIL 0 | SIL 1 | SIL 2 | SIL 3 | SIL 4 |
| 软件需求规范 | R | R | R | HR | HR |
| 软件架构 | — | R | R | HR | HR |
| 软件设计与实现 | R | HR | HR | HR | HR |
| 软件验证与测试 | — | R | R | HR | HR |
| 软件确认 | R | R | R | R | R |
), ArticleFig(id=1241719314659733598, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=表1, caption=
EN 50128 推荐的软件开发活动和形式化应用情况
, figureFileSmall=null, figureFileBig=null, tableContent=
| 软件开发活动 | SIL 0 | SIL 1 | SIL 2 | SIL 3 | SIL 4 |
| 软件需求规范 | R | R | R | HR | HR |
| 软件架构 | — | R | R | HR | HR |
| 软件设计与实现 | R | HR | HR | HR | HR |
| 软件验证与测试 | — | R | R | HR | HR |
| 软件确认 | R | R | R | R | R |
), ArticleFig(id=1241719314743619680, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=null, figureFileBig=null, tableContent=
| 应用 | 功能 | ProB | NuSMV | UPPAAL | CPN | Atelier B | SPIN | Simulink |
| 开发功能 | 规范/建模方式 | 文本 | 文本 | 图形 | 图形 | 文本 | 文本 | 图形 |
| 自动代码生成 | 否 | 否 | 否 | 否 | 是 | 否 | 是 |
| 文档/报告生成 | 部分 | 否 | 部分 | 否 | 部分 | 部分 | 是 |
| 需求可追溯性 | 否 | 否 | 否 | 否 | 否 | 否 | 是 |
| 项目管理 | 是 | 否 | 否 | 是 | 是 | 否 | 是 |
| 验证功能 | 仿真 | 文本/图形 | 文本 | 图形 | 图形 | 否 | 文本 | 图形 |
| 形式化验证方法 | 多种 | 多种 | 多种 | 多种 | 一种 | 一种 | 一种 |
| 基于模型的测试 | 是 | 否 | 是 | 否 | 否 | 否 | 是 |
| 语言表达能力 | 并发性 | 无 | 同步 | 同步 | 异步 | 无 | 异步 | 无 |
| 时序性 | 否 | 是 | 是 | 是 | 否 | 否 | 是 |
| 概率性/随机性 | 否 | 否 | 是 | 否 | 否 | 否 | 否 |
| 浮点数支持 | 否 | 是 | 是 | 否 | 否 | 否 | 是 |
), ArticleFig(id=1241719314827505762, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=表2, caption=
主流形式化工具
, figureFileSmall=null, figureFileBig=null, tableContent=
| 应用 | 功能 | ProB | NuSMV | UPPAAL | CPN | Atelier B | SPIN | Simulink |
| 开发功能 | 规范/建模方式 | 文本 | 文本 | 图形 | 图形 | 文本 | 文本 | 图形 |
| 自动代码生成 | 否 | 否 | 否 | 否 | 是 | 否 | 是 |
| 文档/报告生成 | 部分 | 否 | 部分 | 否 | 部分 | 部分 | 是 |
| 需求可追溯性 | 否 | 否 | 否 | 否 | 否 | 否 | 是 |
| 项目管理 | 是 | 否 | 否 | 是 | 是 | 否 | 是 |
| 验证功能 | 仿真 | 文本/图形 | 文本 | 图形 | 图形 | 否 | 文本 | 图形 |
| 形式化验证方法 | 多种 | 多种 | 多种 | 多种 | 一种 | 一种 | 一种 |
| 基于模型的测试 | 是 | 否 | 是 | 否 | 否 | 否 | 是 |
| 语言表达能力 | 并发性 | 无 | 同步 | 同步 | 异步 | 无 | 异步 | 无 |
| 时序性 | 否 | 是 | 是 | 是 | 否 | 否 | 是 |
| 概率性/随机性 | 否 | 否 | 是 | 否 | 否 | 否 | 否 |
| 浮点数支持 | 否 | 是 | 是 | 否 | 否 | 否 | 是 |
), ArticleFig(id=1241719314911391844, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=EN, label=null, caption=null, figureFileSmall=null, figureFileBig=null, tableContent=
| 项目名称 | 立项年份 | 资助机构 | 涉及研究对象 | 列控相关研究内容 |
| EuroInterlocking | 1999 | 国际铁路联盟 | 联锁 | 为联锁子系统开发功能需求和标准接口，并提供形式化功能需求描述方法和关键验证方法 |
| AVACS | 2004 | 德国科学基金会 | ETCS | ETCS的自动设计、分析和验证技术 |
| EuRailCheck | 2007 | 欧洲铁路局 | ETCS | ETCS规范的形式化建模验证方法及工具 |
| Deploy | 2008 | 欧盟 | CBTC | 开发形式化工程方法，集成建模、分析和代码生成一体的系统级形式化工具链 |
| INESS | 2008 | 欧盟 | 联锁 | 定义新一代联锁子系统的完整规范，开发支持需求规范形式化验证的工具链 |
| OpenETCS | 2009 | 德国联邦教育及研究部等 | ETCS | 为ETCS规范的形式化提供集测试验证与代码生成为一体的工具链 |
| MBAT | 2011 | 欧盟 | CBTC、联锁 | 结合基于形式化模型的测试和静态分析方法，实现对列控系统的验证确认 |
| OpenCOSS | 2011 | 欧盟 | ETCS、联锁 | 设计横跨航空、铁路、汽车的通用认证架构模型，引入“以模型为中心”的安全认证方法，建立开源的安全认证软件工具 |
| SafeCap | 2011 | 英国铁路安全、标准委员会等 | 联锁 | 支持形式化验证联锁子系统安全性的建模工具 |
| RobustRail | 2012 | 丹麦战略研究理事会 | 联锁 | 结合领域方法和形式化方法，提供列控系统的形式化开发与验证技术和工具 |
| PERFECT | 2012 | 欧盟 | ETCS | 为全面评估ETCS规范和欧盟各国铁路信号操作规则在安全方面的一致性提供形式化方法和工具 |
| CRYSTAL | 2013 | 西班牙工业、能源和旅游部等 | ETCS、CBTC | 集成系统需求管理、设计、安全分析和测试的工具链，改善互操作性，弥合系统开发过程中基于模型的系统工程（Model-Based System Engineering, MBSE）和基于模型的安全分析（Model-Based Safety Analysis, MBSA）之间的差距 |
| EULYNX | 2014 | — | 联锁 | 提供基于MBSE方法体系的列控地面子系统的建模规范，定义和标准化未来数字列控系统中的接口 |
| X2Rail-2 | 2017 | 欧盟 | ETCS | 为ETCS的需求捕获、设计、验证和确认提出形式化方法，并应用于具有标准化接口和运营场景的系统开发 |
| 4SECURail | 2019 | 欧盟 | ETCS | 提供最先进的形式化方法和工具的案例，提高系统需求规范的质量 |
| X2Rail-5 | 2020 | 欧盟 | ETCS | 提供可应用于系统体系级（System of System, SoS）的形式化方法和工具链，指定标准接口的MBSE方法，实现需求的形式化和验证 |
), ArticleFig(id=1241719314991083622, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719285861634091, language=CN, label=表3, caption=
列控领域形式化方法应用研究相关项目
, figureFileSmall=null, figureFileBig=null, tableContent=
| 项目名称 | 立项年份 | 资助机构 | 涉及研究对象 | 列控相关研究内容 |
| EuroInterlocking | 1999 | 国际铁路联盟 | 联锁 | 为联锁子系统开发功能需求和标准接口，并提供形式化功能需求描述方法和关键验证方法 |
| AVACS | 2004 | 德国科学基金会 | ETCS | ETCS的自动设计、分析和验证技术 |
| EuRailCheck | 2007 | 欧洲铁路局 | ETCS | ETCS规范的形式化建模验证方法及工具 |
| Deploy | 2008 | 欧盟 | CBTC | 开发形式化工程方法，集成建模、分析和代码生成一体的系统级形式化工具链 |
| INESS | 2008 | 欧盟 | 联锁 | 定义新一代联锁子系统的完整规范，开发支持需求规范形式化验证的工具链 |
| OpenETCS | 2009 | 德国联邦教育及研究部等 | ETCS | 为ETCS规范的形式化提供集测试验证与代码生成为一体的工具链 |
| MBAT | 2011 | 欧盟 | CBTC、联锁 | 结合基于形式化模型的测试和静态分析方法，实现对列控系统的验证确认 |
| OpenCOSS | 2011 | 欧盟 | ETCS、联锁 | 设计横跨航空、铁路、汽车的通用认证架构模型，引入“以模型为中心”的安全认证方法，建立开源的安全认证软件工具 |
| SafeCap | 2011 | 英国铁路安全、标准委员会等 | 联锁 | 支持形式化验证联锁子系统安全性的建模工具 |
| RobustRail | 2012 | 丹麦战略研究理事会 | 联锁 | 结合领域方法和形式化方法，提供列控系统的形式化开发与验证技术和工具 |
| PERFECT | 2012 | 欧盟 | ETCS | 为全面评估ETCS规范和欧盟各国铁路信号操作规则在安全方面的一致性提供形式化方法和工具 |
| CRYSTAL | 2013 | 西班牙工业、能源和旅游部等 | ETCS、CBTC | 集成系统需求管理、设计、安全分析和测试的工具链，改善互操作性，弥合系统开发过程中基于模型的系统工程（Model-Based System Engineering, MBSE）和基于模型的安全分析（Model-Based Safety Analysis, MBSA）之间的差距 |
| EULYNX | 2014 | — | 联锁 | 提供基于MBSE方法体系的列控地面子系统的建模规范，定义和标准化未来数字列控系统中的接口 |
| X2Rail-2 | 2017 | 欧盟 | ETCS | 为ETCS的需求捕获、设计、验证和确认提出形式化方法，并应用于具有标准化接口和运营场景的系统开发 |
| 4SECURail | 2019 | 欧盟 | ETCS | 提供最先进的形式化方法和工具的案例，提高系统需求规范的质量 |
| X2Rail-5 | 2020 | 欧盟 | ETCS | 提供可应用于系统体系级（System of System, SoS）的形式化方法和工具链，指定标准接口的MBSE方法，实现需求的形式化和验证 |
)], attaches=null, journal=Journal(id=1129340393107079197, delFlag=0, nameCn=前瞻科技, nameEn=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, issn=2097-0781, eissn=, cn=10-1786/N, coden=null, periodic=2, language=CN, oaType=null, ccby=null, superviseOffice=null, ownerOffice=null, pubOffice=null, editorOffice=null, officeType=null, aims=null, clcCode=null, officeProv=null, officeCity=null, officeAddr=null, officeZip=null, officeEmail=null, officePhone=null, editDirector=null, officeDirector=null, officeDirectorPhone=null, officeStaffNum=null, officeEmpNum=null, coverPicUrl=ti95jJIJzXaf02YNe1UF2A==, journalPrice=null, startedYear=null, abbrevIsoEn=Sci Technol Fore, journalRemark=null, publicationField=null, createdTime=null, updatedTime=1757931223825, createdBy=null, updatedBy=15831073675, firstLetterCn=S, firstLetterEn=S, subjectCode=Natural Sciences, subjectName=自然科学, subjectCodeEn=Natural Sciences, subjectNameEn=null, picCn=ti95jJIJzXaf02YNe1UF2A==, picEn=cuGsq8KPhoqtfsQROuZvoQ==, jcr=null, cjcr=null, exts=[JournalExt(id=1174411930946125939, language=CN, name=前瞻科技, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/CN/2097-0781/home.shtml, createdTime=1757931223856, updatedTime=1757931223856, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/CN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.cast.org.cn/webm/, submissionEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionReviewUrl=https://qzkjauthor.cast.org.cn/webm/, submissionCeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionAeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, option={"copyright":""}), JournalExt(id=1174411931076149364, language=EN, name=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/EN/2097-0781/home.shtml, createdTime=1757931223887, updatedTime=1757931223887, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/EN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionReviewUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionCeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionAeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, option={"copyright":""})], databaseList=null, tenantJournalId=1146032081894723586, websiteList=[Website(id=1148243202353652128, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/CN, language=CN, createTime=1751692112768, createBy=18614031015, updateTime=1753516254852, updateBy=18614031015, name=《前瞻科技》中文站点, tplId=1146099689490845704, title=前瞻科技, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1148618977242275853, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=articleTextType, value=kx, createTime=1751781704483, updateTime=1751781704483, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977217110026, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=banner, value=null, createTime=1751781704477, updateTime=1751781704477, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977204527113, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1751781704474, updateTime=1751781704474, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977233887244, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1751781704481, updateTime=1751781704481, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977225498635, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1751781704479, updateTime=1751781704479, creator=18614031015, updator=18614031015)]), Website(id=1155894377965830154, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/EN, language=EN, createTime=1753516295187, createBy=18614031015, updateTime=1753516295187, updateBy=18614031015, name=《前瞻科技》英文站点, tplId=1146101810881728533, title=Science and Technology Foresight, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1155894740970233959, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=articleTextType, value=kx, createTime=1753516381733, updateTime=1753516381733, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740953456740, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=banner, value=null, createTime=1753516381729, updateTime=1753516381729, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740945068131, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1753516381727, updateTime=1753516381727, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740966039654, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1753516381732, updateTime=1753516381732, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740961845349, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1753516381731, updateTime=1753516381731, creator=18614031015, updator=18614031015)])], journalTitle=前瞻科技, weixinUrl=null, journalUrl=null, iacademicId=null, status=0, seqNo=null, journalTitleEn=Science and Technology Foresight, journalPhotoCn=ti95jJIJzXaf02YNe1UF2A==, journalPhotoEn=cuGsq8KPhoqtfsQROuZvoQ==, journalFirstLetter=S, journalRecommend=null, journalNew=null, journalCollection=null, jcrJf=null, cjcrJf=null, jcrJfStr=null, cjcrJfStr=null, submissionFirstDecision=null, sciSubjectClassification=null, casSubjectClassification=null, citeScore=null, totalCitationFrequency=null, icpCode=null, psCode=null, advertisingLicenseCode=null, copyrightInformation=null, country=null, option=, provinceCode=null, provinceName=null, collectFlag=false), detailUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.008, detailUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/10.3981/j.issn.2097-0781.2023.01.008, pdfUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/PDF/10.3981/j.issn.2097-0781.2023.01.008, pdfUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/PDF/10.3981/j.issn.2097-0781.2023.01.008, aliStartDate=null, aliEndDate=null, collectionFlag=false, citedCount=null, citedUrl=null, reference=null)
PDF Download
Full
2147
1054
Close Full
