ModelCheck.h

Go to the documentation of this file.
00001 /** @file ModelCheck.h
00002 * @author Gabor Madl
00003 * @date Created 08/2005
00004 * @brief Model Checker library.
00005 *
00006 *
00007 * =================================================================
00008 * DREAM License v2.0
00009 * 
00010 * DREAM - Distributed Real-time Embedded Analysis Method
00011 * http://dre.sourceforge.net.
00012 * Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.
00013 * 
00014 * This file is part of DREAM.
00015 * 
00016 * DREAM is free software; you can redistribute it and/or modify it
00017 * under the terms of the GNU General Public License version 2 as
00018 * published by the Free Software Foundation. No future versions of
00019 * the GPL license may be automatically applied to DREAM. It is in
00020 * the sole discretion of the copyright holder to determine whether
00021 * DREAM may be released under a different license or terms. There
00022 * are no restrictions on the use of DREAM for any purpose.
00023 * 
00024 * DREAM is distributed in the hope that it will be useful,
00025 * but WITHOUT ANY WARRANTY; without even the implied warranty of
00026 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
00027 * GNU General Public License for more details.
00028 * 
00029 * You should have received a copy of the GNU General Public License
00030 * along with this program; if not, write to the Free Software
00031 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
00032 * MA 02110-1301, USA.
00033 * 
00034 * By submitting comments, suggestions, code, code snippets,
00035 * techniques (including that of usage), and algorithms, submitters
00036 * acknowledge that they have the right to do so, that any such
00037 * submissions are given freely and unreservedly, and that they
00038 * waive any claims to copyright or ownership. In addition,
00039 * submitters acknowledge that any such submission might become
00040 * part of the copyright maintained on the overall body of code,
00041 * which comprises DREAM. By making a submission, submitter agrees
00042 * to these terms. Furthermore, submitters acknowledge that the
00043 * incorporation or modification of such submissions is entirely
00044 * at the discretion of the moderators of the DREAM project.
00045 * 
00046 * DREAM links to the Libxml2 third party library. Please see 
00047 * COPYING-libxml for the copyright information of Libxml2.
00048 * =================================================================
00049 */
00050 
00051 #ifndef DREAM_MODELCHECK
00052 #define DREAM_MODELCHECK
00053 
00054 #include "../algorithm/GeneticAlgorithm.h"
00055 
00056 namespace DREAM
00057 {
00058 
00059 /** Model check class.
00060 * Provides methods to verify System designs.
00061 */
00062 class ModelCheck
00063 {
00064 public:
00065         /** Constructor */
00066         ModelCheck (DREAM::System* system_ptr);
00067 
00068         /** Destructor */
00069         ~ModelCheck () {};
00070 
00071         /** Random-tests the system. Do not underestimate this method!
00072         * @return true if the system is schedulable
00073         * @param system_ptr is the pointer to the System.
00074         * @param verbose specifies whether output will be generated or not.
00075         */
00076         bool random_testing (DREAM::System* system_ptr, bool verbose)
00077 #ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
00078                 throw (DREAM::Exception)
00079 #endif
00080         ;
00081 
00082         /** Simple proof-of-concept simulation-based model checker. Model checks a distributed non-preemptive real-time system.
00083         * @return true if the system is schedulable
00084         * @param system_ptr is the pointer to the System.
00085         * @param verbose specifies whether output will be generated or not.
00086         */
00087         bool trace_based_model_check (DREAM::System* system_ptr, bool verbose)
00088                 throw (DREAM::Exception);
00089 
00090 private:
00091 
00092         /** Used to generate cartesian cross-product of branching points.
00093         * @param node_avltree contains the Tasks to be manipulated.
00094         * @param verbose specifies whether output will be generated.
00095         */
00096         bool branching_point (DREAM::NODE_AVLTREE* node_avltree, bool verbose);
00097 
00098         /** Pointer to the system */
00099         DREAM::System* system_ptr_;
00100 
00101         /** Stores the worst case end-to-end execution time encountered during the analysis. */
00102         double endtoend_;
00103 };
00104 
00105 };
00106 
00107 #endif
00108 

Generated on Fri Jul 27 18:30:03 2007 for DREAM by  doxygen 1.5.1