Scheduling design and verification for open soft real-time systems

Open soft real-time systems, such as mobile robots, experi-ence unpredictable interactions with their environments and yet must respond both adaptively and with reasonable tem-poral predictability. New scheduling approaches are needed to address the demands of such systems, in which many of the assumptions made by traditional real-time scheduling theory do not hold. In previous work we established foun-dations for a scheduling policy design and verification ap-proach for open soft real-time systems, that can use different decision models, e.g., a Markov Decision Process (MDP), to capture the nuances of their scheduling semantics. However, several important refinements to the prelimi-nary techniques developed in that work are needed to make the approach applicable in practice. This paper makes three main contributions to the state of the art in scheduling open soft real-time systems: (1) it defines a novel representation of the scheduling state space that is both more compact and more expressive than the model defined in our previ-ous work; (2) it exploits regular structure of that represen-tation to allow efficient verification of properties involving both discrete and continuous system state variables under specific scheduling policies; and (3) it removes the unnec-essary use of a time horizon in our previous approach, thus allowing the more precise specification and enforcement of a wider range of scheduling policies for open soft real-time systems.