VeriTech is a lab project for Formal Verification at the System and Software Development Laboratory (SSDL) in the Computer Science Department at the Technion. VeriTech aims at integrating several well known Formal Verification tools, by translating to and from their model notation.
The goal of VeriTech is the development of an interactive extensible tool for translations to facilitate formal verification of hardware and software. The project integrates a variety of existing verification and specification tools that have very different notations, proof methods, and verification capabilities. VeriTech is based on translating from each component verification tool to a core representation and from the core to each tool, thereby allowing automatic transformations among the systems. This encourages using different verification tools for various aspects of the same specification and implementation.
New verification capabilities, especially those involving abstraction and partial orders, can be added as transformations to the core representation of VeriTech . In this way these capabilities become available to all of the component methods, by using the translations to and from the core representation. The tool represents a significant advance in capabilities for formal verification of complex systems.
VeriTech has a simple Core Description language (CDL) based on sets of labeled textual transitions and compositions of modules. Among the translations to and from CDL are those for SMV, Spin, Petri nets, STeP, SAL, and translation in one direction for LOTOS and Murphi. Most of the translations have been tested for a benchmark of typical problems, available from the Examples page. Individual compilers with specific translations can be obtained by writing to the Contact email in the top-level menu.
See a slide show overview of VeriTech.
The translation from one specification language (source) to another specification language (destination) is not direct. Instead we translate from the source specification language to the core design language (CDL) and then we translate from the core language to the destination specification language. This way, if we have N specification languages, we can translate between any two languages using only 2*N translations ( instead of N*(N-1) in the direct translation method).
To make translations from CDL to another language easier we created the Core Parser, a parser for the core language. All our translations from the core are based on this parser.
Read the following documents to learn more about the core design language (CDL), the core parser and all related tools:
The older translations translate directly between the textual forms of the languages. If the languages do not match completely (for example: the source language has a special construct for loops while the destination doesn't) then in the translation this information is lost and the only sign for it is the log file (which is just a plain text file). In the new translations we first translate the source language to an XML format, translate it to an XML version of the destination language and only then create a textual version in the destination language, This way we can keep the lost relationship between the source syntactic building blocks and the result in the destination and use this information when translating back (for detailed information see the XML chapter).
The VeriTech project is now moving from the UNIX environment to the LINUX environment. We are transferring the latest versions (mostl XML translation) from UNIX to LINUX. We will not transfer the oldest (mostly textual) translation to LINUX.
(which translations exist)
about the text in the table
The translation is finished but the results are not 100% tested and the project tree + documentation must be upgraded for the the level needed from a release version.Core to Petri Net (Text, Linux, ver 1.0)
Basically the translation works. We are currently working to optimize the SMV code created.
In the Linux version, some examples do not give the expected result.
When running the translation on a Linux machine we experience some memory allocation problems. We are working to solve this out.
This translation was designed as an XML translation, but we didn't implemented the additional info part yet, so it is classified as textual translation.
The translation include function calls to generate the additional info. To get an XML translation: this functions must be implemented and the parsed input SMV program must be translated to XML format.
If you want to learn about XML, you can:
Why do we use XML at the first place? Read this popular document to get the main idea.
More formal document that describe the additional information gathered during the translation.
The dtd files can't be displayed inside the browser. To examine the dtd file save it on your local disk and use your favorite tools to open it.
Core design language (CDL)
The Xml Viewer is a tool written as part of the VeriTech project. The Xml Viewer display the source & destination languages (xml & textual format) and show the links between expressions in the source and destination languages.
Get the application (to install, just un-zip)
If you need more information regarding the VeriTech project, if you would like to join the VeriTech project or if you have any questions or comments: Please send an e-mail to: email@example.com
If you would like to get any of the VeriTech applications or if you would like to get the source of a specific translation, please copy the following section, provide the missing information and e-mail it to: firstname.lastname@example.org
Status (e.g., researcher, PhD student, etc):____________________________
Affiliation (Academic Institution or Company):_____________________________
Requested material: ________________________ (please specify what you would like to download from the VeriTech project)
The submission of this form implies agreement with the following terms:
|You are visitor number:|