There are many verification tools for formal verification, both commercial and in

academia, however not every tool is appropriate for every verification task. Often,

an available tool is not appropriate for checking some property that a user of the

tool wants to check on some source program. One of the possible solutions to this

problem is to translate both the source program and the property to another notation

used by a different verification tool, that is capable of checking the property.

VeriTech is a general framework for translating among notations of formal

verification tools. The key element of the framework is the core design language

CDL. Each notation has a translation to and from CDL, thus requiring only 2*N

for each available notation A and allows a user to translate a source program written

using a given notation S to a target program in any other notation T treated by

VeriTech.

In this work we present the extension of the VeriTech whose purpose is to solve

two main problems with the previous implementation: inability to save additional

information during translations and inability to advice a user on a best choice for a

target notation.

The first problem is solved by adding a few XML-based components to the

VeriTech framework. By utilizing the power of XML, not only have we unified the

format of a source and target programs in a translation, but also used a variation of

the same XML format to save additional information gathered during translations.

The XML approach provided developers of new translations with many existing

tools that allow creating compilers in almost any language on almost any platform.

In order to provide a user with an advice on which notations are best suited

to be translated to, an expert system was designed and built. The expert system

was built using the Bayesian Network approach. In order to collect the information

about different tools a survey was conducted. Based on responses from creators of

the tools, the Bayesian Network was created and it became the basis of the expert

system.

For system download and set-up, please, click here.