Description of Tool Performance Study
In this study, we used SPIN version 3.2.4, SMV version 2.5.3, and
INCA version 3.4. All runs were made on a Sun Enterprise 3500 with
two processors and 2 GB of memory, running Solaris 2.6. SPIN and SMV
were compiled with the Sun C compiler. For INCA, we used Harlequin
Lispworks 4.1.0.
We studied the time performance of these different tools on the
analysis of Chiron systems with two artists. We scaled the Chiron
systems as follows: given an integer n>1, we divided the
event set into three subsets of size approximately n/3 (with
allowances for rounding). The first artist registered for each event
in the first and third subsets, and the second artist registered for
each event in the second and third subsets.
The tables give a detailed accounting of the user + system time (in
seconds) for each part of the analysis, for each property (or part of
a property). The graphs give the total time for each analysis tool as
a function of the number of events in the Chiron system.
Description of table column headings
- Property
- the property or property part. For some tools and some properties,
the property was formulated in more than one part. These parts are
labeled, a, b, c, etc. For details, see the individual property
descriptions.
- Artists
- the number of artists in the Chiron system.
- Events
- the number of events in the Chiron system.
- a2s
- the time used by ada_to_sedl to translate the Ada source code into
SEDL.
- Derive
- the time used by INCA to construct its internal FSA
representations from the SEDL code.
- Never
- the time time used by SPIN to execute the "spin -F" command, which
is used to create a never clause from an LTL formula by constructing
the Büchi automaton.
- Prom
- the time used by INCA to generate the SPIN input file.
- Spin
- the time used by SPIN to execute the "spin -a" command, which
takes the Promela file generated by INCA and creates C source files to
analyze the problem.
- Cc
- the time used by the Sun C compiler to compile the SPIN analyzer.
- Pan
- the time used to execute the SPIN analyzer.
- Trans
- the time used by INCA to generate the SMV input file.
- SMV
- the time used by SMV to analyze the problem from the
INCA-generated input file.
- analyze
- the time used by INCA to analyze the property. For some
properties, this results directly in a conclusive verification of the
property, for others, the result is an inequality system which must be
analyzed for consistency by CPLEX before a conclusive result can be
given.
- Cplex
- the time used by CPLEX to solve the integer linear programming
created by the INCA "analyze" command.
- NNever
- like "Never", but for the Native SPIN version of the problem.
- NSpin
- like "Spin", but for the Native SPIN version of the problem.
- Ncc
- like "Cc", but for the Native SPIN version of the problem.
- NPan
- like "Pan", but for the Native SPIN version of the problem.
- FAda
- the time used by FLAVERS to go from the Ada source code to the
CFGs.
- FJava
- the time used by FLAVERS to go from the CFGs to the point where
the State Propagation algorithm can be executed.
- FSP
- the time used by FLAVERS to run the State Propagation algorithm,
returning an analysis result.
What is included in the totals
- For INCA
- Derive + Analyze + Cplex
- For INCA-SPIN
- Never + Spin + Cc + Pan
- For Native SPIN
- Nnever + NSpin + Ncc + NPan
- For INCA-SMV
- SMV
- For FLAVERS
- FAda + FJava + FSP
Parameters Used with INCA-SPIN
For all properties, SPIN was invoked with the command
spin -a <FILENAME>
For all properties except Deadlock (Property 0), the analyzer was then
compiled with the command
cc -DMEMCNT=32 -o pan pan.c
For Deadlock, it was compiled with the command
cc -DSAFETY -DMEMCNT=32 -o pan pan.c
For all properties other than Deadlock, the analyzer was then executed
with the command
pan -n -a
For Deadlock, the analyzer was executed with the command
pan -n
Parameters Used with Native SPIN
For all properties, SPIN was invoked with the command
spin -a <FILENAME>
For Deadlock, the analyzer was compiled with the command
cc -DSAFETY -DMEMCNT=32 -DNOBOUNDCHECK -o pan pan.c
For Property 8, the analyzer was compiled with the command
cc -DMEMCNT=32 -DSAFETY -o pan pan.c
For all other properties, the analyzer was compiled with
the command
cc -DMEMCNT=32 -DNOBOUNDCHECK -o pan pan.c
For Deadlock, the analyzer was executed with the command
pan -n
For Property 8, the analyzer was executed with the command
pan -n -E
For all other properties, the analyzer was executed with the
command
pan -n -a
Back to Chiron Analysis Tool Performance
Study