by farn_red
* Model-checking/simulation-checking library for real-time system with dense-time models in C with CRD (Clock-Restriction Diagrams) technology. * Parametric analysis library for linear-hybrid systems in C with HRD (Hybrid-Restriction Diagram) technology.
================================= Notes on Thursday 08 May 2009: This version is temporary and does not work for model-checking. It works for reachability and safety analysis. Some bugs thas have been removed affect the correctness of the following ...
================================= Notes on Thursday 08 May 2009: This version is temporary and does not work for model-checking. It works for reachability and safety analysis. Some bugs thas have been removed affect the correctness of the following ...
===================================== Note on 11 March 2009: We have fixed a bug in REDLIB that affects the postcondition calculation when we try to use the destinaiton invariance of a process transition to prune the intermediate space ...
===================================== Notes on Friday 09 April 2009: We have added a new procedure, red_query_process_role(), to allow the users to query the roles of processes. ===================================== Notes on Sunday 15 March 2009: ...
A new version of reference manual has been uploaded that describes how to access the game synchronous transition tables used in simulation checking and bisimulation checking.
We have implemented a new version of REDLIB. The new version supports an integrated software architecture for the evalaution of time-progress preconditions with various techniques.
We are glad to announce that now a reference manual for REDLIB in PDF is now available in this sourceforge webpage. The reference manual explains many of the procedures for basic space manipulations, model-checking, and simulation-checking. Some ...
Copyright © 2009 SourceForge, Inc. All rights reserved. Terms of Use
