Position Statement:  Insup Lee
 -------------------------------------

 Some lessons learned from extracting formal models from
 informal requirements

 Insup Lee
 Department of Computer and Information Science
 University of Pennsylvania

 Requirements are usually specified in natural language.  We present
 issues, challenges and opportunities of extracting formal models from
 informal requirements based on two case studies.

 The first case study is an infusion pump system being developed by
 WRAIR (Walter Reed Army Institute for Research).  The system consists
 of an infusion pump, a blood pressure measurement unit, and the CARA
 software, where CARA is an algorithm for controlling an infusion pump
 to allow rapid stabilization of a patient's blood pressure.  WRAIR
 provided us with a set of informal requirements for CARA consisting of
 a tagged requirements document and a listing of questions and answers
 which amended that document.  The tagged requirements document mixed
 user, system, and environmental requirements.  We used these documents
 to create manually a formal model of the CARA system, as a number of
 EFSM's (Extended Finite State Machine).  These EFSM models were used
 as a reference specification by several teams that modeled the system
 using a variety of analysis tools.  We also constructed a
 hardware-in-the loop simulation of the infusion process.  The case
 study allowed us to gain a better understanding of the model features
 that need to be extracted from informal documents.

 The second case study considers the FDA regulation 21 CFR 610.40,
 ``Hepatitis B Testing Protocols'' that contains guidelines for the
 nation's blood bank industry.  This industry encompasses the
 collection, testing, distribution, and management of blood products.
 The systems managing these blood products may be categorized as very
 large, partial real-time, distributed inventory systems.  It has been
 established that blood product management system developers are having
 difficulty translating regulatory requirements into their operational
 management systems, and that the complexity of these systems makes
 them subject to errors and unforeseen consequences.  The goal of the
 case study is to assess the feasibility of the model extraction
 process.  The translation tasks were done manually.  We extracted an
 EFSM specification in a format suitable for analysis and test
 generation.  The case study allowed us to better understand the
 features needed in EFSM to cope with partial models and dealing with
 merging of partial models as well as actual testing of a working 
 system.