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

基于Uppaal的时延Petri网到时间自动机等价模型验证 被引量：1

Model Checking of Timed Petri Nets to Semantically Equivalent Timed Automata Based on Uppaal
下载PDF
导出
摘要 时延Petri网和时间自动机都可以有效地对实时系统的行为进行模拟和性能分析。利用时延Petri网到时间自动机等价转换算法(简记作TPNtoTA转换),将一个描述实时系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型。使用时间自动机中成熟的模型验证工具Uppaal对此时延Petri网的模型进行验证。 Both timed Petri nets and timed automata can carry on behavior simulation and performance analysis to the real-time system effectively.Utilizes a translation algorithm (referred to as TPN-to-TA translation) which can map a timed Petri nets model of real-time system into a collect of semantically equivalent timed automata, use a mature model checker Uppaal for timed automata to verify the performance of this timed Petri nets model.
作者 周清雷 王静
机构地区 郑州大学信息工程学院 信息工程大学信息工程学院
出处 《计算机应用研究》 CSCD 北大核心 2005年第6期64-66,共3页 Application Research of Computers
基金 国家自然科学基金资助项目(69873040)
关键词 时延PETRI网 时间自动机 TPN-to-TA转换 UPPAAL Timed Petri Nets Timed Automata TPN-to-TA Translation Uppaal
分类号 TP301.1 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献9

  • 1Zonghua Gu, Kang G Shin. Analysis of Event-driven Real-time Systems with Time Petfi Nets: A Translation-based Approach [ C]. Norwell, MA: Kluwer Academic Publishers, 2002. 31-40.
  • 2R Alur, D L Dill. A Theory of Timed Automata [ J ]. Theoretical Computer Science, 1994, 126: 183-235.
  • 3R Alur. Timed Automata[ C]. Heidelberg: Springer-Vedag Heidelberg, 1999. 8-22.
  • 4Johan Bengtsson, Fredrik Larsson. Uppaal A Tool for Automatic Verification of Real-time Systems [ D ]. Sweden: Uppsala University,1996.1-69.
  • 5Johan Bengtsson, Kim G Larsen, Fredrik Larsson, et al. UPPAAL:A Tool Suite for Automatic Verification of Real-time Systems [ M ]. NewYork: Springer-Verlag, 1996. 232-243.
  • 6Zonghua Gu, Kang G Shin. An Integrated Approach to Modeling and Analysis of Embedded Real-time Systems Based on Timed Petri Nets[ C]. Washington D C: IEEE Computer Society, 2003. 350-359.
  • 7R Alur, D L Dill. Automata-theoretic Verification of Real-time systems[ M]. New York: John Wiley & Sons Publishers, 1996. 55-82.
  • 8Sungdeok Cha, Hanseong Son, Junbeom Yoo, et al . Systematic Evaluation of Fault Trees Using Real-time Model Checker UPPAAL[ J]. Reliability Engineering and System Safety, 2003, 82 : 11-20.
  • 9L A Cortes, P Eles, Z Peng. Verification of Embedded Systems Using a Petri Net-based Representation[ C]. New York: ACM Press, 2000.149-155.

同被引文献7

  • 1Cassez F, Roux O H. Structural translation from Time Petri Nets to Timed Automata- Model-Checking Time Petri Nets via Timed Automata [J]. The journal of Systems and Software, 2006,79(10) :1456-1468.
  • 2Gu Zonghua, Shin K G. Analysis of Event-Driven Real-Time Systems with Time Petri Nets: A Translation Based Approach [C]. Norwell, MA : Kluwer Academic Publishers, 2002,31 (40) : 31 -40.
  • 3Schmidt D D. MDE4DRE: Model-Driven Engineering for Distributed Real-time and Embedded Systems [C]// 13th IEEE Real-Time and Embedded Technology and Applications Symposium. Washington, 2007.
  • 4Boucheneb H, Hadjidj R. CTL model checking for time Petri nets[J]. Theoretical Computer Science, 2006,353 (1) : 208-227.
  • 5Berard B, Cassez F, Haddad S, et al. Comparison of the Expressive heSS of Timed Automata and Time Petri Nets [C]// 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 05). volume 3829 of Lecture Notes in Computer Science. Uppsala, Sweden, Springer. , September 2005.
  • 6Boniol F, Wiels V, Ledinot E. Experiences in using model e-hecking to verify real time properties of a landing gear control system[C]. 3rd European Congress Embedded Real Time Software, ERTS, 2006.
  • 7Dotoli M,Fanti M P. A colored Petri net model for automated storage and retrieval systems serviced by rail-guided vehicles: a control perspective[J]. International Journal of Computer Integrated Manufacturing, 2005,18(2/3) :122-136.

引证文献1

二级引证文献5

计算机应用研究
2005年 第6期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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