Christos Stergiou

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2013-163

September 30, 2013

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-163.pdf

We address the schedulability question for PTIDES programs and uniprocessor platforms. A PTIDES program is schedulable if for all legal sensor inputs, there exists a scheduling of the PTIDES components that meets all the specified deadlines. The timing specifications allowed in the discrete-event formalism can be seen as a generalization of end-to-end latencies which are usually studied in the hard real-time computing literature. This results in a rather idiosyncratic schedulability problem. We first show that for a large subset of discrete-event models, the earliest-deadline-first scheduling policy is optimal. Second, we show that all but a finite part of the infinite state space of a PTIDES execution results in demonstrably unschedulable behaviors. As a result the schedulability problem can be reduced to a finite-state reachability problem. We describe this reduction using timed automata.

We next turn to the verification problem for DE systems themselves. We study a basic deterministic DE model, where actors are simple constant-delay components, and two extensions of it: first, one where actors are not constant but introduce non-deterministic delays, and second, one where actors are either deterministic delays or are specified using timed automata. We investigate verification questions on DE models and examine expressiveness relationships between the DE models and timed automata.

Finally, we discuss extensions of this work to cover a wider range of discrete-event actors, and propose an approach to design more efficient and practical analyses for schedulability testing.

Advisors: Edward A. Lee and Koushik Sen

---

BibTeX citation:

@phdthesis{Stergiou:EECS-2013-163,
    Author= {Stergiou, Christos},
    Title= {Schedulability Analysis and Verification of Real-Time Discrete-Event Systems},
    School= {EECS Department, University of California, Berkeley},
    Year= {2013},
    Month= {Sep},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-163.html},
    Number= {UCB/EECS-2013-163},
    Abstract= {We address the schedulability question for PTIDES programs and uniprocessor platforms.  A PTIDES program is schedulable if for all legal sensor inputs, there exists a scheduling of the PTIDES components that meets all the specified deadlines.  The timing specifications allowed in the discrete-event formalism can be seen as a generalization of end-to-end latencies which are usually studied in the hard real-time computing literature.  This results in a rather idiosyncratic schedulability problem.  We first show that for a large subset of discrete-event models, the earliest-deadline-first scheduling policy is optimal.  Second, we show that all but a finite part of the infinite state space of a PTIDES execution results in demonstrably unschedulable behaviors.  As a result the schedulability problem can be reduced to a finite-state reachability problem.  We describe this reduction using timed automata.

We next turn to the verification problem for DE systems themselves.  We study a basic deterministic DE model, where actors are simple constant-delay components, and two extensions of it: first, one where actors are not constant but introduce non-deterministic delays, and second, one where actors are either deterministic delays or are specified using timed automata.  We investigate verification questions on DE models and examine expressiveness relationships between the DE models and timed automata.

Finally, we discuss extensions of this work to cover a wider range of discrete-event actors, and propose an approach to design more efficient and practical analyses for schedulability testing.},
}

EndNote citation:

%0 Thesis
%A Stergiou, Christos 
%T Schedulability Analysis and Verification of Real-Time Discrete-Event Systems
%I EECS Department, University of California, Berkeley
%D 2013
%8 September 30
%@ UCB/EECS-2013-163
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-163.html
%F Stergiou:EECS-2013-163