Title :
A Conservative Approximation Method for the Verification of Preemptive Scheduling Using Timed Automata
Author :
Madl, Gabor ; Dutt, Nikil ; Abdelwahed, Sherif
Author_Institution :
Univ. of California, Irvine, CA
Abstract :
This paper presents a conservative approximation method for the real-time verification of asynchronous event-driven distributed systems. This problem is known to be undecidable in the generic setting. The proposed approach is based on composable timed automata models that provide a sufficient condition to determine schedulability. We demonstrate the method on a real-time CORBA avionics design.
Keywords :
automata theory; distributed object management; formal verification; asynchronous event-driven distributed systems; composable timed automata models; conservative approximation method; preemptive scheduling verification; real-time CORBA avionics design; real-time verification; timed automata; Approximation methods; Automata; Dynamic scheduling; Energy consumption; Mathematical model; Mission critical systems; Reachability analysis; Real time systems; Sufficient conditions; USA Councils; Model checking; distributed real-time embedded; preemptive scheduling; timed automata;
Conference_Titel :
Real-Time and Embedded Technology and Applications Symposium, 2009. RTAS 2009. 15th IEEE
Conference_Location :
San Francisco, CA
Print_ISBN :
978-0-7695-3636-1
DOI :
10.1109/RTAS.2009.32
