News
- DREAM has been recently integrated in the Scenery project by Fujitsu Laboratories of America to analyze real-time properties in embedded software and MPSoCs. We are working on publishing early results of this collaboration in the close future.
- We are looking for sponsors to integrate the open-source DREAM tool with the SAE AADL standard. Please contact us if you are interested.
- We have just released a new version of DREAM, that implements several major improvements. Download it now!
- Please see our recent publication on the theory behind the DREAM model checker engine, and a journal paper for a description on how DREAM utilizes third-party timed automata model checkers for real-time analysis.
- The DREAM source has been moved to the Subversion version control system on Sourceforge. Browse it online now!
Introduction
Key challenges in the design, development and analysis of distributed real-time embedded (DRE) systems include safe composition of system components, formal analysis of real-time properties, the systematic measurement of coverage by simulations, and the automated generation of directed test vectors. Model-based technologies help address these issues by enabling design-time analysis and providing the means for the rapid evaluation of design alternatives with respect to end-to-end QoS properties, predictability and performance measures before committing to a specific platform. The Distributed Real-time Embedded Analysis Method (DREAM) is an open-source tool and method for the real-time verification and performance estimation of DRE systems. The project focuses on the practical application of formal analysis methods to real-time middleware to automate the verification, development, configuration, and integration of middleware-based DRE systems.
Proposed method
DREAM proposes a discrete event simulation-based formal verification and performance evaluation method for DRE systems, that employ fixed-priority scheduling. DREAM utilizes a formal, executable C++ model for real-time analysis based on discrete event scheduling, and third-party timed automata model checkers, allowing to bridge the gap between simulations and formal verification. The proposed model explicitly captures the flow of data and communication effects (such as non-deterministic delays etc.) in event-driven systems for dynamic performance evaluation. DREAM does not store timed states, like timed automata model checking methods, just events and constraints on the (global) timestamps of real-valued events. Note that this approach represents real-time properties in continuous time. Storing timed states is the most significant contributor to memory consumption in model checking tools. The proposed method has minimal memory requirements, providing a way for runtime on-the-fly analysis in adaptable DRE systems. Our preliminary results show that the proposed DES-based evaluation method can achieve better coverage in large-scale DRE systems than alternative methods.