Quick Start to Verification
with
TVT-Tools

Antti Puhakka


 

ARA

TVT

LTS file format

ARA LTS

TVT LSTS

Input language -> LTS

arassgu (LOTOS)

tvt.compiler

Visualisation

araillux (does not work very well)
lts2ps (PostScript)

tvt.illux

Simulation

arasimu (LOTOS)

tvt.simulate

System
construction

ltspar, stool (stubborn set parallel composition + hiding)

tvt.createrules,
tvt.parallel (parallel composition + hiding + renaming)

CFFD-reduction / normalisation

aranoru

tvt.CFFD_normalize

Bisimulation minimisation

arabisim

tvt.SBreduction

Comparison (w.r.t. CFFD)

aracompu

tvt.CFFDcompare

Conversion ARA <-> TVT

 

tvt.fftool

Translating Processes from TVT Input Language into LSTSs

Visualisation

Composing Systems

Reducing and Comparing Systems

A Small Verification Example


abp_sender.prog:
TYPEDEF
   BitValue: [ bit0 bit1 ]

PROCESS Sender

GATES
   send sdata rack

IS

VARIABLES
   bit: BitValue

EVENT_PARAMS
   sdata<BitValue>
   rack<BitValue>

INIT
   [ bit' = bit0; ] -> idle

*idle:
   send -> senddata

*senddata:
   sdata!bit -> senddata
   rack!bit [ bit' = INC bit; ] -> idle

ENDPROC

abp_datachannel.prog:
TYPEDEF
   BitValue: [ bit0 bit1 ]

PROCESS DataChannel

GATES
   sdata rdata

IS

VARIABLES
   recBit: BitValue

EVENT_PARAMS
   sdata<BitValue>
   rdata<BitValue>

INIT
   [recBit' = bit0;] -> wait

*wait:
   sdata?recBit' -> received

*received:
   rdata!recBit -> wait
   TAU -> wait

ENDPROC

abp_ackchannel.prog:
TYPEDEF
   BitValue: [ bit0 bit1 ]

PROCESS AckChannel

GATES
   sack rack

IS

VARIABLES
   recBit: BitValue

EVENT_PARAMS
   sack<BitValue>
   rack<BitValue>

INIT
   [recBit' = bit0;] -> wait

*wait:
   sack?recBit' -> received

*received:
   rack!recBit -> wait
   TAU -> wait

ENDPROC

abp_receiver.prog:
TYPEDEF
   BitValue: [ bit0 bit1 ]

PROCESS Receiver

GATES
   rec rdata sack

IS

VARIABLES
   bit recBit: BitValue

EVENT_PARAMS
   rdata<BitValue>
   sack<BitValue>

INIT
   [ bit' = bit0; ] -> wait

*wait:
   rdata?recBit' -> received

*received:
   [ recBit = bit ] -> rec DELETE recBit -> declared
   [ recBit != bit ] -> sack!recBit DELETE recBit -> wait

*declared:
   sack!bit [ bit' = INC bit; ] -> wait

ENDPROC

abp.ren:
"sdata";
"sdata";
"rdata";
"rdata";
"sack";
"sack";
"rack";
"rack";

abp.col:
"send" blue
"rec" green
"tau" grey