Earticle

초록

영어

With the continuous increase in the size and complexity of a real-time computer system, the use of formal verification methods in software development is also on the rise. The traditional formal verification method is not fully applicable to the development of actual system life cycle. Therefore, this paper presents a new real-time system verification method, It takes the deadlock timed Büchi automata as the medium, and translates the timed temporal logic into timed communicating sequential process language. The tock event is also joined, which can be directly used for the detection of refinement tool FDR. The method verifies the situation of deadlock. To establish the link between the conventional model checking and refinement model checking can well combine the advantages of both and improves system security and reliability.

목차

Abstract
 1. Introduction
 2. Preliminaries
 3. Refinement Verification based on TLTL
  3.1 Refinement Verification
  3.2 Conversion of TLTL
  3.3 Refinement Verification Process
 4. Verification Case: Railway Crossing
 5 . Conclusions
 Acknowledgements
 References

키워드

저자

• Jing GUO [ School of Electronics & Information Engineering ,Tongji University Shanghai ,China ]
• Zhong-wei XU [ School of Electronics & Information Engineering ,Tongji University Shanghai ,China ]
• Meng MEI [ School of Electronics & Information Engineering ,Tongji University Shanghai ,China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Grid and Distributed Computing

• 간기

  격월간

• pISSN

  2005-4262

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605