The Distributed Real-time Embedded Analysis Method (DREAM) is a tool and method for the real-time verification and performance estimation of distributed real-time embedded (DRE) systems. It focuses on the practical application of formal verification and timing analysis to real-time middleware.
ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.
JCCad is a project to develop a 2D/3D CAD program that can be used to create technical drawings. One of the main goals of this project is to include a plugin system to allow usuaries to make new commands. In this way it will be easy to use the program for any particular task. JCCad provides an easy interface with a command line.
PEP is a modeling and verification framework for parallel systems. It provides a large number of different modelling languages (e.g. SDL, B(PN)^2, Petri nets, Process algebras and Finite Automata), and verification techniques (e.g. reachability and temporal logic model checking). Due to its Tcl/Tk-based GUI, PEP is easily extensible to other analysis or specification tools. The framework offers fully integrated simulation and debugging features on all levels.
Platform Independent Petri Net Editor (PIPE) creates and analyses Petri Nets quickly, efficiently, and effectively. A key design feature is the modular approach adopted for analysis, enabling new modules to be written easily and powerfully, using built-in data layer methods for standard calculations. Six analysis modules are provided, including Invariant Analysis, State-Space Analysis (deadlock, etc.), and Simulation Analysis and Classification. PIPE adheres to the XML Petri net standard (PNML). The file format for saving and loading Petri Nets is extensible through the use of XSLT, the default being PNML.