ModelCheck.h

Go to the documentation of this file.

/** @file ModelCheck.h
* @author Gabor Madl
* @date Created 08/2005
* @brief Model Checker library.
*
*
* =================================================================
* DREAM License v2.0
* 
* DREAM - Distributed Real-time Embedded Analysis Method
* http://dre.sourceforge.net.
* Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.
* 
* This file is part of DREAM.
* 
* 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.
* =================================================================
*/

#ifndef DREAM_MODELCHECK
#define DREAM_MODELCHECK

#include "../algorithm/GeneticAlgorithm.h"

namespace DREAM
{

/** Model check class.
* Provides methods to verify System designs.
*/
class ModelCheck
{
public:
        /** Constructor */
        ModelCheck (DREAM::System* system_ptr);

        /** Destructor */
        ~ModelCheck () {};

        /** Random-tests the system. Do not underestimate this method!
        * @return true if the system is schedulable
        * @param system_ptr is the pointer to the System.
        * @param verbose specifies whether output will be generated or not.
        */
        bool random_testing (DREAM::System* system_ptr, bool verbose)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
                throw (DREAM::Exception)
#endif
        ;

        /** Simple proof-of-concept simulation-based model checker. Model checks a distributed non-preemptive real-time system.
        * @return true if the system is schedulable
        * @param system_ptr is the pointer to the System.
        * @param verbose specifies whether output will be generated or not.
        */
        bool trace_based_model_check (DREAM::System* system_ptr, bool verbose)
                throw (DREAM::Exception);

private:

        /** Used to generate cartesian cross-product of branching points.
        * @param node_avltree contains the Tasks to be manipulated.
        * @param verbose specifies whether output will be generated.
        */
        bool branching_point (DREAM::NODE_AVLTREE* node_avltree, bool verbose);

        /** Pointer to the system */
        DREAM::System* system_ptr_;

        /** Stores the worst case end-to-end execution time encountered during the analysis. */
        double endtoend_;
};

};

#endif

---