% \documentclass[9.5pt,journal,final,finalsubmission,twocolumn]{IEEEtran}
\documentclass[12pt,journal,draftcls,letterpaper,onecolumn]{IEEEtran}
%\documentclass[12pt,journal,letterpaper,onecolumn]{IEEEtran}
\usepackage{cite,graphicx,url,algorithmic,multirow}
\hyphenation{spec-ifi-cation mega-bytes}
\usepackage{lineno}
%%%%% deleted...
% \newcommand{\thetitle}{The Benefits of Combining Diverse Model
% Translation and Verification Strategies}
%%%%% added...
\newcommand{\thetitle}{Combining Diverse Translation and Verification
Tools to Detect Faults in SCR Specifications}

\begin{document}
\title{\thetitle}
\author{David~Owen, % ~\IEEEmembership{Member,~IEEE,}
  Bojan~Cukic,~\IEEEmembership{Member,~IEEE,}
  and~Tim~Menzies,~\IEEEmembership{Member,~IEEE}}

\markboth{IEEE Transactions on Software Engineering,~Vol.~XX, No.~X,~Month~200X}
  {Owen \MakeLowercase{\textit{et al.}}: \thetitle}

\pubid{} % just to make space for IEEE copyright info

\maketitle

\modulolinenumbers[2]
\linenumbers

\begin{abstract}
It can be difficult to determine which verification strategy is best
for a particular software system.  Researchers have observed
complementary relationships between verification tools and argued
that there is no single best verification tool: as users' needs
change, the choice of tool should change as well.
%%%%% deleted...
% We provide further
% evidence of complementary relationships between verification tools,
% specifically considering tools available for software specifications
% written in the Software Cost Reduction (SCR) modeling language. We
% show how verification tools and their associated modeling languages
% may be considered complementary in terms of both accuracy and
% scalability. Rather than providing guidance for users deciding
% between tools, we argue that a verification strategy combining
% results from multiple tools will yield the most accurate results,
% i.e., results worthy of the greatest trust.
%%%%% added...
We provide further evidence of complementary relationships between
verification strategies, specifically considering tools for automatically
translating from the Software Cost Reduction (SCR) modeling language to
several different verification and debugging tools for formal models.
We show how verification strategies---each with its own formal modeling
languages, automatic translator and verification tool---may be considered
complementary in terms of both accuracy and scalability.  Rather than
providing guidance for users deciding between strategies, we argue that
a verification strategy combining results from multiple tools will yield the
most accurate results, i.e., the results worthy of the greatest trust.

% This article provides several motivating examples in which the use
% of multiple verification tools resulted in improved accuracy and
% performance.  In some cases the use of a single tool would have
% produced incorrect results, giving no indication to the user that
% the tool had been used incorrectly.  The use of a second tool,
% producing results inconsistent with the first, led to a better
% understanding of both tools and greater accuracy of the overall
% verification result. We discuss a case study that produced
% experimental results consistent with motivating examples, showing
% how four verification tools can be used together effectively to
% verify software specifications written in the SCR modeling language.

\end{abstract}

\begin{keywords}
%%%%% deleted...
% Software verification, model checking, tool diversity, fault
% tolerance, software performance.
%%%%% added...
Software verification, model checking, mutation of specifications,
automatic translation, fault detection, scalability of verification and
debugging tools.
\end{keywords}

\label{introduction}
\input{introduction}

\label{related}
\input{related}

\label{motivation}
\input{motivation}

\label{dsn08-background}
\input{dsn08-background}

\label{case-study}
\input{case-study}

\label{discussion}
\input{discussion}

\label{conclusion}
\input{conclusion}

\bibliographystyle{IEEEtran.bst}
\bibliography{phd}

\end{document}
