טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentEstrin Yacov
SubjectExpert System On Translations among Formal Verification
Tools in VeriTech
DepartmentDepartment of Computer Science
Supervisor Professor Shmuel Katz


Abstract

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 2n translations in order to achieve all of the n2/2 relations among n different notations.

The completed framework contains both A -> CDL and CDL -> A translations 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.