There is little doubt in the software engineering community that requirements engineering plays an important role in the development of a software system. Requirements engineering [1] is generally divided into 5 stages: elicitation of the requirements from the customer or user, analysis of the elicited requirements, management of the requirements (i.e., controlling of requirements), verification of requirements, and documentation.

Requirements engineering can employ a variety of methods that effectively capture requirements. Success with this phase of the development life cycle is considered crucial in that the remainder of life-cycle activities is highly dependent on this early foundation (in terms of schedule, cost, and user acceptance). These methods are broadly divided into three categories: informal, semi-formal, and formal methods [2], each having its own advantages and disadvantages.

In the requirement phase, requirements are often specified informally with a language in which the customer or end-user is familiar. This often results in the use of natural language (e.g., spoken and written English) to create a requirements document such as the system requirements specification or concept of operations [2]. Such informal specifications are not adequate in that they are often inaccurate, inconsistent, and ambiguous [2]. Natural language specifications are also very lengthy, making them difficult to check for completeness.

Applying semiformal methods that emphasize the use of graphical representations of the software being built can mitigate this disadvantage. A major problem with the semiformal approach, however, is the lack of precise semantics, which may lead to ambiguous interpretation of certain requirements. Sometimes the application of formal methods is offered as a solution to problems associated with both the informal and semiformal approaches.

Formal methods as with other approaches, also have specific advantages and disadvantages that may make their use desirable or impossible. In sections two, three and four of this article, is a brief discussion of formal methods and considerations bearing on their use. In that some of the disadvantages of formal methods are quite severe, a relaxed model of formal methods, know as lightweight formal methods has been proposed. A description of the lightweight, formal method technique is provided in section five. A summary is presented in section six.

Software systems under development are often categorized based on the application for which they are targeted. One such grouping is safety critical systems and non-safety critical systems. In safety-critical systems, faults may prove fatal to human life. Air-traffic control systems, patient record-management systems, medical systems, and avionics [2] fall into this category.

Another common grouping is complexity - some systems fall into the category of highly complex systems while others are considered less complex. Following traditional software development methods may not be suitable for the development of safety critical or highly complex systems.

It is essential that the system and software requirements be effectively captured, understood, and properly implemented in the later stages of development. Following informal and semiformal methods often does not give sufficient results in terms of precision and preciseness. A formal requirement specification tool has precise mathematical semantics [2]. A method using formal tools or notation is called a formal method. Formal methods usually employ a subset of mathematical notation consisting of set theory and logic [2] but may, depending on the tool selected, use a much more complicated notation (see [3] for a more complete treatment of this topic). A representation of the requirements based on mathematics will aid in the precise specification of the software, thereby ensuring that the correctness, completeness, and unambiguous properties of the system are preserved. The formal representation of software requirements also often provides a method for logical reasoning about the artifacts produced. This achieves more precision in the description and allows for a stronger design that satisfies required properties.

Informal methods normally use natural languages for requirement specification. A major advantage of natural language is its flexibility and ease of use. As suggested earlier, obtaining correct requirements early in the development process is critical to the correct development of the system and to schedule and cost considerations. The participation of stakeholders (e.g., users or customers) is important for proper requirements elicitation. The burden of this task normally falls to the system or software engineer working closely with the customer. Various verification and validation techniques are employed to obtain some confidence in correctness. Since the determination of correctness cannot be a unilateral process accomplished by the technical staff, it becomes important that the format of the requirement documents be such that all parties can read and understand them. This often drives the developer to use natural language. This decision, however, has many negative repercussions [4] that include the following:

• Noise: the presence of redundant information in the specification.
• Silence: the absence of certain necessary information in the specification.
• Over-specification: the reader is told too much about the solution while trying to grasp the problem.
• Contradiction: the presence of two or more elements in the text that define a feature of the system in an incompatible way.
• Ambiguity: the presence of an element in the text that makes it possible to interpret a feature of the problem in at least two different ways.
• Forward reference: the presence of elements in the text that use features of the problem not defined until later in the specification.
• Wishful thinking: occurs when solutions cannot be validated.

These negative aspects may affect latter phases of the software development and result in an incorrect system. Although the theoretical objective is total fault elimination in a system, in reality, most systems expect and plan for an acceptable level of defects. The type of system being delivered often dictates an acceptable threshold for such defects. If the system developed is not considered safety-critical for example, there is more flexibility about faults (e.g., commercial software products sold for general-purpose use). Such faults are often seen as correctable during the maintenance phase and in planned subsequent releases. In the case of safety-critical systems however, the objective becomes to drive defects to as close to zero as possible. In such environments, developers are often driven to use formal methods as a method of defect reduction - but not without significant cost to the development life cycle.

Formal methods for requirement specification have many well-known drawbacks. As noted earlier, formal methods use mathematical notation to represent requirements. These notations attempt to represent the system as a whole with all the necessary details to aid in the understanding and development of the system. Formal methods do not effectively handle large and complex system development [5]. The requirements for large and complex systems will always be problematic initially and will evolve continually throughout the life cycle. This creates a need for the method of requirement implementation to be flexible and robust, so that it can easily accommodate the inevitable continuous stream of change [5].

Many practicing programmers do not have advanced training in the field of mathematics and often think of formal methods as a difficult concept to master. This is, however, often not true because the level of knowledge of mathematics required to implement formal methods is not necessarily advanced [6]. Formal methods, like other software engineering techniques and tools, have various difficulty levels associated with them depending on the selected technique. A known common method is Z (pronounced Zed) with mathematics primarily based on set theory - at about the level one would expect to find taught during high school. Similarly, another method known as Communicating Sequential Processes is exceptionally difficult and would normally require specialized training. Model-based formal specifications are generally not difficult to teach and apply while axiomatic and algebraic methods are seen as more challenging.

The scarcity of well-worded examples of successful industrial use of formal methods is another limiting factor. Although there are certainly some examples in industry where formal methods were employed, these are generally very limited, rare, and generally apply to only a small part of the overall development. Many examples cited in the literature appear to be research oriented vs. practical application. Similarly, finding software engineers in industry with such experience (positive or negative) is extremely difficult. This implies that employing such talent would be even more difficult.

One argument for using formal methods has been damaging overall to the technique. The argument is that such methods can offer the ability to prove systems correct. The word prove is used here in a mathematical sense - that means rigorous proofs that specifications are consistent with a stated objective, that code is consistent with specification, and that code produces a desired result and none other. Academia is partially at fault for promoting this capability in the theoretical classroom where demonstrating a proof of concept is easy but where scalability of the technique is questionable. Proving software correct has not been a successful endeavor after more than 30 years of research, and remains elusive. This is not to claim that proofs cannot be done on critical aspects of the software system. As long as the amount of code is relatively small, proofs can be accomplished. This technique, however, should be viewed as a positive side effect of formalism and not a desired result. The primary objective of a strong formal approach should be in precise and unambiguous specification.

There are many myths associated with using formal methods [6, 7]. Some appear to be the main reason for the lack of acceptance of formal methods:

• Such methods can guarantee software perfection. This normally proves to be wrong since software is far too complex to offer any such guarantee. Practice proved this during the last 20 years in the area of computer security where trusted operating systems constructed at high levels of assurance using formalisms still failed.
• Only critical systems benefit from using formal methods. While it is true that critical systems need a rigorous use of formal methods, any system, irrespective of whether it is critical or not, can certainly benefit from using formal methods. The question is not benefit, but rather affordability.
• Formal methods increase the cost of software development. This is true when the development organization is in its initial stages of introducing formal methods, however, the high cost of formal methods can possibly be offset when compared with a reduced cost of corrective maintenance. Additionally, low personnel turnover and an experience base can reduce costs in an organization.
• Formal methods are incomprehensible to the client and therefore should not be used. Our experience shows this to be partially true and a consideration for the systems engineer (SE). Although you can argue that several model-based methods use commonly understood set theory, we still find customers think it is difficult and do not wish to work with such notation. All formal methods we are aware of used in practice require a natural language explanation of each formal representation as an effort to overcome the communication problem between the customer and the developer. This may lead, however, to an over dependence on the informal description and a secondary validation effort is required to insure that the informal description does indeed properly represent the formal.
• Formal methods may delay the development process. This may occur because any formal method relies heavily on construction and analysis of the specifications. This up-front effort expends more time, which can lead to a longer development cycle.

