Click for next page ( 13


The National Academies | 500 Fifth St. N.W. | Washington, D.C. 20001
Copyright © National Academy of Sciences. All rights reserved.
Terms of Use and Privacy Statement



Below are the first 10 and last 10 pages of uncorrected machine-read text (when available) of this chapter, followed by the top 30 algorithmically extracted key phrases from the chapter as a whole.
Intended to provide our own search engines and external engines with highly rich, chapter-representative searchable text on the opening pages of each chapter. Because it is UNCORRECTED material, please consider the following text as a useful but insufficient proxy for the authoritative book pages.

Do not use for reproduction, copying, pasting, or reading; exclusively for search engines.

OCR for page 12
Requirements and Software Architectural Analysis Because specifications of software requirements are typically ex- pressed in "natural" rather than technical language, they suffer from ambiguity and incompleteness. Poorly specified requirements are often the cause of software defects. It is believed that roughly half of soft- ware defects are introduced during the requirements and functional analy- sis stage, 1 and some well-known software development projects have had a large percentage of serious software defects introduced during the specifica- tion of requirements. Therefore, utilization of techniques that improve the software requirements can save substantial time and money in software development and will often result in higher-quality software. The ability to develop high-quality requirements specifications is of crucial importance to the Department of Defense (DoD) in particular, since catastrophic failure (including loss of life) can result from defects in some DoD software-inten- sive systems. Clearly, any important advances in methods for requirements specification and checking need to be considered for use with DoD sys- tems. In addition to the more timely identification of software defects and design problems, the development of better requirements specifications can 1Results of a 1992 study (Lutz, 1993) of defects detected during the integration and testing of the Voyager and Galileo spacecraft showed that 194 of 197 significant software defects could be traced to problems in the specification of function and interface require- ments. 12

OCR for page 12
REQUIREMENTS AND SOFTWAREARCHITECTURAL ANALYSIS 13 also facilitate software testing by establishing a solid foundation for model- based testing and for estimating the testability of a software system. In this section we discuss in detail two methodologies useful for re- quirements specification: software cost reduction and sequence-based speci- location. SOFTWARE COST REDUCTION Constance Heitmeyer of the Naval Research Laboratory described soft- ware cost reduction (SCR), a set of techniques for developing software, pioneered by David Parnas and researchers from the Naval Research Labo- ratory (NRL) beginning in 1978. A major goal of the early research was to evaluate the utility and scalability of software engineering principles by applying them to the reconstruction of software for a practical system. The system selected was the Operational Flight Program (OFP) for the U.S. Navy's A-7 aircraft. The process of applying the principles to the A-7 re- quirements produced new techniques for devising precise, unambiguous requirements specifications. These techniques were demonstrated in a re- quirements document for the A-7 OFP (Heninger, 19801. Further re- search by Heitmeyer and her group during the 1990s produced a formal model to define the special SCR notation (Heitmeyer, leffords, and Labaw, 1996) and a suite of software tools for verifying and validating the correct- ness of SCR-style requirements specifications (Heitmeyer, Kirby, Labaw, and Bharadwaj, 19981. A-7 and Later Developments The A-7 requirements document, a complete specification of the re- quired behavior of the A-7 OFP, demonstrated the SCR techniques for specifying software requirements (Heninger, 19801. It introduced three major aspects of S CR: the focus on system outputs, a special tabular notion for specifying each output, and a set of criteria for evaluating a require- ments document. A critical step in constructing an SCR software require- ments document is to identify all outputs that the software must produce and to express the value of each output as a mathematical function of the state and history of the environment. To represent these functions accu- rately, unambiguously, and concisely, the A-7 document introduced a spe- cial tabular notation that facilitates writing and understanding the func- tions and also aids in detecting specification errors, such as missing cases

OCR for page 12
14 INNOVATIONS IN SOFTWARE ENGINEERING and ambiguity. A requirements specification must satisfy three important criteria in order to be acceptable: (1) completeness (i.e., any implementa- tion satisfying every statement in the requirements document should be acceptable), (2) freedom from implementation bias (i.e., requirements should not address how the requirements are addressed), and (3) organiza- tion as a reference document (i.e., information in the document should be easy to find). During the 1980s and 1990s, a number of organizations in both in- dustry and government (such as Grumman, Bell Laboratories, NRL, and Ontario Hydro) used SCR to document the requirements of a wide range of practical systems. These systems include the OFP for the A-6 aircraft (Meyers and White, 1983), the Bell telephone network (Hester, Parnas, and Utter, 1981), and safety-critical components of the Darlington nuclear power plant (Parnas, Asmis, and Madoy, 19911. In 1994, SCRwas used to document the requirements of the operational flight program of Lockheed's C-1301 aircraft (Faulk, 19951. The Lockheed requirements document con- tains over 1,000 tables and the operational flight program over 250K lines of Ada source code, thus demonstrating that SCR scales. Until the mid-1990s, SCR requirements specifications were analyzed for defects using manual inspection. While such inspection can expose many defects in specifications, it has two serious shortcomings. First, it can be very expensive. In the certification of the Darlington system, for ex- ample, the manual inspection of SCR tabular specifications cost millions of dollars. Second, human inspections often overlook defects. For example, in a 1996 study by NRL, mechanized analysis of tables in the A-7 require- ments document exposed 17 missing cases and 57 instances of ambiguity (Heitmeyer, leffords, and Labaw, 19961. These flaws were detected after the document had been inspected by two independent review teams. Thus, while human effort is critical to creating specifications and manual inspec- tions can detect many specification errors, developing high-quality require- ments specifications in industrial settings requires automated tool support. Not only can such tools find specification errors that manual inspections miss, they can do so more cheaply. To establish a formal foundation for tools supporting the development of an SCR requirements specification, Heitmeyer and her research group formulated a formal model to rigorously define the implicit state machine model that underlies an SCR requirements specification. In the model, the system, represented as a state machine, responds to changes in the value of environmental quantities that it monitors (represented as monitored vari-

OCR for page 12
REQUIREMENTS AND SOFTWAREARCHITECTURAL ANALYSIS 15 ables) by changing state and possibly by changing the values of one or more environmental quantities that it controls (represented as controlled vari- ables). For example, an avionics system might be required to respond to a severe change in air pressure by sounding an alarm; the change in pressure corresponds to a change in a monitored quantity, while the sounding of the alarm represents a change in a controlled quantity. NRL has designed a suite of software tools for constructing and ana- lyzing SCR requirements specifications. The SCR tools have been de- signed to support a four-step process for developing requirements specifi- cations. First, the user constructs a requirements specification using the SCR tabular notation. Second, the user invokes a consistency checker (Heitmeyer, leffords, and Labaw, 1996) to automatically detect syntax and type defects, missing cases, ambiguity, and circular definitions in the speci- fication. When a defect is detected, the consistency checker provides de- tailed feedback to aid in defect correction. Third, to validate the specifica- tion, the user may run scenarios (sequences of changes in the monitored quantities) through the SCR simulator (Heitmeyer, Kirby, Labaw, and Bharadwaj, 1998) and analyze the results to ensure that the specification captures the intended behavior. To facilitate validation of the specification by application experts, the simulator supports the rapid construction of graphical user interfaces, customized for particular application domains. Finally, the user may analyze the requirements specification for critical application properties, such as security and safety properties, using static analysis tools. For example, the user may run a model checker, such as SPIN (Holtzman, 1997), to detect property violations, or a verification tool, such as the Timed Automata Modeling Environment (TAME) (Ar- cher, 1999), to verify properties. In using TAME, a specialized interface to the general-purpose theorem-prover prototype verification system, com- pleting a proof may require proving auxiliary properties. To construct these auxiliary properties, the user may invoke the SCR invariant genera- tor Jeffords and Heitmeyer, 1998), a tool that automatically constructs state invariants (properties true of every reachable state) from an SCR re- . .^ . qulrements specl~lcatlon. Industrial Examples Three specific case studies were presented at the workshop. In the first, engineers at Rockwell Aviation applied the SCR tools to a specifica- tion of their Flight Guidance System. Despite extensive prior manual re-

