- DREAM is a project candidate (#5) for the Ptolemy II project at UC Berkeley as part of the Google Summer of Code for 2009! We thank Prof. Edward A. Lee and his team for the nomination.
- DREAM has been recently integrated in the Scenery project by Fujitsu Laboratories of America to analyze real-time properties in embedded software and MPSoCs.
- Download the most recent version of DREAM!
- The DREAM source has been moved to the Subversion version control system on Sourceforge. Browse it online now!
What is DREAM?
The Distributed Real-time Embedded Analysis Method (DREAM) project focuses on the practical application of formal analysis methods to automate the verification, development, configuration, and integration of asynchronous event-driven distributed real-time embedded (DRE) systems, that was applied to the domain of software-intensive mission-critical avionics DRE applications, and the domain of multimedia MPSoCs. In its current form, the open-source DREAM tool is a prototype implementation of three real-time analysis methods:
- A model checking method for the real-time verification of non-preemptive DRE systems by timed automata, utilizing the UPPAAL or Verimag IF model checkers.
- A performance estimation method for DRE systems by discrete event simulations, implemented within DREAM itself.
- A conservative approximation method for the verification of preemptive event-driven asynchronous DRE systems by timed automata. This approach also utilizes the UPPAAL or Verimag IF model checkers.
For the theoretical background on DREAM, please see Gabor's Ph.D. dissertation and final defense presentation:
- Gabor Madl: Model-based Analysis of Event-driven Distributed Real-time Embedded Systems, Ph.D. Dissertation, University of California, Irvine, June 2009.
- Gabor Madl: Model-based Analysis of Event-driven Distributed Real-time Embedded Systems, Final Defense Presentation, University of California, Irvine, May 2009.