There are other concerns regarding the formal methods. A more comprehensive argument for and against is in [6, 7].

From the discussion above, it should be clear that the application of formal methods in its entirety is not as straightforward as it sounds, and certainly not a technique to be adopted without great consideration for its cost [7]. The application of lightweight formal method is a compromise solution for the above problems. Heavyweight formal methods (formal methods applied in their entirety) and lightweight formal methods both deal with the formalization of the software development process. However, they differ in terms of the extent and degree in which they are applied to the software development process (see Table 1).

Table 1: Characteristics of Formal and Lightweight Formal Methods
(Click on image above to show full-size version in pop-up window.)

Formal methods can be applied to all or selected components of a system in varying degrees, depending on the need. These degrees of formalization [5] can range from very formal to very informal. The very formal degree is often referred to as dry, and the very informal degree is referred to as wet formalization [5]. In dry formalization, metalanguage is also formalized and an object-level model is given as a formal theory in the metalanguage. In the less formalized models, the metalanguage may simply be a natural language representation. Formalization is useful only to the extent that it helps to meet concrete goals [5]. This range of formalization gives us the flexibility to apply formal methods as suited for the factors that influence formal method implementation.

Lightweight formalization lies at a level between dry and wet formalisms. Here, formal method applications will provide the advantages of formalism yet will reduce drawbacks due to over formalization. Carefully analyzing the system at hand and determining formalization's effect on the system can achieve this. It will lead the SE to decide "how much formalization is the right level of formalization?"

Cost, schedule, and the other relevant factors must be taken into consideration prior to proceeding to a decision. Specifically, the SE must consider the state of training in formal methods that exists within the development team and the expense to bring training up to an acceptable level. Second, the SE may need to consider the cost of a formal methods consultant. If applying lightweight formal methods is not a normal development skill, a consultant may become necessary.

Customer acceptance becomes an important factor. The decision to move ahead with a lightweight method should include customers in the decision process. The customer may need to commit to an additional close working relationship with the development team while formally specified requirements are constructed and analyzed. The customer's close-working relationship will most certainly involve a commitment for customer training and time, and perhaps an understanding that the need to analyze formal specifications will delay movement to design and code, which is often used to judge progress. In other words, without proper buy-in and understanding by the customer, the use of lightweight formal methods might be placed at risk early in the process - the customer may perceive that development is not moving fast enough.

Lastly, cost can become a factor. Customers often focus on cost as only a development activity ending with system delivery. The cost of development using formalism (of any type) is most certain to add cost to the life-cycle effort from requirements to initial delivery simply because more steps, processes, and time are involved. This is a false savings perspective, however. Years of empirical evidence [8] complied by software engineering researchers tells us that the majority of life-cycle cost lies in maintenance. More importantly, finding and fixing defects after delivery in large systems is often 100 times more expensive to fix then during the requirements phase.

This research has also shown that software projects spend 40 percent to 50 percent of their effort on avoidable rework. About 80 percent of avoidable rework comes from 20 percent of the defects; about 80 percent of the defects comes from 20 percent of the modules; and peer reviews catch 60 percent of defects. These investigative findings provide clear evidence that using a formalism-based approach on critical aspects of the system will pay dividends during the complete life cycle. It also proves that the reduction in cost achieved by a reduction in defects justifies investment in the early part of that life cycle. When looking at implementing lightweight formalism, the SE must consider all these factors and their influence on total cost, schedule, and delivered quality.

