What is VeriTech ?

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.

  To the top of page

Articles

• Read a (somewhat outdated) detailed paper about VeriTech.
• Read a popular paper about VeriTech (Hebrew).
• An article entitled "Faithful Translations among Models and Specifications in VeriTech", by Orna Grumberg and Shmuel Katz, describes the VeriTech core design language (CDL), issues that arise in translation, and a framework for expressing which properties are affected by translations of a model.
• An article entitled "Faithful Translations among Models and Specifications" by Shmuel Katz expands on the need to transform properties along with any translations of models, independent of VeriTech. This paper appears in the proceedings of FME2001 (March 2001, Berlin).
• A paper describing the translations and the additional information gathered for the core-to-Petri-net and the Petri-net-to-core translations, is Katarina Korenblat, Orna Grumberg, and Shmuel Katz, Translations Between Textual transition Systems and Petri Nets,  in the Proceedings of the Integrated Formal Methods Conference (IFM2002) in Turku, Finland, May, 2002.
• An overview of VeriTech and the translation issues it tries to treat is given in: Shmuel Katz and Orna Grumberg, A Framework for Translating Models and Specifications,  in the Proceedings of the Integrated Formal Methods Conference (IFM2002) in Turku, Finland, May, 2002.
  (Look also at the slide show presented at the conference ppt or pdf)

   To the top of page

The Core Language

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 core language.
• Core parser user guide.
• Core parser components.
• Core parser error checks.
• Core parser programmer guide.
• Core parser make file.

   To the top of page

Tools (translations)

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.

Current status

(which translations exist)

about the text in the table

Core to Lotos (XML, Linux, ver 0.9)

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.

• About the translation
• partial synchronization
• User Guide
• programmer guide
• To do list (Hebrew)

Core to Murphi (XML, Linux, ver 3.0)

• project documentation

• project documentation
• A paper describing the translations and the additional information gathered for the core-to-Petri-net and the Petri-net-to-core translations, is Katarina Korenblat, Orna Grumberg, and Shmuel Katz, Translations Between Textual transition Systems and Petri Nets,  in the Proceedings of the Integrated Formal Methods Conference (IFM2002) in Turku, Finland, May, 2002.

Core to SAL (XML, Unix, ver 1.0)

• About the translation
• A slide show that presents the translation principles
• User Guide
• Additional information gathered by the translation.
• Programmer Guide
• To do list

Core to SMV (XML, Linux, ver 2.0)

Basically the translation works. We are currently working to optimize the SMV code created.

• project documentation
• User guide

Core to Spin (Text, Linux, ver 1.1)

In the Linux version, some examples do not give the expected result.

• About the translation
• User guide
• Programmer Guide

Core to STeP (Text, Linux, ver 1.2)

• A slide show that presents the translation principles (ppt)
• Read more notes about the translation.
• User guide.

Petri Net to core (Text, Unix, ver 0.9)

When running the translation on a Linux machine we experience some memory allocation problems. We are working to solve this out.

• project documentation of the first draft
• project documentation of the second draft
• slide show of the project

Sal to core (Text, Linux, ver 0.9)

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.

• user guide
• advanced user guide (contain the translation algorithm)
• programmer guide

SMV to core

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.

• About the translation (Hebrew)
• About the XML (improved) version
• Translating arguments (Hebrew)
• Bugs and un-handled issues (Hebrew)
• Class diagram (Hebrew)

Spin to core

• user guide
• programmer guide
• design documents
  • class tree
  • atomic vs. d-step
  • design
  • translation design

STeP to core

• user guide
• programmer guide
• changes to the original Stanford Step parser
• project documentation
• examples slide show
• project slide show

   To the top of page

XML

If you want to learn about XML, you can:

• look for the XML tutorials at the W3 School site.
• look at the Altova web site (Altova is the creator of XmlSpy)
• use Google to search for XML

Additional information

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.

DTD

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.

Additional info.

Core design language (CDL)

Lotos

Murphi

SAL

SMV

XSL

additional info.

core

smv

XML Viewer

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.

XML Viewer help

Get the application (to install, just un-zip)

   To the top of page

Useful links

• CWB at Edinburgh - The Edinburgh Concurrency Workbench.

• LOTOS (the language) and CADP - the protocol engineering toolbox of VASY at INRIA and the Verimag laboratory.

• Mocha - a vehicle for development of new verification algorithms and approaches

• Murphi - the state exploration invariant checker of Stanford.

• Petri-net.

  • Visit the World of Petri Nets.

  • Look into Wil Van Der Aalst's course about workflow to see usage of Petri Nets.

• PVS - the theorem prover of SRI.

• SAL - Symbolic Analysis Laboratory - SRI

• SMV - the temporal logic model checker of CMU.

• SPIN - the protocol verifier of Bell Labs.

• STeP - the temporal logic program verifier of Stanford.

   To the top of page

Contact us

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: ssdlhelp@cs.technion.ac.il

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: ssdlhelp@cs.technion.ac.il

1. Use of VeriTech software is only allowed for academic research. Any other usage requires specific permission.
2. The software is supplied “as is”. We do not guarantee that it is bug free or works at all. We are not be responsible for any damages caused to you by VeriTech software.
3. In any publication that relies (even partly) on the VeriTech project, you must give appropriate credit to the project.
4. You agree to provide us with feedback about the project:
   1. How was the software used?
   2. What bugs were found?
   3. How would you suggest to improve the VeriTech project?
5. If you would like to get the source code of the program you must:
   1. Fulfill all the software usage terms above.
   2. Describe the project that you are working on and which needs VeriTech source code
   3. Promise to supply us with your code if we ask for it.
   4. To alter our code or to re-use part of it you must:
      1. Get specific permission from us.
      2. Give appropriate credit.
      3. Give us permission to use the altered code.

   To the top of page