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

时间自动机可达性分析算法的改进 被引量：2

Improvement on a Reachability Analysis Algorithm in Timed Automata
下载PDF
导出
摘要 模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。 For most safety properties and some liveness properties of real-time systems, model checking can be reduced to reachability analysis. In his paper, we introduce timed automata and the algorithm of reachability analysis, and proposes an improvement algorithm of the basic successor algorithm.
作者 张松年 庄雷 杜娟
机构地区 郑州大学信息工程学院
出处 《计算机工程与科学》 CSCD 2007年第10期44-46,共3页 Computer Engineering & Science
关键词 时间自动机 可达性分析 后继 timed automata reachability analysis successor
分类号 TP314 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献8

  • 1Clarke E M,Grumberg O,Peled D A. Model Checking[M]. MIT Press , 1999. 被引量：1
  • 2Alur R,Dill D L. A Theory of Tuned Automata[J]. Journal of Theoretical computer Science,1994,126(2) : 183-235. 被引量：1
  • 3Bengtsson J, Wang Yi. Timed Automata: Semantics, Algorithms and Tools [R]. Technical Report UNU-IIST 316, 2004. 被引量：1
  • 4Henzinger T A, Nieollin X, Sifakis J, et al. Symbolic Model Checking for Realtlme Systems[J]. Information and Computation, 1994,111(2) : 193-244. 被引量：1
  • 5Pagani F. Partial Orders and Verification of Real-Time Systerns[A]. Proe of the 4th Int'l Syrup on Formal Teehnlques in Real-Time and Fault-Tolerant Systems[C]. 1996. 327-346. 被引量：1
  • 6陈铭松,赵建华,李宣东,郑国梁.时间自动机可达性分析中的状态空间约减技术综述[J].计算机科学,2006,33(6):1-6. 被引量：3
  • 7Larsen K G, Larsson F, Pettersson P, et al. Efficient Verification of Real2time Systems: Compact Datastructure and State Space Reduction[A]. Proc of the 18th IEEE Real2Time Systeras Symp[C]. 1997. 被引量：1
  • 8Bozga M, Maler O, Pnueli A, et al. Some Progress in the Symbolic Verification of Timed Automata[A]. Proc of the 1997 Computer-Aided Verification[C]. 1997. 被引量：1

二级参考文献20

  • 1Behrmann G, Bouyer P, Larsen K G, et al. Lower and Upper Bounds in Zone Based Abstractlons of Timed Automata. In:Proc. of the 10th International Conf on Tools and Algorithms for Construction and Analysis of Systems(TACAS ' 2004), Barcelona, Spain, 2004 被引量：1
  • 2ZHAO Jianhua,LI Xuandong,ZHENG Tao, et al. Removing Ir-Trelevant Atomic Formulas for Checking Timed Automata Efficiently. In: Proc. of First International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS), Marseille,France,2003, LNCS 2791:34-45 被引量：1
  • 3Godefroid P. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem.LNCS1032, Springer-Verlag,January 1996 被引量：1
  • 4Bengtsson J, Jonsson B, Lilius J, et al. Partial order reductions for timed systems. In: Proc. of 9th International Conference on Concurrency Theory(CONCUR'98), Nice, France, 1998 被引量：1
  • 5Minea M. Partial order reduction for model checking of timed automata. In: Proc. of 10th International Conference on Concurrency Theory ( CONCUR - 99 ), Eindhoven, Netherlands1999,LNCS1664:431-446 被引量：1
  • 6Zhao Jianhua, Xu He, Li Xuandong, et al. Partial Order Path Technique for Checking Parallel Timed Automata. In: 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT 2002), University of Oldenburg,Germany,2002: LNCS2469. 417-432 被引量：1
  • 7Peled D. All from one,one for all: on model checking using representatives. In: Proc. of the 5th International Conference on Computer Aided Verification ( CAV ' 1993 ), Elounda, Greece, 1993,LNCS697 : 409-423 被引量：1
  • 8Pagani F. Partial orders and verification of real-time systems. In:Proc. of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems(FTRTFT' 96),Uppsala, Sweden, 1996, LNCS1135:327-346 被引量：1
  • 9Alur R, Dill D. Automata for modeling real-time systems. In:Proc. of 17^th International Colloquium on Automata, Languages and Programming ( ICALP ' 90 ), Warwick University, England,1990, LNCS443:322-335 被引量：1
  • 10Alur R, Dill D. A theory of timed automata. Theoretical Computer Science(TCS), 1994,26(2) : 183-235 被引量：1

共引文献2

同被引文献31

  • 1AL-ALI R, AMIN K, LASZEWSKI G V, et al. Analysis and provision of QoS for distributed grid applications[J]. Journal of Grid Computing,2004,2(2) : 163-182. 被引量：1
  • 2BUYYA R, ABRAMSON D, VENUGOPAL S. The grid e- conomy[J]. Proceedings of the IEEE, 2005,93 (3) : 698-714. 被引量：1
  • 3SON J H, KIM M H. Improving the performance of time-con- strained workflow processing[J]. Journal of Systems and Soft- ware, 2001,58(3) :211-219. 被引量：1
  • 4GUERMOUCHE N, PERRIN O, RINGESSEN C. Tn'ned speci- fication for Web services conpatibility analysis [ J]. Electronic Notes in Theoretical Computer Science,2008,200(3):155-170. 被引量：1
  • 5BENATALLAH B, CASATI F, PONGE J, et al. On tempo- ral abstractions of Web service protocols[C]//Proceedings of the CAiSE'05 Forum. Porto, Portugal: University of Porto, 2005 : 39-44. 被引量：1
  • 6KAZHAMIAKIN R, PANDYA P K, PISTORE M. Timed modelling and analysis in Web service compositions[C]//Pro- ceedings of the 1st International Conference on Availability, Reliability and Security. Washington,D. C. , USA.. IEEE Com- puter Society, 2006 : 840-846. 被引量：1
  • 7WANG Hongbing, ZHOU Qianzhao, SHI Yanqi. Describing and verifying Web service composition using TLA reasoning [C]//Proceedings of IEEE International Conference on Serv- ices Computing. Washington, D. C., USA.. IEEE, 2010: 234-241. 被引量：1
  • 8HAO Shengang, ZHANG Li. Dynamic Web services composi- tion based on linear temporal logic[C]//Proceedings of 2010 International Conference of Information Science and Manage- ment Engineering. Washington, D. C. , USA: IEEE, 2010, 1: 362-365. 被引量：1
  • 9GIORDANO L, MARTELLI A. Reasoning about Web serv- ices in a temporal action logic[J]. Lecture Notes in Computer Science, 2006,4155: 229-246. 被引量：1
  • 10BENATALLAH B, CASATI F, TOUMANI- F. Represen- ting, analysing and managing Web service protocols[J]. Data Knowledge Engineering, 2006,58(3) : 327-357. 被引量：1

引证文献2

二级引证文献6

计算机工程与科学
2007年 第10期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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