OCR for page 12
16 INNOVATIONS IN SOFTWARE ENGINEERING views of the specification, the tools discovered 28 defects, many of them serious. The second case study involved a specification developed by Elec- tric Boat of the software requirements of a Torpedo Tube Control Panel (TTCP). The software in this case was approximately 15,000 lines of rela- tively complex code. In under five person-weeks, the contractor specifica- tion was translated into SCR, and the SCR tools were used to analyze the specification for errors and to develop a realistic simulator for demonstrat- ing and validating the required behavior of the TTCP. Analysis with the SCR tools and the SPIN model checker identified a serious safety violation in the SCR specification. In the third case study, an SCR requirements specification was devised for a software-based cryptographic device under development at NRL. TAME was used to analyze the specification for eight security properties (e.g., if a cryptographic device is tampered with, the keys are "zero-ized"~. The analysis showed that the SCR specification of the required behavior of the device satisfied seven of the properties and violated the eighth, and therefore the requirements were inconsistent. SEQUENCE-BASED SOFTWARE SPECIFICATION Another approach to the development and verification of complete, consistent, and correct specification of requirements is sequence-based specification, which is described in Prowell et al. (19991. The methodol- ogy was effectively illustrated with the example of a security alarm system. The method begins with stage I, the "black box" definition. The first step of this stage is to "tag" the requirements, i.e., give each of the initially specified requirements a numerical tag (from 1 to n). In the example of the security alarm, the fourth requirement is that if a trip signal occurs while the security alarm is set, a highly pitched tone (alarm) is emitted. Through the remainder of the sequence-based specification process, it is likely that additional requirements will be identified, and they are referred to as derived requirements and are typically given a numerical tag pre- ceded by a "D." The tagging of requirements is followed by a listing of the input stimuli that the system is expected to respond to and a listing of the responses that the system is expected to provide, with both linked back to the requirements. For example, stimuli include setting the alarm, tripping the alarm, entering a bad digit in sequence for turning off the alarm, and entering a good digit in sequence for turning off the alarm. An example of a response is "alarm is turned on when it is tripped," traced back to the fourth requirement.

OCR for page 12
REQUIREMENTS AND SOFTWAREARCHITECTURAL ANALYSIS 1, 7 All possible sequences of input stimuli are then listed in strict order, starting with stimuli of length zero, then one, and so on. For example, if CC r~'' 1 1 CC~' 1 1 CC~ '' 1 1 ~ represents setting tne alarm, 1 tripping tne alarm, ~ entering a can digit, and C`G" entering a good digit, then C`SGGT" is a stimuli sequence of length four. Enumeration of input sequences ends when all sequences of a given length are either C`illegal" or equivalent to a previous sequence, where equivalent means that the two sequences stimulate identical behavior of the system. The correct system response linked to each stimuli sequence is determined by tracing back to the associated requirement tag or tags. When no requirements exist to determine the response, derived requirements are defined and tagged. This process ensures that system behavior is defined for all possible (finite-length) input sequences (an infinite number), and the enumeration process guarantees that this will be done while consider- ing the smallest possible number of sequences. When the enumeration is complete, each stimulus sequence has been mapped to a response and one or more requirements. If each requirement has been cited at least once the specification is both complete and since each stimuli sequence is mapped to a single response consistent. Finally, engineers (or domain experts) can determine whether each derived (and . . . . Orlglnal requirement IS correct. The complete enumeration provides the starting point for stage II, the C`state box" definition. State variables are used to distinguish between dif- ferent states of the system. Each nonequivalent stimuli sequence is exam- ined to identify the unique conditions in the sequence, and state variables are invented to represent these conditions. In the example of the security alarm, the states are whether the device is on or off, whether the alarm is on or off, and whether the digits entered are consistent with the password. Whereas the black box representation of the system was expressed in terms of stimuli sequences and responses, the state box representation is expressed in terms of the current stimulus, the current state of the system, and the system response and state update. The correctness of the specifications can now be examined sequentially as stimuli are processed by the system. (This state box is an excellent starting point for the model underlying Markov chain usage testing, discussed in the following section.) Sequence-based specification provides a constructive process for defin- ing the state machine in a manner that ensures complete, consistent, and correct requirements, whereas SCR, in attaining the same goals, relies on intuition assisted by graphical tools to develop the state machine. A schema called Z (developed by Woodcock and others; see, e.g., Woodcock and

OCR for page 12
18 INNOVATIONS IN SOFTWARE ENGINEERING Davies, 1996) is a type of "set theory" for the formal prescription of state machines. There are tools available for Z and some impressive applications have been made by those mentioned above in collaboration with IBM's Cambridge Lab. A related method developed at IBM's Vienna Lab and known as VDM (for Vienna Development Method) is less formal than Z. Other approaches include that of Luckham and others (see, e.g., Luckham et al., 1995) who have developed a system that is fully formal, and SRI, whose formal system was developed by Rushby and others. Both of these approaches have tools that assist in their application. In the telecommuni- cations industry, there are two state-based systems, Statemate2 and State Description Language, neither of which is constructive but both of which are based on a well-understood application and which use idioms of the application that are accepted as correct based on extensive engineering ex- perience and field success. David Parnas (see Bartoussek and Parnas, 1978, and Parnas and Wang, 1989) has continued SCR in a direction using rela- tions rather than functions and developed table templates for various stan- dard expressions of common needs in software. Prototype tools have also been developed to convert tabular representations of relations to code (see e.g., Leonard and Heitmeyer, 20031. In conclusion, the specification of requirements, if poorly imple- mented, can be an important source of software defects for defense systems. A number of relatively new approaches to checking the specification of requirements have now been developed that can be used to create a set of consistent, complete, and correct requirements. Two leading approaches were described at the workshop, SCR and sequence-based software specifi- cation. SCR has been successfully applied to a number of defense and defense-related software systems. Sequence-based specification has some theoretical advantages given that it is more algorithmic in its application. Both methods are still relatively new and are being further developed, and software tools are increasingly available to facilitate their application. In 2The semantics of Statemate is being applied to the definition of formal behavioral semantics for the graphical state diagram notation employed by the Unified Modeling Lan- guage standard. This modeling and domain analysis notation for system specifications is supported by many vendor tools. See, e.g., Harel and Kupferman (2002) and Harel (2001).

OCR for page 12
REQUIREMENTS AND SOFTWAREARCHITECTURAL ANALYSIS 19 addition, other related approaches have similar advantages. The workshop participants generally agreed on the potential benefit of applying these methods widely to defense software systems in development, and therefore the value of continued testing and analysis of the applicability of such meth- ods to defense systems.