项目名称: 实时安全关键系统的建模、仿真与验证

项目编号: No.61272118

项目类型: 面上项目

立项/批准年度: 2013

项目学科: 自动化技术、计算机技术

项目作者: 王小兵

作者单位: 西安电子科技大学

项目金额: 80万元

中文摘要: 扩展投影时序逻辑PTL(Projection Temporal Logic)为实时时序逻辑TPTL(Timed PTL),研究其语法、语义及逻辑规则。定义TPTL的命题子集-TPPTL(Timed Propositional PTL)作为实时安全关键系统(Real-Time Safety-Critical System,RTSCS)的规范语言,并研究其可判定性与判定算法。定义TPTL的可执行子集-实时时序逻辑程序设计语言RT-MSVL(Real-Time Modeling,Simulation and Verification Language)作为RTSCS的建模语言,研究其操作语义。研究RT-MSVL的解释执行技术与模型检测算法,设计并实现集建模、仿真与验证于一体的RT-MSVL解释器。将TPPTL与RT-MSVL应用于典型RTSCS,例如高速列车控制系统,研究其建模、仿真与验证技术。

中文关键词: 时序逻辑;时序逻辑语言;实时安全关键系统;模型检测;

英文摘要: The syntax,semantics and logic laws of Timed Projection Temporal Logic(TPTL) are investigated based on Projection Temporal Logic.Timed Propositional PTL(TPPTL) which is a propositional subset of TPTL is defined as a specification language for Real-Time Safety-Critical System(RTSCS), then its decidability and decision algorithm are studied.A real-time temporal logic programming language RT-MSVL(Real-Time Modeling, Simulation and Verification Languag)which is an executable subset of TPTL is formalized as an modeling language for RTSCS, and its operational semantics are explored. The interpreter of RT-MSVL is designed and developed according to its reduction rules and model checking algorithm, which is a uniform modeling, simulation and verification platform with real-time temporal logic for RTSCS.TPPTL and RT-MSVL are applied to model, simulate and verify RTSCS to ensure their safety and reliability, such as high-speed railway control systems.

英文关键词: temporal logic;temporal logic languages;real-time safety-critical system;model checking;

成为VIP会员查看完整内容
1

相关内容

军事知识图谱构建技术
专知会员服务
116+阅读 · 2022年4月8日
专知会员服务
30+阅读 · 2021年9月14日
【干货书】面向计算科学和工程的Python导论,167页pdf
专知会员服务
41+阅读 · 2021年4月7日
专知会员服务
53+阅读 · 2021年4月3日
专知会员服务
25+阅读 · 2021年4月2日
专知会员服务
13+阅读 · 2020年12月12日
面向B端算法实时业务支撑的工程实践
阿里技术
0+阅读 · 2022年2月10日
智能合约的形式化验证方法研究综述
专知
15+阅读 · 2021年5月8日
【Flink】基于 Flink 的流式数据实时去重
AINLP
14+阅读 · 2020年9月29日
无人驾驶仿真软件
智能交通技术
21+阅读 · 2019年5月9日
自动驾驶仿真软件列表
智能交通技术
13+阅读 · 2019年5月9日
无人驾驶开源仿真平台整理
智能交通技术
26+阅读 · 2019年5月9日
已删除
将门创投
10+阅读 · 2019年3月6日
一种关键字提取新方法
1号机器人网
21+阅读 · 2018年11月15日
形式化方法的研究进展与趋势
中国计算机学会
35+阅读 · 2018年11月8日
国家自然科学基金
2+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
6+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2022年4月20日
Arxiv
0+阅读 · 2022年4月19日
Arxiv
0+阅读 · 2022年4月18日
Arxiv
0+阅读 · 2022年4月17日
Arxiv
24+阅读 · 2021年1月25日
Arxiv
15+阅读 · 2019年6月25日
小贴士
相关VIP内容
军事知识图谱构建技术
专知会员服务
116+阅读 · 2022年4月8日
专知会员服务
30+阅读 · 2021年9月14日
【干货书】面向计算科学和工程的Python导论,167页pdf
专知会员服务
41+阅读 · 2021年4月7日
专知会员服务
53+阅读 · 2021年4月3日
专知会员服务
25+阅读 · 2021年4月2日
专知会员服务
13+阅读 · 2020年12月12日
相关资讯
面向B端算法实时业务支撑的工程实践
阿里技术
0+阅读 · 2022年2月10日
智能合约的形式化验证方法研究综述
专知
15+阅读 · 2021年5月8日
【Flink】基于 Flink 的流式数据实时去重
AINLP
14+阅读 · 2020年9月29日
无人驾驶仿真软件
智能交通技术
21+阅读 · 2019年5月9日
自动驾驶仿真软件列表
智能交通技术
13+阅读 · 2019年5月9日
无人驾驶开源仿真平台整理
智能交通技术
26+阅读 · 2019年5月9日
已删除
将门创投
10+阅读 · 2019年3月6日
一种关键字提取新方法
1号机器人网
21+阅读 · 2018年11月15日
形式化方法的研究进展与趋势
中国计算机学会
35+阅读 · 2018年11月8日
相关基金
国家自然科学基金
2+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
6+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
相关论文
Arxiv
0+阅读 · 2022年4月20日
Arxiv
0+阅读 · 2022年4月19日
Arxiv
0+阅读 · 2022年4月18日
Arxiv
0+阅读 · 2022年4月17日
Arxiv
24+阅读 · 2021年1月25日
Arxiv
15+阅读 · 2019年6月25日
微信扫码咨询专知VIP会员