VeriTech  Project
  About     Articles     The Core Language     Tools     XML     Links     People     Examples     Contact  
 

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

   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:

   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)

Language from CDL to CDL

Lotos

core 2 lotos

XML, Linux, ver 0.9

Murphi

core 2 murphi

XML, Linux, ver 3.0

 

PetriNet

core 2 petri

Text, Linux, ver 1.0

petri 2 core

Text, Unix, ver 0.9

SAL

core 2 sal

XML, Unix, ver 1.0

sal 2 core

Text, Linux, ver 0.9

SMV

core 2 smv

XML, Linux, ver 2.0

SMV 2 core

Text, Linux, ver 1.1

Spin

core 2 spin

Text, Linux, ver 1.1

spin 2 core

Text, Linux, ver 1.3

STeP

core 2 step

Text, Linux, ver 1.2

step 2 core

XML, Unix, ver 0.9

about the text in the table

XML

The translation generates "additional info" file to connect between items in the input & output files.

(if the input file is in non XML format it will be translated to XML, the output file will be in XML format.)

Text

The translation do not generate "additional info" file.

Linux

The translation is compiled under the Linux operating system.

(the examples may be generated on Unix)

Unix

The translation was compiled under the Unix operating system, and transferring to Linux needs some adjustments.

ver

This is the latest version of the software.

Version below 1 means that the translation is not finished.

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.

Core to Murphi (XML, Linux, ver 3.0)

Core to Petri Net (Text, Linux, ver 1.0)

Core to SAL (XML, Unix, ver 1.0)

Core to SMV (XML, Linux, ver 2.0)

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

Core to Spin (Text, Linux, ver 1.1)

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

Core to STeP (Text, Linux, ver 1.2)

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.

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.

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.

Spin to core

STeP to core

   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.

  • 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

 

People

 

VeriTech group members
Students
Past Workers

      Students

  • Anastasia Braginsky

  • Ayelet Bar-Nir

  • Bracha Greenberg
  • Dikla Yanay
  • Efrat Dagagi
  • Efrat Shabtai
  • Eli Cohen
  • Eran Shany
  • Eyal Sonsino
  • Gilad Hemi
  • Guy Wiener
  • Kobi Toueg
  • Konstantin Radchenko
  • Magid Avi
  • Marcelo Glusman (Phd)
  • Mirit Berg (Msc)
  • Roman Tzarney
  • Roni Baram
  • Royi Ronnen
  • Shlomit Ozer
  • Tamim Nassar
  • Yoav Gur
   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

Name: ______________________________________________________
Status (e.g., researcher, PhD student, etc):____________________________
Affiliation (Academic Institution or Company):_____________________________
Email:_______________________________________
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: 
  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

 

  About     Articles     The Core Language     Tools     XML     Links     People     Examples     Contact  
 

 

You are visitor number: