Schedulability Analysis and Verification of Real-Time Discrete-Event Systems

Cyber-physical systems are systems where there is a tight interaction between the computing world and the physical world. In spite of the significance of time in the dynamics of the physical world, real-time embedded software today is commonly built using programming abstractions with little or no temporal semantics. PTIDES (Programming Temporally Integrated Distributed Embedded Systems) is a programming model whose goal is to address this problem. It proposes a model-based design approach for the programming of distributed real-time embedded systems, in which the timing of real-time operations is specified as part of the model. This is accomplished by using as an underlying formalism a discrete-event (DE) model of computation, which is extended with real-time semantics.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