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

基于SPIN的系统建模研究 被引量：1

Research on System Modeling Based on SPIN
下载PDF
导出
摘要 模型检测由于其自动化程度高,是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器,首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理,并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型,并对实验结果进行分析。 Because of the high degree of automation, model checking technology has become one of the most popular way to en- sure correctness in the formal verification field. To use the model checker, the user should model the verification-needed system. This paper summarizes the basic principles of model checking technology and explores the Promela modeling with model checker SPIN. Finally, a simple bus operation prototype model is given, and the experimental results are analyzed.
作者 徐小丽
机构地区 北京航空航天大学计算机学院
出处 《计算机与现代化》 2012年第9期209-214,共6页 Computer and Modernization
关键词 模型检测 建模 SPIN PROMELA model checking modeling SPIN Promela
分类号 TP311.53 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献20

  • 1林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(12A):1907-1912. 被引量：163
  • 2Clarke E M,Grumberg 0, Peled D A. Model Checking [M] . Cambridge, MA: MIT Press, 1999.
  • 3Holzmann G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997,23(5) ;279-295.
  • 4戎玫,张广泉.模型检测新技术研究[J].计算机科学,2003,30(5):102-104. 被引量：22
  • 5Emerson E Allen,Lei Chin-Laung. Efficient model checking in fragments of the prepositional Mu-Calculus [ C]// Proceedings of 1st IEEE Symposium on Logic in Computer Science. 1986 :267-278.
  • 6Walter Bemd. Timed Petri-nets for modeling and analyzing protocols with real-time characteristics [ C]// Proceedings of 3rd IFIP WG 6. 1 International Workshop on Protocol Specification, Testing, and Verification. Amsterdam ; North-Holland, 1983 : 149-159.
  • 7Coolahan Jr James E, Roussopoulos Nick. A timed Petri net methodology for specifying real-time system timing requirements [C ]//International Workshop on Timed Petri.
  • 8Dill David L. Timing assumptions and verification of finite-state concurrent systems [ C ]//Lecture Notes in Computer Science 407-International Workshop on Automatic Verification Methods for Finite State System(89) . 1990: 197-212.
  • 9Alur Rajeev, Courcoubetis Costas, Dill David L. Model-checking for real time systems [ C//Proceedings of the 5 th IEEE Symposium on Logic in Computer Science. 1990 : 414425.
  • 10Wang Yi. CCS + Time = An interleaving model for real time systems [ C]// Proceedings of the 18th International Colloquium on Automata, Languages and Programming. 1991 : 217-228.

二级参考文献15

  • 1Alur R. Henzinger T A. Real-time logics:Complexity and expressiveness, In: Proc. 5th IEEE Symp.Logic in Comput, Sci. 1990, 390~401.
  • 2Berard B, Bidoit M, Finkel A, et al. Systems and Software Verlfication: Model-Checking Techniques and Tools. Springer,Z001.
  • 3Henzinger T A, P H Ho.HyTech: a model checker for hybrid systems. CAV'97, LNCS1254,1997. 460~463.
  • 4Clarke E M, Wing J M. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 1996,28 (4).
  • 5Manna Z, SteP group. SteP:The Steandford Temporal Prover.STAN-CS-TR-95,1562, 1995.
  • 6Peled D A. Software Reliability Methods. Springer,2001.
  • 7Manna Z, Pnueli A. Temporal Verification Reactive Systems:Safety. New York, Springer-Verlag, 1995.
  • 8Inan M K. Kurshan R P. Verification of Digital and Hybrid Systems. Springer, 2000.
  • 9Pnueli A. Verification Engineering : A Future Profession. (A. M.Turing Award Lecture)Sixteenth Annual ACM Symposium on Principles of Distributed Computing, San Diego, Aug. 1997.
  • 10Clarke E M, Grumberg J O, Peled D A. Model Checking. MIT.1999.

共引文献179

同被引文献14

引证文献1

二级引证文献1

计算机与现代化
2012年 第9期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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