返回Google圖書搜尋

Mechanized Verification of Real-time Systems Using PVS.

SRI International. Computer Science LaboratoryNatarajan Shankar

出版	SRI International, Computer Science Laboratory, 1992
URL	http://books.google.com.hk/books?id=n63MGwAACAAJ&hl=&source=gbs_api

註釋Abstract: "Some important properties of certain safety-critical systems can be established only by a careful analysis of their real-time behavior. These real-time systems are typically designed to also meet functional requirements where the real-time behavior is irrelevant. A suitable verification framework for such systems must therefore be capable of coping with functional as well as real-time behavior. We present an approach to the verification of the real-time behavior of concurrent programs and describe its mechanization using the PVS proof checker. Our approach to real-time behavior extends previous verification techniques for concurrent programs by introducing a new operator for reasoning about absolute time