♦ Tevfik Bultan, email: bultan AT cs.ucsb.edu
♦ Zachary Stengel, email: zss AT cs.ucsb.edu
Tune is a tool for analyzing and verifying Singularity channel contracts. Tune offers the following features:
♦ Convert Singularity channel contracts written in Sing # into the following alternative representations:
o Asynchronous Promela model
o Synchonous Promela model
o WSAT Model
o Dot Model
o Realizability Analysis with Models of Belief (RAMOB) Model
♦ Realizability analysis / deadlock detection in Singularity contract protocols
♦ LTL Property validation
Tune implements the realizability analys described in [ISSTA'09]. It also utilizes the Spin model checker and the WSAT protocol analysis tool to perform portions of its analysis.
Tune's minimum requirement for basic functionality is the .NET v2.0 framework. To support all target models and analyses, the following applications must be installed and accessible via the PATH environment variable:
♦ The WSAT protocol analysis tool
♦ Dot
♦ The Microsoft C++ compiler (cl.exe)
To compile Tune's sources, the only requirement is C# compiler. csc.exe is included with Microsoft Visual Studio and was used to compile Tune's binaries (download available below); however, any standards compliant C# compiler should work.
Tune's basic usage is described below:
---------------------------------------------------------------------------------------------
Tune v0.0.0.2
Copyright (c) UCSB 2009
---------------------------------------------------------------------------------------------
Usage: tune.exe [options]
::
:: Translation Options
::
/cs:ChannelSize :: The size of the Promela channel. Only used if /t is set to 'Spin'.
/i:path :: The Singularity source file (or directory) to translate.
/t:TranslationTarget :: The translation target. [Spin, Wsat, Dot, RAMOB]
::
:: General Options
::
/Check:path :: Runs Spin against the specified Promela model.
/Debug :: Enables debug mode.
/f:Formula :: Translates the specified LTL formula into Promela never claims for Tune
:: and WSAT generated models.
/? :: Displays the help.
/o:path :: The directory where translation output will be stored.
Example #1
To translate all Singularity channel contracts to Promela models and analyze with Spin, execute the following command:
>tune.exe /i:"{SingularitySourceCodeRoot}" /t:Spin /o:{OutputDir}
Where {SingularitySourceCodeRoot} is the path to the root directory containing the Singularity source code, and {OutputDir} is the path to a directory where output will be stored.
Example #2
To produce a never claim to be inserted into a Promela model and checked using Spin:
>tune.exe /f:"{LTL Forumla}"
Where {LTL Forumla} is an LTL formula in Spin's syntax. In LTL formulas, contract elements such as states and messages can be reference by use specific prefixes as follows:
♦ To reference states, prefix with "pIN_STATE_"
♦ To reference a Server->Client message that has ever been sent, prefix with "pSENT_IMSG_"
♦ To reference a Client->Server message that has ever been sent, prefix with "pSENT_OMSG_"
♦ To reference the most recent message sent, prefix with "pLASTMSG_"
Example #3
To translate all Singularity channel contracts to Dot specifications and produce PDF documents containing state machine diagrams:
>tune.exe /i:"{SingularitySourceCodeRoot}" /t:Dot /o:{OutputDir}
Where {SingularitySourceCodeRoot} is the path to the root directory containing the Singularity source code, and {OutputDir} is the path to a directory where output will be stored.