Projects

The Nimbus Environment

Formal Verification--Model Checking

Formal Verification--Theorem Proving

Refutation using Random Search

Modeling Methodology

Specification Centered Testing

Statistical Testing

Correct Code Generation

CriSys Home

CS Home

Methodology

Despite advantages over traditional requirements techniques, formal specification languages have not achieved widespread use in industry.  One major obstacle is the lack of guidance on the process of writing of such a specification and descriptions of the most effective techniques for capturing the requirements in the desired language.  Although some work has been done on such guidelines, it is fragmented and incomplete.  Another barrier is cost: formal requirements specifications are typically much more costly to develop than their natural language counterparts.

Many companies that build critical systems often create lines of similar products, or product families.  Product family members (i.e., the individual products) share many common features (called commonalities) but vary in certain well-defined ways (called variabilities).  The concept of a product family is well understood in most industries. For example, in the auto industry, many cars from the same maker might share parts; some cars are even built on the same chassis with different sheet metal and trim, e.g., the Chrysler Concorde and Dodge Intrepid, or the Ford Taurus and Mercury Sable.  Unfortunately, in the software industry it is common to see different (but related) products being developed by different project teams with little coordination and essentially no reuse.  This duplication of effort is costly; and, it makes building a formal specification of each family member out of the question.  Therefore, reuse of the formal requirements specifications in the context of product families is absolutely essential for successful adoption of these techniques by industry.

A methodology, or set of guidelines, on how to create formal specifications would remove or reduce several major barriers to industrial acceptance by making the languages more accessible to the average practitioner and enabling reuse of the specifications.  The methodology must address how to organize, or structure, the requirements.  Just as a book must be organized to be readable, a requirements specification must be organized to be useful.  This research will produce structuring techniques that support the development of software families (for example, a line of pacemakers for different heart conditions), as well as more ad-hoc techniques suitable for special situations.  The methodology will include a discussion of the benefits and drawbacks of each technique.  The techniques will be illustrated in RSML^-e.

Special requirements specification language features that allow related pieces of the formal specification to be grouped together are necessary to support structuring for the requirements.  However, researchers have focused on the development of tools to assist in the creation of formal requirements, analysis of the requirements, and execution of the formal specifications, but not on techniques describing how to create the specifications. Thus, many formal specification languages lack such an organizational construct.  A part of the research will be to add an organizational construct to RSML^-e.  This will facilitate the techniques presented in the methodology and allow RSML^-e to be used in more extensive, industrial-sized case examples.

Finally, the methodology will integrate existing techniques and previous work.  This will make the methodology comprehensive: practitioners who wish to apply these techniques to their own systems will not have to read volumes of research journals.  Rather, the essentials of the current state-of-the-art will be presented in one location.