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.
Rushby, John (SRI International Corp. Menlo Park, CA, United States)
August 16, 2013
April 1, 1993
Publication: CNES, Real-Time Embedded Processing for Space Applications