Timed Systems Verification Tool (Tivet)
---------------------***---------------------
Author: Hoang-Viet Tran and Pham Ngoc Hung, VNU University of Engineering and Technology.Email:
15028003 "at" vnu "dot" edu "dot" vn
hungpn "at" vnu "dot" edu "dot" vn
---------------------------------------------------------------------------------------------------------
USER MANUAL
---------------------------------------------------------------------------------------------------------
#Required environment:
Our implementation has been tested on the Windows 10 Enterprise, 64 bit.
This tool is developed by C#.NET, .NET Framework 4.6.1 on Visual Studio 2019, the community edition.
#Overview
This is the user manual for the tool Tivet version 1.0.0.
You can download the installation file here.
For any information related to the source code or test data, please contact the author.
#Input of this tool
This tool implemented the two assumption generation methods
+ The first one uses the two-phases assumption generation algorithm.
+ The second one uses our one-phase assumption generation algorithm.
+ Both assumption generation methods use the same candidate and membership queries answering algorithms in Teacher. Candidate queries answering algorithm is implemented with the enhancement where counterexample that was already returned to Learner will not be returned the second time.
- Sample input file can be downloaded here for its format reference.
#Install this tool
Simply download and run the installer here and follow the instruction of the installation wizard.
Note: The installer already contains the test data used in our research. You can use it as initial sample to run the tool.
#Using this tool
The main screen
After installation, run the Tivet tool, the main screen looks like this:
In order to generate assumption, please choose a file with the same format as the sample file given above for the "Input" and the output file.
If you want to generate assumption using two-phases assumption learning algorithm, please click on "Two phases learn" button.
If you want to generate assumption using one-phase assumption learning algorithm, please click on "One phase learn" button.
Don't know maxbound field represents the maximum number of candidate query that Teacher processes before answering "Don't know" to Learner.
After finish processing, you can open the output file for result.
End.