Time and Event Based System Software Design and Verification

June 27, 2008

Chris Gill


Time and Event Based System Software Design and Verification

Time:   4:15pm
Location:   Amphitheatre H-1005

Distributed real-time system software consists of layered stacks of mechanisms, including: operating system level threads, ports, sockets, and timers; low-level middleware abstractions such as reactors and monitor objects; and high-level middleware services such as gateways and request brokers. In these systems, task chains span multiple hosts and may be initiated asynchronously. Furthermore, limited host resources must be shared among competing task chains according to policies that can ensure safety, liveness, and timing properties end-to-end. Our research, which has been supported in part by NSF awards CCF-0448562 (CAREER) and CNS-0716764 (Cybertrust), focuses on system software design, modeling, verification and property enforcement in distributed real-time systems.

This talk summarizes the evolution of our research over the past two years, from a focus on middleware modeling and property enforcement, towards higher level work on real-time component models and verification tool chains, and towards lower level work on scheduling policy design and verification in diverse operating environments. A brief survey of results from our prior research collaborations, on timed automata models for middleware verification and protocols and mechanisms for property enforcement, is given first as background for our current work. The second part of the talk presents our work on a new real-time component model designed specifically for distributed real-time component middleware with different concurrency configurations. The third part of the talk describes our work on scheduling policy design and verification for open soft real-time systems, including methods for designing and verifying scheduling policies under realistic degrees of variability in system timing behavior.