Bojan: 
the best place to handle R2-8 might be as some additional text added to the r0.tex stuff i sent you before.

--------------

OLD>
One drawback with  our proposal is that users have a hard enough
time running one translation system, let alone multiple versions.
Having said that, our work highlights the advantages of combining
verification systems. A future direction that arises from our work
is simplifying the overhead associated of moving specifications and
properties between verification systems. There are early signs that
the research community is moving in that direction. For example,
the BEEM website\footnote{Benchmarks for Explicit Model checkers  
\url{http://anna.fi.muni.cz/models/}.} lists an extensive
benchmark suite for explicitly model checkers.    To use the
benchmarks, researchers must build a translator from the syntax
used at this site into their own local format. Given a back-translator
(from the local format back to the BEEM format), then the  BEEM syntax
could become a {\em lingua franca} connecting together multiple verification
systems and enabling our proposal to use multiple verification systems.

NEW>
One drawback with  our proposal is that users have a hard enough
time running one translation system, let alone multiple versions.
Having said that, our work highlights the advantages of combining
verification systems. A future direction that arises from our work
is simplifying the overhead associated of moving specifications and
properties between verification systems. 

There are early signs that
the research community is moving in that direction:
\bi
\item
The BEEM website\footnote{Benchmarks for Explicit Model checkers  
\url{http://anna.fi.muni.cz/models/}.} lists an extensive
benchmark suite for explicitly model checkers.    To use the
benchmarks, researchers must build a translator from the syntax
used at this site into their own local format. Given a back-translator
(from the local format back to the BEEM format), then the  BEEM syntax
could become a {\em lingua franca} connecting together multiple verification
systems and enabling our proposal to use multiple verification systems.
\item
A consortium of researchers at NASA's Langley research center~\cite{miller05}
have developed cross-language translators from Simulink, StateFlow to 
NuSMV, the PVS interactive theorem prover, and the Sal language 
from Stanford Research Institute~\footnote{\url{http://sal.csl.sri.com/}}. The key to
this translation library is a pre-translation step to Lustre, then compilers that convert
Lustre models to the formats required by various formats needed for the verification engines.
\ei
The Langley and BEEM work indicate that, in the near future, it will be both practical and simple
to implement our proposal for the use of  multiple verification systems.

@misc{miller05,
	title="Model-Based Analysis \& Design",
	author="Steven S. Miller",
	notes="Available from \url{http://shemesh.larc.nasa.gov/fm/fm-flightdeck.html}, see the
			link ``Methods and Tools For Flight Critical Systems''",
	year=2005
}

