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

fYear

2009

fDate

13-16 April 2009

Firstpage

255

Lastpage

264

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time and Embedded Technology and Applications Symposium, 2009. RTAS 2009. 15th IEEE

Conference_Location

San Francisco, CA

ISSN

1545-3421

Print_ISBN

978-0-7695-3636-1

Type

conf

DOI

10.1109/RTAS.2009.32

Filename

4840586