- This event has passed.
Model-based Analysis of Event-driven Distributed Real-time Embedded Systems
May 27, 2009 @ 3:00 pm - 4:00 pm PDT
Model-based Analysis of Event-driven Distributed Real-time Embedded Systems
by Gabor Madl
Location: DBH 3011
Date and Time: May 27, 2009 10:00am
Committee:
Chancellor’s Professor Nikil Dutt (Chair)
Professor Tony Givargis
Professor Ian Harris
Abstract:
As embedded systems become increasingly networked, and interact with the physical world, Distributed Real-time Embedded (DRE) systems emerge. DRE systems range from small-scale Multi-processor Systems-on-Chip (MPSoCs) operating in resource constrained environments such as cell phone platforms, medical devices and sensor networks all the way to large-scale software-intensive systems of systems used in avionics, ship computing environments, and in supervisory control and data acquisition systems managing regional power grids.
This dissertation focuses on the model-based analysis of event-driven DRE systems. Event-driven DRE systems are based on a reactive communication paradigm, where the execution of tasks is triggered asynchronously, invoked by external events, interrupts, or by other tasks. Events can also express time, providing a common semantic domain for the compositional analysis of time- and event-driven DRE systems.
The key technical contributions of this dissertation are (1) the specification of a formal semantic domain for DRE systems, (2) a model checking method for the real-time verification of non-preemptive DRE systems using timed automata, (3) a performance estimation method for DRE systems by discrete event simulations, (4) a conservative approximation method for the verification of preemptive event-driven asynchronous DRE systems by timed automata, (5) a method for the functional verification and performance estimation of MPSoCs built on an industry standard interconnect, and (6) a cross-abstraction real-time analysis method for MPSoC designs utilizing bus matrix interconnects.
The novelty of our approach lies in combining formal methods and symbolic simulations for the system-level evaluation of DRE designs early in the design flow, and utilizing multiple abstractions to trade off analysis accuracy in scalability.
We implemented the proposed analysis methods in the open-source Distributed Real-time Embedded Analysis Method (DREAM) framework for the model-based real-time verification and performance estimation of DRE systems. DREAM focuses on the practical application of formal analysis methods to automate the verification, development, configuration, and integration of event-driven DRE systems. DREAM is available for download at http://dre.sourceforge.net. We applied the proposed design flow to the domain of software-intensive mission-critical avionics DRE applications, and the domain of multimedia MPSoCs.