Number : WUCSE-2007-34 2007 Scheduling Induced Bounds and the Verification of Preemptive Real-Time Systems

Distributed real-time and embedded (DRE) systems have stringent constraints on timeliness and other properties whose assurance is crucial to correct system behavior. Our previous research has shown that detailed models of essential middleware mechanisms can be developed, composed, and for constrained examples verified tractably, using state of the art timed automata model checkers. However, to apply model checking to a wider range of real-time systems, particularly those involving more general forms of preemptive concurrency, new techniques are needed to address decidability and tractability concerns. This paper makes three contributions to research on formal verification and validation of DRE systems. First, it describes how bounded fair scheduling policies introduce a quasi-cyclic structure in the state space of multi-threaded real-time systems. Second, it shows that bounds on the divergence of threads' execution can be determined for that quasi-cyclic structure, which then can be exploited to reduce the complexity of model checking. Third, it presents a case study involving progress-based fair scheduling of multi-threaded processing pipelines, with which the approach is evaluated. Notes: Research at Washington University was supported in part by NSF awards CCF-0615341 (EHS) and Type of Report: Other Department of Computer Science & Engineering Washington University in St. Louis Campus Box 1045 St. Louis, MO 63130 ph: (314) 935-6160 Scheduling Induced Bounds and the Verification of Preemptive Real-Time Systems ∗ Terry Tidwell and Christopher Gill CSE Department, Washington University St. Louis, MO, USA {ttidwell,cdgill}@cse.wustl.edu Venkita Subramonian AT&T Labs, Inc. Florham Park, NJ, USA venkita@research.att.com