期刊文献+

数理逻辑的程序可靠性验证 被引量:1

Validation of Reliability on Mathematical Logic Program
下载PDF
导出
摘要 程序可靠性验证往往占用软件开发周期很长的时间,而现行的软件可靠性验证方法主要是基于形式化的方法如基于SPIN的模型检测方法等,但这种方法可能由于模型建立的问题导致验证的复杂性极大提高,造成最后验证失败的结果比比皆是。为解决此问题,本文使用数学方法从数理逻辑角度用推理的方法实现了程序可靠性验证,并完成了客户服务器程序的可靠性验证,证明了该方法切实有效。 The reliability verification of program often takes a very long time to develope the software, while the current software reliability verification method is mainly based on formal methods such as SPIN based on model checking method, but this method may lead to the complexity of verification to improve greatly bing due to model problems, and then finally fails in validation results everywhere. In order to solve this problem, this paper used mathematical methods from mathematical logic perspective to realize the program reliability verification, and completed the reliability verification of client server program, the method was be proved the validity in true.
作者 顾名宇
出处 《山东农业大学学报(自然科学版)》 CSCD 2015年第4期621-624,共4页 Journal of Shandong Agricultural University:Natural Science Edition
关键词 数理逻辑 程序 可靠性 Mathematical logic program validation
  • 相关文献

参考文献7

二级参考文献15

  • 1周明天,谭良.可信计算及其进展[J].电子科技大学学报,2006,35(S1):686-697. 被引量:27
  • 2Lu Si-mei, Zhang Jian-lin, and Luo Li-ming. The automatic verification and improvement of SET protocol model with SMV[C]. Proceedings of Information Engineering and Electronic Commerce, Ternopil, Ukraine, 2009: 433-436.
  • 3Mclnnes A I. Model-checking the flooding time synchronization protocol control and automation[C]. Proceedings of ICCA 2009, Christchurch, 2009: 422-429.
  • 4Biere A, Cimatti A, and Clarke E M, et al.. Bounded model checking[J]. Advances in Computers, 2003, 58: 117-148.
  • 5Lima V, Talhi C, and Mouheb D, et al.. Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages[J]. Electronic Notes in Theoretical Computer Science, 2009, 254: 143-160.
  • 6Li Jing and Li 3in-hua. Model checking the SET purchasing process protocol with SPIN[C]. Proceedings of 5th International Conference on Wireless Communications, Networking and Mobile Computing, Beijing, 2009: 1-4.
  • 7Islam S M S, Sqalli M H, and Khan S. Modeling and formal verification of DHCP using SPIN[J]. International Journal of Computer Science & Application, 2006, 2(6): 145-159.
  • 8O‘Leary J, Saha B, and Tuttle M R. Model checking transactional memory with spin[C]. Proc. of the twentyseventh ACM symposium on Principles of distributed computing, Montreal, QC, 2009: 335-342.
  • 9Flanagan C and Godefroid P. Dynamic partial-order reduction for model checking software[J]. A CM SIGPLAN Notices, 2005, 40(1): 110-121.
  • 10Holzmann G J. The Spin Model Checker: Primer and Reference Manual[M]. First edition, Boston: Addison Wesley, 2004: 217-360.

共引文献18

同被引文献8

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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