The Distributed Real-time Embedded Analysis Method (DREAM) is a tool and method for the real-time verification and performance estimation of distributed real-time embedded (DRE) systems. It focuses on the practical application of formal verification and timing analysis to real-time middleware.
|Tags||education Scientific/Engineering Electronic Design Automation (EDA) Mathematics Software Development Testing|
|Operating Systems||OS Independent|
Release Notes: This version implemented several optimizations for improved model checking performance, resulting in impressive performance gains of at least 2-3 times. There are no known memory leaks present in the current release. Balanced AVL trees are now used, resulting in exponential speedups in several steps of the model checking method. XML Schema validation was implemented. Verification time reporting was upgraded to include data on the simulation speeds. Random simulation-based testing now provides an execution trace when a deadline is missed.
Release Notes: The simulation-based verification engine was vastly improved. DREAM now implements a dynamic analysis that takes all events (branching points), race conditions, and race condition combinations into consideration. Two larger case studies are now included in the examples.
Release Notes: This release implements a discrete event simulator, a random tester facility, a validating XML parser, and interpreters to model checkers based on the timed automata formalism. It supports several build environments, including automake, Visual Studio 6.0 and 7.1, KDevelop, and the Eclipse framework.