Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2007

Filename

wucse-2007-34.pdf

DOI:

10.7936/K71G0JHQ

Technical Report Number

WUCSE-2007-34

Abstract

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.

Comments

Research at Washington University was supported in part by NSF awards CCF-0615341 (EHS) and CCF-0448562 (CAREER).Permanent URL: http://dx.doi.org/10.7936/K71G0JHQ

Download

Share

COinS