The technical contribution of this paper is a particular way of adding model-checking to the repertoire of more familiar techniques (such as rate monotonic analysis) for analyzing real-time behavior. Model-checking comprises automated methods of search and reasoning that apply, in principle, to any system representable as a finite state machine. It can be used to verify not only that deadlines are met but other system properties as well. The methods we propose are general, but are applied in the context of a specific solution to the problem of safety-critical runtime support. The Ravenscar subset of Ada tasking is designed to support pre-emptive scheduling while requiring minimal runtime support. The Ravenscar profile is supported by the RAVEN/sup TM/ runtime, developed at Aonix to be FAA certifiable. Our immediate goal is to verify Ravenscar programs running on RAVEN/sup TM/.
Analysis of real-time code by model checking
19th DASC. 19th Digital Avionics Systems Conference. Proceedings (Cat. No.00CH37126) ; 1 ; 1D5/1-1D5/8 vol.1
01.01.2000
678415 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Analysis of Real-Time Code by Model Checking
British Library Conference Proceedings | 2000
|Logic Model Checking of Time-Periodic Real-Time Systems
NTRS | 2012
|Logic Model Checking of Time-Periodic Real-Time Systems
AIAA | 2012
|