[Presented at the Eleventh International Software Quality Week 1998,May 26-29, 1998]
Formal Specification Languages in Conformance Testing
Kathy Liburdy, Meerkat Computing
Martha M. Gray and Lynne S. Rosenthal, Information Technology Laboratory,
National Institute of Standards and Technology
Introduction
The application of Formal Specification Languages (FSLs) to conformance testing is a relatively new area of study in software engineering. Interest in this area has been motivated by a realization that the traditional approach to conformance testing suffers from shortcomings which severely hinder the timely development of effective tests [GRA94]. The traditional approach relies on a natural language description of a test (e.g., a sentence or two describing a purpose) and a programming language implementation of the test. The use of natural languages to state specifications introduces ambiguity and provides little support for automating portions of the test development process. Similarly, the use of programming languages to implement conformance tests imposes many language features and constraints designed to support software development rather than software testing. As a result, the traditional approach to conformance testing is best characterized as a highly labor intensive development process which yields deficiencies in the quality of the resulting tests. The goal of this report is to assess the potential advantages to be gained through the application of formal specification languages to the problems of conformance testing.
Although the problems associated with conformance testing are well known, they bear repeating in this report to serve as guidelines for evaluating potential alternatives. Alternatives, especially those based on formal specification languages, will be required to demonstrate significant improvements in these areas in order to be accepted by the user community. Therefore, these problems with traditional approaches might also be viewed as a potential basis for metrics to be applied to evaluate alternatives based on formal description techniques. For example, one problem associated with traditional approaches to conformance testing is that they are error prone. If a measure can be developed to demonstrate that fewer errors are introduced in an alternative approach, more support may be gained to adopt the alternative approach.
Specific problems associated with the labor-intensive nature of traditional conformance test development include:
* Error prone
* High cost of development
* Significant time lag with corresponding standards
Problems associated with the quality of conformance tests developed using the traditional approach include:
* Difficult to modify and maintain
* Difficult to measure coverage of the corresponding standard
* Difficult to subset or extend functionality
In view of these problems, the general goals of an alternative approach may be stated as follows:
* Reduce the labor associated with test development by using languages designed especially for the expression of tests, and which form a basis for automated tool support and test development environments.
Figure 1. The general areas of Consensus-based Software Standards, Specification Languages, and Software Correctness contribute constraints and unsettled issues to the problem of applying Formal Specification Languages to Conformance Testing.
Open Issues
Specification Languages
A broad definition of a language is a set of strings (or sentences) defined by a grammar with the fundamental purpose of facilitating communication. Within the context of software engineering, a specification language expresses software behavior or characteristics. Specification languages may be categorized as natural or formal. Natural languages enjoy the advantage of familiarity but have the inherent characteristic of ambiguity. Ambiguity allows a great degree of expressiveness in day to day communication among people. People often rely on past experience or current context to resolve ambiguities, or intentionally use ambiguities for recreational purposes such as humor.
In software specification, however, ambiguities can be disastrous resulting in lawsuits, loss of property, and even loss of life. Formal specification languages offer the ability to remove such ambiguities by providing a precise meaning for each valid syntactic structure. In addition, an important benefit obtained by the removal of ambiguities is the enhanced capability for machine manipulation and subsequently tool support.
The type of tool support receiving the most attention in the formal methods community has been related to formal verification techniques such as theorem proving. However, the overhead associated with learning and applying formal specification languages in a comprehensive environment designed for theorem proving has been rejected by many in the software community. Subsequently, the question of partial applications of formal methods, sometimes referred to as "lightweight" formal methods, has arisen. Levels of partial use of FSLs have been identified, ranging from supplementing natural language specifications with mathematical notation to the use of FSLs for complete specification but without formal verification techniques. Therefore, when considering the question of how FSLs may be applied to conformance testing, the various levels of potential application must also be considered.
Figure 2. Open Issue: What level of use of FSLs will be adopted by the software community?
Software Standards
In the consensus-based approach to standardization, volunteers from many different cultures and backgrounds come together and work toward reaching a consensus on the emerging software standards. Conformance testing is obviously an important component in the realization of software standardization goals such as portability and interoperability. However, the issue of who has the responsibility for developing and applying conformance tests is far from settled [LEA94].
One extreme position is "Let the marketplace decide." The underlying assumption of this position is that conformance testing need not be given any formal consideration, either within the standards making process or afterwards by an independent certification or branding company/organization. Instead, the responsibility for imposing conformance to the standard is assigned to the customer: through trial and error, non-conforming products will eventually be rejected by the customer from the market place.
Figure 3. Open issue: Who will develop the conformance tests?
At the other extreme is the position that testing issues should be explicitly decided and recorded during the standards development process, and that these issues should form the basis for a test standard. The assumption in this position is that any test suite should conform to the test standard, and any product claiming conformance should be required to pass a conforming test suite.
In addition to these two extreme positions, there are various positions in between. For example, a compromise which has appeared in the IEEE POSIX community is that of considering testing related issues during the development of the standard without a formal standardization process for the testing. The intent is to develop a testable standard without the overhead of explicitly developing a standardized test specification.
This issue of who will assume responsibility for developing conformance tests has potentially significant impact on the problem of determining how to apply FSLs to conformance testing. If the standardization bodies assume responsibility, the testing standards will be subject to the same regulations and biases as the corresponding software standards. For example, the JTC 1 Directives encouraging the use of FSLs would apply for ISO standards, although the Directives recognize that a transition period to permit learning and tool support for the broad community of standards developers must be allowed. Alternately, if a group of experts in the application of FSLs accept the task of developing the tests, the use of FSLs becomes much more feasible in the near future and tool support to buffer the experts from the underlying mathematics is unnecessary. Therefore, in addressing the question of how to apply FSLs to conformance testing, the broader issue of who will be developing the conformance tests must also be considered.
Software Correctness
Software is considered correct if it meets the corresponding specification. Techniques for assessing software correctness may be broadly categorized as testing, verification and symbolic evaluation. Verification typically involves formal reasoning based on mathematical proofs. Symbolic evaluation includes techniques such as program function derivation, code inspections and walkthroughs. Testing is the most common approach to measuring software correctness, and many different approaches and techniques have evolved. There are theoretical foundations for software testing, but these academic results offer little practical assistance in the development of tests. Instead, test developers tend to rely on experience and heuristics to create test suites capable of providing some measure of confidence that a software implementation meets its specification.
An open issue which has been the subject of considerable debate within the software community concerns the level of integration of testing within the software process. A prevalent view initiated by small scale programming practices and reinforced by the classical waterfall model of software development is that testing is a separate, post-mortem activity to be considered only after coding is complete. Realizations of this view can be seen by companies with "quality assurance" teams who have little if any input
Figure 4. Open Issue: How will testing be integrated within the software lifecycle?
during the earlier stages of software development. This view is also apparent in much of the software standards community - most of the volunteers prefer to leave all consideration of testing issues to someone else after the software standard is completed. The unfortunate result is often a set of requirements in the standard which are not testable. A much more unified view of testing is emerging from the growing requirements engineering community. As this community acknowledges the critical importance of sound requirements in all phases of the software lifecycle, a specialized area of requirements based testing is also appearing . This coupling of the earliest phase of the software lifecycle with the phase considered by many to the final stage (i.e.testing) offers much support for adopting a unified view of testing.
When considering the problem of applying FSLs to conformance testing, the level of integration
of testing within the software standard lifecycle should also be addressed. For example, tool
support for testing as a post mortem activity, that is, after all standards development has been
completed, could assume a much different role than tools designed to support testing which is
developed in parallel with standards development (e.g., in the latter case, a rapid prototyping tool
to provide feedback on the testability of requirements stated in the standards might be
appropriate).
Background
Conformance Testing
Conformance testing is the process of testing software implementations claiming adherence to a standard. The outcome of a conformance test is generally a pass or fail result, possibly including reports of problems encountered during the execution. The results of a conformance test are intended to provide a measure of confidence in the degree of conformance of the implementation tested. A common problem with conformance testing is the difficulty associating a degree of confidence with a given test.
Focusing attention on conformance testing as opposed to testing in general restricts consideration to functional testing techniques (also referred to as behavioral testing, black box or requirements based testing). In functional testing, the Implementation Under Test (IUT) is subject to tests derived from the requirements only; no awareness of the structure of the IUT is assumed. This view is both practical and necessary as it would be prohibitively costly to develop a structural test for each individual implementation, and it
would be impossible to maintain a shield of impartiality on behalf of the test suite developer. Therefore, conformance testing may be viewed as a special case of functional testing which inherits the problems, policies and politics of the corresponding standards organization.
Figure 5. A Hierarchy of Conformance Testing Components.
A further restriction of the domains considered in this work is the conformance of software with behavior which can be automatically evaluated based on the state of an underlying machine. In this general view, a test specification is a collection of interfaces which alter the state of the underlying machine and one or more descriptions of expected states of the machine. The actual states of the machine during the execution of the test may be automatically compared with the expected states as described in the test specification to provide an evaluation of the conformance of the implementation.
This restriction eliminates from consideration systems which require human involvement (or possibly artificial intelligence) in determining conformance to a standard. Examples of such systems include graphics systems which require a human user to verify screen characteristics and computer-human interface standards which requires a person to evaluate properties such as "user friendliness" and "consistent appearances." The goal of a test developer is to gain as much confidence as necessary in the behavior of the system under test with a reasonable expenditure of time and money. The level of confidence required and the bounds on reasonable expenditures will vary with circumstances.
In order to make the effort manageable, the general requirement for conformance can be broken down into a collection of subgoals called hypotheses. As many test specifications as deemed appropriate are designed to support or refute each hypothesis. Note that some situations requiring a high degree of confidence may include redundant tests (i.e., tests that demonstrate the same behavior but under different circumstances) and that some hypotheses may require more than one test to demonstrate complex behavior (e.g., one test may demonstrate normal behavior and another may demonstrate exceptional behavior).
test_specification process_ids is met --The test specification -- name.
when a call on get_process_id() --A call on an interface. returns my_pid
and when a call on get_parent_process_id() --A call on an interface. returns parent_pid
and when the expression my_pid /= parent_pid holds. --A constraint on system --state.
Figure 6. A CATSII test specification. Commentary identifying the specification components is given after the double dashes.
A test suite is a collection of test specifications. A test specification may be viewed as a description of a special use, or application of the implementation designed to evaluate the implementation's behavior rather than to solve a particular problem. The conceptual componentsof a test specification are the scenario (i.e., a description of interface calls such as open, write, write, close, read, read, close), state variables to permit input and output values (e.g., the name of a file), and an expression of the expected behavior of the implementation for the given scenario and input data. The expected behavior is stated as constraints on the state variables, such as "length < MAX". These constraints are sometimes referred to as assertions since they assert one or more properties which must hold in order for the IUT to pass the test.
Figure 7. A conformance test may be viewed as a special "use" of an implementation designed to provide confidence in the correctness of the implementation rather than solve a problem with the implementation.
Formal Specification Languages
A formal specification language is a language which permits a precise, unambiguous expression of software characteristics and behavior. The basis for the precision and absence of ambiguity in the language is an underlying mathematical foundation. For example, a notation which represents a function has exactly one meaning, and this meaning may be expressed using mathematics (Figure 8.).
Formal specification languages are a component of "formal methods" which consist of a FSL, a deductive apparatus, and pragmatic guidelines [WIN90]. The deductive apparatus provides the means of formally reasoning about a system described with a FSL, and the pragmatic guidelines indicate strengths and weaknesses of the formal method, areas suited for application, and guidelines for use. Although efforts in formal methods have focused almost exclusively on formal verification techniques such as theorem proving, the use of FSLs in a less comprehensive manner has recently been advocated (also called "lightweight" formal methods). Subsequently, new areas of application for formal specification languages are being considered. One such area is that of requirements capture. In this field, FSLs and support tools are being explored as a means of understanding user requirements [HSI94]. Another general area of emerging interest and application is software testing.
a) X DY 4 {R: X GY | Ax: X; y,z: Y 2 (x,y) UR and (x,z) UR L y = z}
b) A function is a mapping of elements in a domain to a unique member of the range.
Figure 8. Functional notation and its meaning expressed using a) mathematics and b) natural language.
In trying to extend existing knowledge about FSLs to areas such as testing, an immediate observation is that there is a tremendous diversity in FSLs. This diversity is made apparent by factors such as differing syntactic notations and differing semantic domains. Taxonomies have been suggested, often along the lines of the mathematical foundations of the languages. For example, the general categories of model-based, property based and operational specification languages have often appeared in the literature, usually with the acknowledgment that a given FSL usually displays some combination of features from each of these areas.
Model-based FSLs, as exemplified by Z and VDM-SL, facilitate the development of software models using mathematical constructs such as sets and relations. Property-based FSLs permit the expression of software characteristics, and may be further categorized as axiomatic and algebraic. The foundations of axiomatic FSLs are based on Hoare's work on proofs of correctness and consist of preconditions and postconditions expressing constraints on the system state. ADL and the interface specification component of Larch are examples of FSLs based upon this approach. Algebraic FSLs are based on the expression of data types and processes defined as heterogeneous algebras. The shared language of Larch is an example of this style, in which system properties are expressed using definitional equations. An operational style of specification is a description of a system based on an underlying abstract machine. Finite state machines and Petri nets are examples of this style.
Figure 9. Illustrations of several styles of Formal Specification Languages
Test Related Language Characteristics
The characteristics selected for study are expressiveness and executability, programming language dependence, and standardization.
Expressiveness and Executablility
Expressiveness and executability are two of the most important language features to be considered in any application of formal specification languages. Executability refers to the ability of a specification to be executed on a (possibly abstract) machine, and expressiveness is the ability to communicate and reason about relevant concepts effectively. Executability places constraints on details which must be present in a representation in order to achieve translatability into machine code. Expressiveness is as much about what doesn't have to be explicitly specified as it is about what must be specified. This ability to ignore certain details is what is meant by abstraction in specification languages.
Unfortunately, these two features are in direct conflict with each other. There is a well-known fundamental trade-off between expressiveness and executability. An executable FSL is by definition limited to the specification of computable functions. By relaxing the requirement of executability, a specification language may gain expressiveness in two ways: by permitting non-computable statements (for example, universal quantification over infinite domains) and by permitting statements which omit details required for computation (for example, a predicate characterizes a set of states but imposes no order on the evaluation of components). The use of generalities supports communication and reasoning about system properties at a level of abstraction appropriate for a given problem without the clutter of irrelevant details, but this expressiveness is gained at the expense of executability.
Both capabilities play an important role in the software development process. Highly expressive languages are usually associated with the requirements development phase of the software lifecycle. Z is an example of a formal specification language often used for requirements development.
At the other extreme, executable languages are often more closely related to the implementation phase. The most common occurrence of this class of languages is programming languages, which are translated into machine code by compilers (or interpreters). Some formal specification languages may be directly executable, and this capability is often referred to as "animation". As an example, Petri nets may be animated by a graphical representation of the evolution of a given Petri net for a selected starting state. Animation provides insights into the integrity of the specifications and supports prototyping of both the specifications and tests for the specifications.
Languages which attempt to include both expressiveness and executability also exist, and are sometimes referred to as "wide spectrum" languages. VDM-SL is an example of a wide spectrum language. It includes both predicates in support of expressiveness and imperative constructs which support executability. As might be expected, compromises are included as well. The basic constructs are not as simple as those found in Z, where everything is a set. Also , only a subset of the VDM-SL language is executable.
As with software development, expressiveness and executability have associated trade-offs which must be considered when selecting a language for a given phase of testing. High level, expressive languages are useful for describing and reasoning about testing requirements while lower level languages are necessary to describe an executable representation of a test.
Programming Language Dependence
Another characteristic of formal specification languages is that of a programming language dependence. It has been noted that programming languages are formal specification languages, but that formal specification languages are not necessarily programming languages. Formal specification languages which are not programming languages are often characterized by the extent to which they are dependent upon, or similar to, a programming language. There is a wide spectrum of levels of programming language dependence, ranging from FSLs which are extensions of programming languages to FSLs which are independent of a particular programming language.
In considering the application of FSLs with programming language dependence versus those without, one immediate tradeoff which arises is that of familiarity versus generality. FSLs based on programming languages are easier for programmers to use, and a repository of established tool support typically exists as well. However, the generality of a programming language dependent specification language is limited both in use and readability to people familiar with the given programming language. A programming language dependent specification language may suffer many of the characteristics that render programming languages inappropriate for the specification of system properties (e.g., the low-level details of programming languages inhibit reasoning about higher level concepts ).
How does the level of dependence of a FSL on a programming language relate to testing? First, there is an extensive body of experience in the development of conformance tests with programming languages, and relatively little else. Therefore, we might expect that FSLs with a strong programming language dependence might ease the transition into the use of FSLs. However, there is also a long list of difficulties with current approaches to conformance testing, and the underlying means of expression (i.e., programming languages) should be carefully evaluated with respect to their potential contributions to this unhappy state.
ADL and Anna are two examples of FSL which are extensions of programming languages (C and Ada respectively). At the other extreme is a family of FSLs exhibiting complete independence from programming languages and even the traditional, imperative style of programming (e.g., Z) . A compromise is seen in the FSL Larch. Larch places the semantics of operations in a programming language independent language (the Larch Shared Language) and then provides an interface to the operations in a language reflecting characteristics of the target programming language. This design allows both the reuse of underlying semantics as well as a bridge to the target programming language. For an example of both Larch and Z, the reader is referred to Wing's paper "A Specifier's Guide to Formal Methods" where each language is used in the specification of a symbol table [WIN90].
A compromise of a different sort is seen in the CATSII language. This language was designed to retain the procedural style of imperative programming languages while abstracting away from programming level details (e.g., variable declarations). The CATSII design provides an interesting contrast to the design of ADL, which may be characterized as a programming language dependent FSL which is based on declarative rather than imperative specifications.
Standardization
A formal specification language is a language standardized by a formal process through a recognized standards organization such as IEEE, ANSI, or ISO. These standards are often characterized as "consensus based" since the process is based on the generation of an agreement among interested members of the software community. In general, the standardization of a formal specification language offers many advantages to potential users or developers, since a standard:
* indicates maturity of the language,
* represents significant community commitment,
* forms a stable base for competitive tool support from multiple vendors, and
* offers a well-defined forum for contributions and influence.
However, standardization is often a very slow process. Because of the effort involved with developing a standard, leading edge efforts often bypass this process and develop languages designed to meet a particular need.
With respect to testing, standardized FSLs form a stable basis for evaluation and study. However, the standardized FSLs have not been developed to directly support the testing process. Furthermore, there is an attitude among many of the software community that testing is inferior, not exciting, etc. Therefore, it is often difficult to gain the volunteer participation required to develop a test-related standard.
Examples of standardized formal specification languages include Petri Nets, LOTOS, Z and VDM-SL. The FSL Petri Nets is being standardized by the standards group ISO/IEC JTC1/WG11. The FSL Petri Nets is a generalization of automata theory in that concurrency is included. Petri Nets have typically been applied to the domain of protocol testing. Substantial tool support for Petri Nets exists which offers capabilities such as graphical viewing and editing of nets as well as simulation (or animation) of the system properties. Cabernet is one such tool which was recently introduced. This tool provides the capabilities mentioned in addition to a hierarchical manager which allows navigation of nets in varying levels of abstraction.
The formal specification LOTOS (Language Of Temporal Ordering Specification) is an ISO standard applied to the design of protocols and distributed systems. LOTOS is based on Milner's calculus of communicating systems (CCS) and on the ACT ONE abstract data type formalism. Tools exist and are being developed that support the execution of LOTOS specifications, thereby permitting the specifications to be validated against the system requirements.
Z and VDM-SL are also ISO standards with many similarities. Both are used to describe sequential software systems through the development of system models. They also both have extensive tool support and have been widely used in industry. VDM-SL has been used to provide a formal semantics for the programming language Modula-2.
Applications of Formal Specification Languages to Conformance Testing
This section examines how the problems associated with conformance testing may be addressed by the use of formal specification languages. One observation used as a guideline in this study is that parallels between software development and conformance testing may be exploited to accelerate the application of formal specification languages in conformance testing. For example, both software and test development have an associated lifecycle, including requirements analysis, design, implementation and validation. Therefore, as various formal specification languages have taken on different roles to support different stages of the software lifecycle, so might a similar paradigm emerge for testing.
Another observation is that the role of natural and formal specification languages is complementary rather than adversarial in both software and test development. An example is the complementary role of programs (based on formal specification languages) and associated documentation (based on natural language). Since programming languages are themselves a subset of formal specification languages (Figure 9.), the issues surrounding the application of formal specification languages to both software and test development are best phrased as " How can formal specification languages be extended to all phases of the software (or testing) lifecycle?" rather than "Can formal specification languages be used in the software (or testing) lifecycle?"
The study of applications of formal specification languages to conformance testing is presented in two levels of coverage. First, an overview of the general areas of potential application of formal specification languages in conformance testing is given along with examples from both software development and conformance testing. The next section provides an in depth analysis of two state of the art testing systems based on formal specification languages. In this analysis, both strengths and weaknesses are presented as well as examples of specifications.
Three general areas of application of formal specification languages in conformance testing are considered. Enhanced reasoning capabilities, tool support and environment development are each discussed as potential candidates for the application of formal specification languages. Each is presented in terms of its basic purpose, sample applications of formal specifications in software development, potential applications in conformance testing, and actual applications in state of the art conformance testing systems.
Enhanced Reasoning Capabilities
Reasoning involves the representation and manipulation of knowledge at an appropriate level of abstraction in order to effectively comprehend explicit facts as well as to make inferences about implicit information. In most real world problems, reasoning is required at many levels of abstraction during the development of a solution. Natural language facilitates some measure of reasoning by humans, but suffers from ambiguity and a lack of precision. Programming languages facilitate a computer implementation of the solution, but as a consequence they also include many computation related details which restrict the level of abstraction to that appropriate for computation. These shortcomings motivate the need to formally represent characteristics and properties at levels of abstraction higher than programming languages.
Formal specification languages have addressed these shortcomings in software development by abstracting away from programming details while retaining a precision of semantics unattainable with natural languages. An example is the formal specification language Z , which is often used in the requirements phase to develop models of systems using sets as the basic construct. Each of these examples illustrates the ability of formal specification languages to focus on the semantics of the system under consideration independent of implementation details.
In conformance testing, as in software development, constructs to facilitate reasoning must be considered both for small scale and large-scale efforts. Testing in the small requires reasoning about the development of a single test specification and perhaps about the collective semantics of a small number of test specifications. One simple means of facilitating reasoning at this level is that of keywords selected especially to reflect testing concepts. Keywords serve as both a guideline in the development process and as a sort of documentation to assist reviewers of the test specifications. The use of keywords might also facilitate tool support, such as the automatic identification of interfaces participating in various roles (as defined by the keywords) to assist coverage analysis.
Automated Testing Tools
Software tools may be categorized as software implementations of labor intensive tasks designed to reduce the effort required by humans. In software development, the use of formal specification languages supports the development of tools such as compilers, semantic analyzers, theorem provers and model checkers.
Unlike test specification languages, tool support for testing has received considerable attention in the past decade. The phrase "automated testing" has been broadly used to indicate the automation of any portion of any testing process. Therefore, a variety of automated tools are present supporting areas unrelated to conformance testing, such as structural coverage tools or regression testing tools. In many respects, the phrase has had somewhat unfortunate connotations in conformance testing, since test design for complex systems is usually an inherently creative process which is typically not completely automatable.
The need for tools to support the translation of test specifications into executable tests is based upon the need for formal testing specification languages other than programming languages (e.g., a formal specification language designed to support reasoning about
test specification dir_ops is met
when a call on get_allowed_process_permissions()
returns perms successfully
and when a call on create_directory("new_dir", perms) returns <>
and e_code contains the error condition
and when a call on is_directory("new_dir") returns new_dir_status successfully
and when the expression new_dir_status = 1 holds
and when a call on remove_directory("new_dir") returns <> successfully
and when a call on is_directory("new_dir") returns new_dir_status successfully
and when the expression new_dir_status = 0 holds.
a)
get_allowed_process_permissions perms;
create_directory "new_dir" perms ;
is_directory_p "new_dir" new_dir_status;
remove_directory "new_dir";
b)
Figure 10. An illustration of a specification which is translatable into executable code. a) A test specification written according to the CATSII grammar which checks to see if a directory is successfully created and deleted. b) The translated code which is executable by an abstract machine (the CATS harness).
tests). A general concern for tools based on formal specification languages is the practicality of using the tools. In the recent paper by Clark and Wing describing the state of the art in formal methods, they indicate that a criterion for the ease of use of tools is that they should be as "easy to use as a compiler". An emphasis for improvement in this area is the development of translators to generate executable tests which are as easy to use as compilers for programming languages.
Test Development Environments
Environments may be described as software programs designed to assist a human in understanding the complexity of a given situation. An example of an environment in software development which is based on the use of formal specification languages is the prototyping environment provided by the direct execution of some styles of specifications (e.g., Petri Nets). The structure imposed by formal specification languages also allows enhanced navigation capabilities, such as those provided by tools such as Cabernet and the VDM Toolbox. Existing test environments such as test harnesses (also called test scaffolds) provide minimal support routines to assist the testing process. Examples of test harness functionality include assistance with the compilation and execution of tests as well as analysis support such as predefined test metrics.
Executable specifications assist the testing process by providing a way of prototyping and validating the tests, i.e., a way to determine that a test is consistent with the specification . If the specifications are executable, a prototype test can be executed on the specifications. If the test specification does not pass when applied to the software specification, it is an invalid test.
Possible advances in test development environments based on the use of FSLs include enhanced navigation, prototyping and visualization capabilities [STE87], [POT91]. For example, a well defined hierarchy of abstractions, as established by a FSL, provides a sound basis for browsing through different levels of test expressions (e.g., families of related test specifications, all preconditions predicated upon a selected variable). A browser capable of automatically generating coverage maps at the differing levels of abstraction would be helpful in the development of effective coverage strategies.
A prototyping facility would enable a test designer to get rapid feedback on the quality of the tests as they are being developed. Many FSLs are executable and thus provide a basis for prototyping. FSLs such as Petri nets and finite state machines have a well-established capability for "animating" specifications. An animation is an execution of the specification typically accompanied by a graphical display of state changes.
Finally, the visualization of large quantities of data to assist understanding is an area of great potential. Since one of the fundamental problems with testing is the selection of strategies and data from huge numbers of choices, visualization offers one means for humans to grasp and manage the associated complexity.
Conclusion
Formal specification languages offer many of the same advantages in the development of conformance tests as found in the development of software. Specifically, they offer a broad range of expressiveness and they are amenable to machine manipulation. The ability to select the appropriate level of abstraction supports reasoning about large and complex test designs, and machine manipulation supports the development of labor reducing testing tools and environments. However, while software development may be viewed as a process of creation, conformance testing is best viewed as a special use of an implementation intended to provide confidence in the correct behavior of the implementation. As such, the potential contributions of formal specification languages in conformance testing lie in the definition of test scenarios (which define how an implementation is used), a precise description of scenario semantics (which defines how a correct implementation should behave for the given scenario) and computer assisted support (such as the automated comparison of the actual behavior of an implementation with the expected behavior).
The effective testing of artifacts in any engineering discipline requires techniques and tools designed especially to support the testing process, and conformance testing of software is no exception. A general observation regarding difficulties associated with software testing is that the software community has failed to address testing as a first class citizen. Instead, languages and tools primarily intended to support software development have been applied to software testing with dismal results. The emergence of formal specification languages into realms other than verification offers a unique opportunity to re-evaluate the requirements of testing as an important component of the software lifecycle in its own right. A key to exploiting the use of formal specification languages in conformance testing is to gain insight from the parallels found in their application to software development while acknowledging the differences between software development and software testing.
References
M. Gray and K. Liburdy, "Testers Open Dialogue at Inaugural NIST Workshop", IEEE Software, The Institute of Electrical and Electronics Engineers, September 1994.
P. Hsia, J. Samuel, J. Gao, D. Kung, Y. Toyshima and C. Chen, "Formal Approach to Scenario Analysis", IEEE Software, 1995, March 1994.
J. Leathrum and K. Liburdy, "The Role of Testing Methodologies in Open Systems Standards", International Conference on Software Engineering, 1994.
P. Pulli, M. Heikken and R. Lintulampi, "Graphical Animation as a Form of Prototyping Real-Time Software Systems", Real-Time Systems, 5, 173-195, 1993.
S. Stepney and S. Lord, "Formal specifications of an access control system", Software - Practice and Experience, 17(9):575-593,1987. An early account of animating a Z specification using Prolog.
J. Wing, "A Specifier's Introduction to Formal Methods", IEEE Computer, 23(9):8-24 September 1990.