Requirements Formalization and Test Suite Production Process
The production process used at the Linux Verification Center to develop tests includes the following main stages:
- Decomposition of the standard into groups of related functions.
- Analysis of the standard and extracting requirements for every group of functions.
- Formalization of the requirements to check for.
- Development of the test action scenarios for every group of functions.
- Automatic generation of tests by CTesK tools.
At the stage of standard decomposition, all the interfaces described in the standard are divided into groups of functions that are logically related. Every such a group usually consists of functions and data types related to a certain set of operations and is closed relative to reversion of operations. For example, the functions for opening and closing a file, creating and removing objects should be placed into the same groups. We have divided the 1532 functions of the LSB Core 3.1 standard into 169 function groups.
All the other stages are executed within the selected groups of functions, though usually with stage intersection. Clear distinction of the stages in this document is for simplification purposes. The workflow of the main stages for a function group is shown on the fig.1:
Fig. 1. Process of conformance tests development (simplified).
The stage of analysis of the standard and extraction of requirements lies in thorough reading of the standard text to identify atomic requirements. Usually, there are from single requirement to several dozens requirements extracted for each function. An identifier is assigned to every requirement. As a result of the analysis, a catalog of requirements is created, which represents a table of requirements in the form of {standard, identifier, text of requirement} (example for mkdir function). In addition to the plain list of requirements, we have found interesting to represent the catalog in the form of marked up HTML text of the standard, where each requirement is highlighted in color.
The stage of requirements formalization starts with choosing particular requirements to check. This is necessary because far from all requirements of the standard can be tested. The Standard IEEE Std 2003.1 for methods of POSIX testing emphasizes the following reasons why a requirement of a standard can be not checked:
- there are no known methods for checking the requirement;
- the requirement is not formulated clearly enough;
- checking the requirement needs unreasonably high efforts.
Extracted requirements are transformed into formal specifications in SeC language – Specification extension of C language. Each operation is described by means of pre- and post-conditions. Pre-condition of the operation defines its definitional domain. Post-condition defines the restrictions on the results of the operation's work and on the resultant state of the system, depending on the values of its input parameters and the previous system state before calling the operation. For data types and data elements, we define restrictions of consistency called invariants. Usually, a single file is created for each function group where specification of the system state model and all the necessary specifications for the functions of the group are defined (example of the specification file for the math.integer group). One should note that the checks in specifications contain explicit references to the corresponding requirements in the text of the standard – this assures traceability of the specification to the standard, and also allows generating reports about test coverage and discrepancies found in terms of original requirements.
At the stage of test scenarios development the formal specifications of the requirements are supplemented by scenarios of test actions. A test scenario specifies the sequence of test actions for the system being tested. A call to a certain interface function with specific parameters is implied by a test action. The scenario may define both static chain of actions and a finite state machine that models the behavior of the component being tested in such a manner that executing all of the branches guarantees coverage of 100% of situations according to the criteria chosen. The machine is defined by means of a function calculating the state, and a set of possible actions for each state. This set of actions depends on the state. Using state machines in describing the scenario allows getting thorough test coverage with controlled deepness by low efforts.
And at last, the stage of generating the tests lies in using the CTesK tools for automated building the test suite based on formal specifications and test scenarios. Using such an approach allows ensuring the conformance between the specifications and the tests. Besides, separate description of specifications and test scenarios facilitates tests modifications as requirements are updated and simplifies scaling of completeness and thoroughness of testing. This is very important for effective use and maintenance of the tests including their use on different target platforms and/or adaptation to specific requirements.
More detailed description of the test architecture as well as technical aspects of formalizing the requirements, creating specifications and tests can be found in the document "Specification-Based Testing: Getting Started" 
.
Extended process of developing tests
One should note an important aspect that defects in the text of the standard become most apparent during the analysis of the standard when extracting requirements and formalizing them. These defects can be ambiguities, inconsistencies between statements in different parts of the standard, unintentionally inexact requirements, typos, incomplete description of the functionality, etc. We register all such remarks in a tracking system for further processing – the confirmed remarks are reported to the developers of the standards for incorporating changes into future versions, which is an important result in itself.
One more important aspect is that during requirements formalization and developing test scenarios a set of parameters is defined, which is then used by the configuration and execution control system. These parameters may include both options declared in the standard and additional ones defined by developers of the specifications. Some of the configuration settings define which requirements to check, while others allow user to specify a particular variant of system behavior from several ones allowed by the standard. The others may define that some specific functionality is absent in the system at all, and the corresponding functions should not be called. Some parameters may define the possible error codes returned by the functions. And at last, an important group of parameters controls the thoroughness of testing.
The extended process of development of a test suite is shown on the fig.2:
Fig. 2. Details of conformance tests development process.