基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
Uppaal是一种对实时系统模型进行建模和验证的工具,PVS( Prototype Verification System)是开发和分析形式化规格说明的原型证明系统.介绍了Uppaal2PVS翻译器的设计与实现,给出了一种将用Uppaal生成的时间自动机规格说明翻译成PVS文件的方法,从而将模型检查问题转换成了定理证明问题,解决了潜在的状态空间爆炸问题.最后给出了一个实例.
推荐文章
基于Uppaal的时延Petri网到时间自动机等价模型验证
时延Petri网
时间自动机
TPN-to-TA转换
Uppaal
Petri网到VHDL的翻译器设计与实现
Petri网
条件/事件系统
语法分析
翻译器
硬件描述语言
抽象语法树
SpaceWire网络层分析的时间自动机模型
SpaceWire
时间自动机
模型检验
UPPAAL
一种基于时间自动机的域构造方法
模型检验
时间自动机
TCTL
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 Uppaal到PVS的时间自动机翻译器
来源期刊 计算机应用与软件 学科 工学
关键词 时间自动机 翻译器 Uppaal PVS
年,卷(期) 2008,(6) 所属期刊栏目 基金项目论文
研究方向 页码范围 19-20,48
页数 3页 分类号 TP3
字数 1236字 语种 中文
DOI 10.3969/j.issn.1000-386X.2008.06.008
五维指标
作者信息
序号 姓名 单位 发文数 被引次数 H指数 G指数
1 缪淮扣 上海大学计算机工程与科学学院 100 1030 16.0 26.0
2 许庆国 上海大学计算机工程与科学学院 9 35 4.0 5.0
3 刘振通 上海大学计算机工程与科学学院 1 1 1.0 1.0
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (0)
共引文献  (0)
参考文献  (1)
节点文献
引证文献  (1)
同被引文献  (0)
二级引证文献  (0)
1994(1)
  • 参考文献(1)
  • 二级参考文献(0)
2008(0)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(0)
  • 二级引证文献(0)
2010(1)
  • 引证文献(1)
  • 二级引证文献(0)
研究主题发展历程
节点文献
时间自动机
翻译器
Uppaal
PVS
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
计算机应用与软件
月刊
1000-386X
31-1260/TP
大16开
上海市愚园路546号
4-379
1984
chi
出版文献量(篇)
16532
总下载数(次)
47
总被引数(次)
101489
相关基金
国家自然科学基金
英文译名:the National Natural Science Foundation of China
官方网址:http://www.nsfc.gov.cn/
项目类型:青年科学基金项目(面上项目)
学科类型:数理科学
  • 期刊分类
  • 期刊(年)
  • 期刊(期)
  • 期刊推荐
论文1v1指导