DREAM

Distributed Real-time Embedded Analysis Method - DREAM

Open-source formal verification and analysis

Downloads

Changelog

DREAM 0.7 beta

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. 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, and KCacheGrind, and managed to achieve impressive performance gains (around 2-3x at least) compared to previous DREAM releases.

FYI: the Linux version of DREAM 0.7 Beta is faster than the Win XP MSVC 2005 version on my laptop (by around 30-50%). If I'm not mistaken this hasn't been the case before. GCC is clearly improving...

Balanced AVL trees are now used to store branching points and race conditions at run-time, resulting in exponential speedups in several steps of the model checking method. Implemented XML Schema validation. Upgraded verification time reporting to include some meaningful data on the simulation speeds. Random simulation-based testing now provides an execution trace when a deadline is missed. Added performance estimation capability. Updated Uppaal interpreter to use the new Uppaal 4 syntax.

Moved source code from CVS to Subversion on Sourceforge. To simplify development efforts, only VC7.1, VC8.0 and GNU make/gcc build processes are supported in DREAM from now on. Added Visual Studio project files for the libxml2 library under Win32.

DREAM 0.6 beta

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

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.

DREAM 0.4 pre-alpha

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

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

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 as well.

DREAM 0.1 pre-alpha

DREAM 0.1 pre-alpha includes 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 License v2.0


DREAM - Distributed Real-time Embedded Analysis Method
http://dre.sourceforge.net.
Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.


DREAM is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License version 2 as published by the Free Software Foundation. No future versions of the GPL license may be automatically applied to DREAM. It is in the sole discretion of the copyright holder to determine whether DREAM may be released under a different license or terms. There are no restrictions on the use of DREAM for any purpose.


DREAM is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.


You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.


By submitting comments, suggestions, code, code snippets, techniques (including that of usage), and algorithms, submitters acknowledge that they have the right to do so, that any such submissions are given freely and unreservedly, and that they waive any claims to copyright or ownership. In addition, submitters acknowledge that any such submission might become part of the copyright maintained on the overall body of code, which comprises DREAM. By making a submission, submitter agrees to these terms. Furthermore, submitters acknowledge that the incorporation or modification of such submissions is entirely at the discretion of the moderators of the DREAM project.


DREAM links to the Libxml2 third party library. Please see COPYING-libxml for the copyright information of Libxml2.