As described earlier, varying the degree of formalization can reduce its effects. Customer communication is an important factor in the success of requirement elicitation. The customer will be able to find faults in the requirements only if he/she is able to understand the requirement specification. If the specification is entirely formal, the customer or user is not likely to be able to understand the system properly, thus risking success of the requirement elicitation process.

Address this in two ways. First, select a formal method that involves notation easily understood by a large segment of the customer community (e.g., the Z language or perhaps the Vienna Development Method). Next, supplement this method with natural language descriptions and joint walkthroughs with the customer and the specification creator. This will combine the precision of specification (in the user's perspective) with the ability for correct analysis allowing the customer to contribute to the rigorous analysis that must take place.

Another interest in formalization is the range in which to apply it. Lugi and Goguen [5] suggest considering three different atomic units for the application of formal methods, which are defined as small, large, and huge. Classic formal methods fall into the small-grain category. These methods have a mathematical basis at the level of individual statement, and the complexity of this notation grows with program size. Small-grain methods have great difficulty in handling changes and thus fit poorly into the software life cycle. Large-grain methods involve module composition. They increase the atomic unit size from individual lines or small programs to modules that are collections of small programs. Huge-grain parts are much larger than small-grain statements and large-grain modules. They may be systems themselves, typically commercial off-the-shelf (COTS) systems.

Until now, the discussion was on the atomicity of formal method application. In the lightweight application of formal methods, atomicity plays an important role in determining the applicability of the method. If the atomicity is huge-grain, the smallest unit on which the formal methods can be applied is at the system level. Even if we can vary the complexity of the formalism, we cannot vary the range of application of formal methods. In the case of small-grain and large-grain atomicity, there is flexibility in the application of formal methods.

To make the requirements analysis cost effective, the cost of specification creation and analysis has to be reduced dramatically [3]. In pursuing this objective, the SE would search for automated tools that accompany the specification language to help maintain an electronic copy of the specification, traceability of modifications, documentation accompanying the specification, and perhaps assist in the analysis process. The cost of proving a system correct is generally much more than the cost of specifying the system, and is not recommended in the lightweight approach. The objective then becomes an in-depth analysis seeking correctness and completeness of the specification document vs. proof that the system itself is defect free. Using formal methods results in a high cost, thus industry is generally reluctant to invest in such an approach with low return value and where other more cost-effective approaches exist. Using a lightweight approach that emphasizes partiality and focused application can improve its cost effectiveness.

We based our previous discussion mainly on using formal methods in the specification of software requirements. Formal methods do not limit their application to the specification of requirements. They can also be useful in verification and validation of software requirements [3]. Mistakes that prove to be expensive to correct in later phases of the development life cycle generally originate in the initial stages of software development. If formal methods are used in specifying requirements, there is a high probability of detecting errors by formal verification and validation activities due to the precision of requirement structure and of verification and validation activities. To obtain the benefit of accuracy, reduce specification error, and yet remain cost competitive, it is suggested that verification and validation using formal methods should also follow a lightweight approach in most cases. The exception to this statement remains for safety-critical components where the need for correctness outweighs the additional cost incurred.

Daniel Jackson and Jeannette Wing [3] suggests four elements of a lightweight approach:

• Partiality in language. The language used for requirement specification should be both expressive and tractable. Treating the language as a general mathematical notation is ineffective. This generality comes at the expense of analysis. Therefore, the language used in specification should also have informal components existing in it.
• Partiality in modeling. Complete formalization of a large system is not feasible. Some details have to be preserved at the expense of other details. This decision-making is an important part in the success of the lightweight approach. There is not much freedom in the partiality of modeling if the system developed is a safety critical system. However, in the case of other normal large systems, this is not the case.
• Partiality in analysis. A sufficiently expressive language, even if designed for tractability cannot be decidable, making complete analysis impossible. It is better to sacrifice the ability to find proofs than to sacrifice ability to find faults. So the analysis should be flexible accepting the best practice suitable for the component under verification.
• Partiality in composition. For large systems, a single, partial specification may not be sufficient. It may be necessary to compose many partial specifications to allow some analysis of consistency.

This article discussed the application of formal methods in requirements engineering and made the case for a lightweight approach. It included a discussion of the pros and cons of the application of formal methods with respect to informal approaches and the domain of application. The authors suggest that the lightweight formal method has a better cost-effect ratio than the heavyweight formal methods and is more suited to actual industrial application. Find an in-depth study of empirical evidence to this conclusion in [9].

Many factors influence deciding when and where to use lightweight and heavyweight formal methods. For large complex projects, the application of a heavyweight formal method is virtually impossible thus the lightweight formal method is a good candidate. When we are dealing with safety-critical systems or even, perhaps, trusted systems (in the ISO 15408 sense), using the lightweight formal method is debatable. In these cases, it may be better to use a heavyweight formal specification and analysis if time and cost permit. This article's intent was to examine alternatives to strict formalism in software development and to suggest an intermediate solution between formal and informal. That solution is the adoption of a lightweight (or partial) approach.

1. Van Buren, Jim, and David A. Cook. "Experiences in the Adoption of Requirements Engineering Technologies." CrossTalk Dec. 1998.
2. Saiedian, Hossein. "Formal Methods in Information Engineering." Software Requirements Engineering. IEEE Computer Society, 1997.
3. Saiedian, Hossein. "An Invitation to Formal Methods." IEEE Computer 1996.
4. Meyer, Bertrand. "On Formalism in Specification." IEEE Software Jan. 1985.
5. Luqi, and Goguen, Joseph. A. "Formal Methods: Problems and Promises." IEEE Software Jan. 1997.
6. Hall, Anthony. "Seven Myths of Formal Methods." IEEE Software Sept. 1990.
7. Bowen, Jonathan P. and M. G. Hinchey. "Seven More Myths of Formal Methods." IEEE Software July1995.
8. Boehm, B., and V. R. Basili. "Software Defect Reduction Top 10 list." IEEE Computer Jan. 2001.
9. Eastbrook, Steve. "Experiences Using Lightweight Formal Methods for Requirements Modeling." IEEE Transaction on Software Engineering Jan. 1998.

1. This work is partially supported by the National Science Foundation, grant number CCR-0085749.

1. Feather, Martin. S. "Rapid Application of Lightweight Formal Methods for Consistency Analysis." IEEE Transaction on Software Engineering. Nov. 1998.
2. Gervasi, Vincenzo and Bashar Nuseibeh, "Lightweight Validation of Natural Language Requirements: A Case Study." Institute of Electrical and Electronics Engineers, 2000.

Vinu George is currently an instructor at Mary Holmes College, West Point, Miss. He previously worked as graduate researcher at Diagnostic Instrumentation and Analysis Laboratory, Mississippi State, in the field of instrumentation and control, software development. George has a master's degree in computer science from Mississippi State University and is currently a candidate for doctoral degree in computer science. He is a certified software engineer.

Department of Computer Science
P.O. Box 9637
Mississippi State University
Mississippi State, MS 39762
Phone: (662) 325-2756
E-mail: george@cs.msstate.edu

Rayford Vaughn, Ph.D., is a professor of computer science at Mississippi State University teaching and conducting research in software engineering and information security. Previously he served 26 years in the Army where he commanded the Army's largest software development organization and created the Pentagon Single Agency Manager organization. He also worked at the National Security Agency's National Computer Security Center where he authored national level, computer security guidance, and conducted computer security research. Dr. Vaughn retired as colonel in 1995 and worked as vice president, Defense Information Systems Agency, Integration Services, Electronic Data Systems. Dr. Vaughn is author of more than 30 publications and actively contributes to software engineering and information security conferences and journals. He has a doctorate degree in computer science from Kansas State University.

Department of Computer Science
P.O. Box 9637
Mississippi State University
Mississippi State, MS 39762
Phone: (662) 325-2756
E-mail: vaughn@cs.msstate.edu