DREAM / News: Recent posts

DREAM 0.7 Beta is a major jump from previous releases. The main discrete event simulation-based model checking is not only more stable, but also faster in this release. DREAM 0.7 Beta was checked for memory leaks using Valgrind (http://valgrind.org). Several memory leaks were traced down and fixed. There are no known memory leaks present in the current release.

DREAM 0.7 Beta Linux release now implements several optimizations for improved model checking performance. We profiled DREAM using Callgrind (http://valgrind.org/info/tools.html), and KCacheGrind (http://kcachegrind.sourceforge.net), and managed to achieve impressive performance gains (around 2-3x at least) compared to previous DREAM releases.... read more

Vastly improved simulation-based verification engine. 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.

DREAM 0.5 alpha has been integrated with the Verimag IF toolset. A random testing facility has also been added to DREAM. Some bugfixes and optimizations have been implemented in the UPPAAL interpreter.

The simulator engine in DREAM 0.4 pre-alpha has been extended to handle non-deterministic execution times in continuous time and non-deterministic thread-level scheduling. The random function has been reimplemented using a more efficient algorithm. DREAM now supports the libxml XML parser. XML parser regression tests have been added.

DREAM 0.3 pre-alpha simplifies the timed automata models used for the verification of preemptive scheduling. The package now supports automake, KDevelop and the Eclipse framework.

DREAM 0.2 pre-alpha utilizes efficient genetic algorithms to optimize the fixed-priority non-preemptive scheduling of distributed real-time embedded systems. The package includes a simple proof-of-concept simulation-based model checker, a discrete event simulator, a validating XML parser and a UPPAAL interpreter to provide a way for the formal verification of DRE systems based on the timed automata formalism.

DREAM 0.1 pre-alpha has been released! It includes a discrete event simulator, a validating XML parser and a UPPAAL interpreter which provides a way for the formal verification of DRE systems.