NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal methods for dependable real-time systemsThe motivation for using formal methods to specify and reason about real time properties is outlined and approaches that were proposed and used are sketched. The formal verifications of clock synchronization algorithms are concluded as showing that mechanically supported reasoning about complex real time behavior is feasible. However, there was significant increase in the effectiveness of verification systems since those verifications were performed, at it is to be expected that verifications of comparable difficulty will become fairly routine. The current challenge lies in developing perspicuous and economical approaches to the formalization and specification of real time properties.
Document ID
19940022237
Document Type
Conference Paper
Authors
Rushby, John (SRI International Corp. Menlo Park, CA, United States)
Date Acquired
August 16, 2013
Publication Date
April 1, 1993
Publication Information
Publication: CNES, Real-Time Embedded Processing for Space Applications
Subject Category
COMPUTER OPERATIONS AND HARDWARE
Funding Number(s)
CONTRACT_GRANT: NAS1-18969
CONTRACT_GRANT: N00014-92-C-2177
CONTRACT_GRANT: NAS1-18266
Distribution Limits
Public
Copyright
Other