期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于UPPAAL软件的实时系统设计研究 被引量：1

Using UPPAAL Tool Modeling and Verifying a Real Time System
下载PDF
导出
摘要 UPPAAL是丹麦Aalborg和瑞士Uppsala大学联合开发,具有世界先进水平的实时系统模拟,校核的软件,基于对实时系统严密逻辑,真实时间的抽象,而构建时间状态机动态模型网络,模拟,校核系统,检测潜在失败,保证设计可靠性,雷达传感器内存接口实时系统是航天雷达系统重要组成部分。本文UPPAAL软件对此系统精确的动态数学模型,模拟,校核系统,覆盖各设计阶段,保证实时系统设计可靠性。 UPPAAL is integrated tool software of modeling , simulation, verification for the real time system , that developed jointly by Aalborg university in Denmark and Uppsala university in Sweden have the advanced level in the world . that is constructed dynamic model as the network of timed automata with rigorous logic and real timed abstraction of real time system and simulates , verifies the system. That detects potential faults in the system, and guarantee the reliability of the design. the real time system of memory interface in the radar sensor is modeled and verified to check potential faults in the system by UPPAAL software, that covers each phase of the design. And guarantees the reliability of the design of the real time system.
作者 李乃斌
机构地区 中国重型汽车公司技术发展中心
出处 《航空计算技术》 2004年第4期70-72,共3页 Aeronautical Computing Technique
关键词 UPPAAL 时间状态机 模拟 模型检查 校验 UPPAAL timed automata simulation model check verification
分类号 TP317 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献3

  • 1[1]Kim G. Larsen, Paul Pettersson and Wang Yi. UPPAAL in a Nutshell. In Springer Internarional Journal of Software Tools for Technology Transfer(1 + 2) ,1997.
  • 2[2]Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson,Wang Yi. "UPPAAL in 1995". Workshop on Tools and Algorithms for the Construction and Aualysis of Systcms, Passau,Germany,27-29 March,1996. LNCS 1055,pages 431 -434,T. Margaria and B. Steffen(Eds).
  • 3[3]Kim G. Larsen, Paul Pettersson and Wang Yi "UPPAAL:Status & Developments" the 9th Intemational Conferenee on Computcr- Aided Verifcation. Haifa, Isracl, 22 - 25 June1997.

同被引文献8

  • 1ARINC 664P7.Avionics Full Duplex Switched Ethemet(AFDX)Networks[S].ARINC 664 Specification Part 7,2005.6.27.
  • 2Cruz Rene L.A Calculus for Network Delay,Part Ⅰ:Network Elements in Isolation Part Ⅱ:Network Analysis[J].IEEE Trans.on Info.Theory,1991,37(1):114-131,132-141.
  • 3LeBoudec J Y,Thiran P.Network Calculus-A Theory of Deterministic Queuing Systems for the Intemet[M].Berlin:Springer Verlag-LNCS 2050,2004.
  • 4Bauer Henri,Scharbarg Jean-Luc,Fraboul Christian.Improving the Worst-Case Delay Analysis of an AFDX Network Using an Optimized Trajectory Approach[J].IEEE Trans.on Industrial Informatics,2010,6(4):1-11.
  • 5Charara H,Scharbarg J L,Ermont J,et al.Methods for Bounding End-to-End Delays on an AFDX Network[A].IEEE 18th EuroMicro Conf.on Real-Time Systems[C].Dresden,Germany:IEEE Computer Society Washington,2006:193-202.
  • 6Gerd B,Alexandre D,Larsen K G.A Tutorial on Uppaal[Z].Department of Computer Science Aalborg University,2004.
  • 7Yao M,Qiu z,Kwak K.Leaky Bucket Algorithms in AFDX[J].Electronics Letters 21st,2009,45(11):543-545.
  • 8Aceto L,Bouyer P,et al.The Power of Reachability Testing for Timed Automata[J].Theor.Compu.Sci,2003:1-3(300):411-475.

引证文献1

二级引证文献2

航空计算技术
2004年 第4期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部