Verification  Engineering

                         Scott   A.  Smolka


{\em Model checking} is powerful technique for verifying hardware and software
systems, especially safety critical systems such as implantable medical
devices, nuclear power plant control software, etc.  Until recently, such
verification activity has been carried our in relative isolation, separate
from the traditional software lifecycle, which involves, among other things,
design, specification, coding, testing, and maintenance.

Our research on model checking and verification in general is concerned with
ameliorating this problem by integrating verification into the lifecycle model.
The goal is to make verification more of an {\em engineering} discipline, on
par and equal to software engineering.  The approach we are following is
manifest in the Concurrency Factory, a graphical environment for the design,
simulation, verification, and implementation of concurrent and distributed
systems.  The project, which is a joint effort between SUNY Stony Brook and
North Carolina State University, officially started in Spring '92, and is
currently supported by grants from  NSF, ONR, and AFOSR.

Two themes central to the project are the following: the use of {\em process
algebra}, e.g., CCS, ACP, CSP, as the underlying formal model of computation,
and the provision of {\em practical} support for process algebra.  By
``practical'' we mean that the Factory should be usable by protocol engineers
and software developers who are not necessarily familiar with formal
verification, and it should be usable on problems of real-life scale, such as
those found in the telecommunications industry.

In this talk, I will describe ongoing research related to the Concurrency
Factory and three recent applications of the Concurrency Factory:
\begin{itemize}
\item Northrop Grumman E-2C Reliable Broadcast Protocol -- The E-2C Hawkeye is an
  airborne early warning/command and control aircraft developed by the Northrop
  Grumman Corporation.  The Hawkeye can monitor 6 million cubic miles of air
  space and more than 15,000 square miles of ocean surface for the presence of
  aircraft, missiles, ships, and fixed targets.  Ph.D. candidate Yifei Dong,
  Gene Stark, and I   have succeeded in modeling and verifying certain aspects
  of the on-board communication software, including a race condition known as
  ``early disconnect.''
\item i-protocol -- The i-protocol is a full-duplex, packet-based, sliding-window
  protocol equipped with several optimizations at reducing control message
  traffic.  It forms part of the GNU UUCP protocol stack.  Y.S. Ramakrishna has
  succeeded in using the Concurrency Factory's model checking facility to
  detect and diagnose a livelock error in the i-protocol.  Ph.D. candidate Vic
  Du has subsequently performed a comparative study of several state-of-the-art
  verification tools (SPIN, COSPAN, SMV) using the i-protocol as a case study.
\item RETHER protocol -- The RETHER protocol is a real-time ethernet protocol for
  the transmission of real-time data such as video over an ethernet.  It was
  designed and implemented by Chitra Venkatramani and Prof. Chiueh.  Evangelos
  Nanos, an M.S. student, Kevin McDonnel, an undergraduate, and Vic Du have
  specified and verified RETHER using the Concurrency Factory.  In the process
  of doing so, we identified a simpler and possibly more economical
  implementation of Rether, which we have also verified. 
\end{itemize}

For more information about the Concurrency Factory, please see:
  http://www.cs.sunysb.edu/~concurr
  http://www.cs.sunysb.edu/~ysr/wrkshp/wrkshp.html
  http://www.cs.sunysb.edu/~clubconc
  http://www.cs.sunysb.edu/~sas

For an overview of Concurrency Theory, the theory behind the Concurrency
Factory, please see:
  
  http://www.cs.sunysb.edu/~sas/sdcr/report/final/final.html