EPIC has moved! The content of this site has been frozen and placed in a Read-Only State. Check out our new Eclipse Marketplace site. Logins to this site have been disabled.
Category: Plugin Directory / IDE / JTLV - Unified Formal Verification Framework.
| | | |
Version: 1.2.1
Support Eclipse Version: 3.3.2
License: Free LGPL
Development Status: Beta
Company:
| |  | Home Page |  | Plugin Support |  | Discussion Forum | |
|
Currently, all existing formal verification tools are designed to serve as formal verifiers, using one implementation or the other.
In order to introduce and implement even the simplest new formal algorithm, the developer has to be completely aware of the entire system she or he is implementing her or his algorithm upon. As if that wasn't enough, from the nature of the formal field, most systems are implemented in a very low level C code. This is since the complexity of such algorithms in exponential to begin with.
Now, let's see you try to implement a new formal algorithm.
JTLV is a new tool aimed to facilitate and provide a unified framework for developing formal verification algorithms in a high level programming environment.
JTLV provides a pure Java user API, while the exponential complexity derived from using BDDs, is actually implemented in C, and is accessed through a JNI interface to the C libraries (e.g. all the underlying BDD implementation is invisible to the user). There are many BDD libraries to pick from, and the BDD package used, can be set dynamically during runtime. The whole BDD interface is all thanks to the JavaBDD Project.
Using the chosen BDD library, JTLV continues to construct Design Modules. Currently, the design modules can be specified using, SMV, or FDS formats (FDS is a simpler format for specifying Finite State Machines, which was implemented first in order to prove the feasibility of this project). Both parsers were written using ANTLR v3. The SMV parser is also connected to the editor, which enables it to use the nice facilities that eclipse can offer (still lots more to come in this area).
From the other hand, algorithm designers can load Specification file (SPC). JTLV support almost all known temporal specification format. The SPC parser is also connected to eclipse as editor, again giving it the nice facilities that eclipse can offer.
AND THUS, it all sums up to be a Java environment,
* Which allows the user to construct his algorithm in Java/Eclipse.
* Using the API given to load and address the specification.
* Using the API given to load and address the design modules and its BDDs.
* Without taking an inch out of performance.
Now, That's the way I want to implement my next formal algorithm.
Added on: 03-Nov-2008
|
|
