The article describes the approach how to transform initial requirements in natural language into the formal requirement model. The model is used to analyze the behavior of the designed system to meet the original requirements during the design stage. Successfully verified the formal requirement model is used to generate test cases that completely cover the behavior of the analyzed application.
The issue of verifying implementation of large-scale and complicated requirements specification is among the main issues of industrial software development and test automation. Documents with requirements specification are usually formulated in natural language and may contain hundreds and thousands of requirement items. Therefore requirements formalization for describing behavioral scenarios used for automated tests or manual test procedures development is characterized as a task of huge complexity and big efforts.
Applicability of formal methods in the industry is largely determined by the level
of formalization language adequacy to the engineering practice involving not only
code developers and testers but also customers, project managers of different levels,
marketers and other specialists. Quite obvious that none of the logical languages can
be used for adequate requirements formalization which would keep the semantics of
the developed application and at the same time satisfy all «persons involved» [
In contemporary project documentation initial requirements are formulated either constructively, when scenario of requirement fulfillment checking can be extracted directly from the text of this requirement in natural language, or unconstructively, when there is no clarification how to check some feature contained in the requirement.
For example, behavioral requirements for telecommunication applications are formulated constructively given that requirements execution procedure is specified, and in this case verification and testing can be used to check their feasibility. Non behavioral requirements are often formulated unconstructively, which requires some additional information in formalization process allowing to work out scenarios of their checking or in other words to transform unconstructive way of formulation into constructive one. 2
Procedure of a requirement checking is exact sequence of causes and consequences of some activities (encoded by actions, signals and states), whose analysis allows to confirm whether this requirement has been fulfilled or not. Such checking procedure being used as criteria of requirement fulfillment can be called criteria procedure. The term "sequence" or "chain of events" will be used along with the term “criteria procedure” in the text of this article.
Tracking the steps of performing criteria procedure in system’s behavioral scenario (either hypothetical or implemented in a model or in a real system) can be served as confirmation that the corresponding requirement is fulfilled in the system under analysis.
Procedure of a requirement checking (a chain) is formulated by specifying the
following information for all elements of this chain:
• conditions (a set of causes) required for activation of some activity;
• the activity, which shall be executed under current conditions;
• consequences - observable (measurable) results of activity execution.
All the following is used to specify causes and consequences: signals, messages or
transactions, commonly used in communications between instances of reactive
systems [
Issues with unconstructive formulating of requirements are solved in the process of procedures development that should check requirements fulfillment on user interfaces or interfaces between components. It means that the requirement for some functionality should be interpreted by functions of user interface or API (Application Program Interface) of components. These functions should describe the encoded functionality in such a way that, based on this interpretation, you can set the procedure for checking the corresponding functionality in the application.
Similar interpretation is formulated in Use Case [
Thus, chains with sequences of activities and states can be used as criterion of requirements fulfillment. Besides that, there may be cases in which the criterion for the fulfillment of a certain requirement is specified by several chains instead of a single chain. 3
The following types of documentation are usually used while formulating technical requirements in industrial software projects: • Marketing Requirement Specification (MRS) – enumeration of new functionality from customer's point of view, often described in Use Case format; • Technical Requirement Specification (TRS) – enumeration of complete functionality to be implemented with brief explanation of each function; • Functional Requirement Specification (FRS) – detailed description of complete functionality to be implemented, full enough for test set creation to test software product on all stages of the lifecycle.
Each requirement in these documents is more often formulated in natural language and expressed in one of two ways: • as behavioral requirement, when scenario of requirement fulfillment checking can be extracted directly from the text of this requirement in natural language; • as non behavioral requirement, when just a structure or wish of having some feature is expressed without explanation of how this feature can be checked or tested. Due to constructive way of expression behavioral requirements allow static and/or dynamic methods of verification and testing for checking their implementation.
Non behavioral requirements are expressed in unconstructive way and require additional information for creating a constructive scenario of their checking in order to make verification and testing applicable.
Formalization of any constructively formulated requirement as well as effective
automated analysis of software requirements are possible and implemented in VRS/TAT
technology [
Use Case Maps (UCM) notation [
UCM notation is clear for a designer, a tester and a customer. It allows describing
behavior of complex software projects in a formal way. Although a transition from
informal requirements to their formal model is performed manually, it can be
significantly simplified by using developed solutions based on templates. The rest stages of
VRS/TAT verification and testing integrated technology are automated [
Considered below are the stages of requirements processing on the example of
Extensible Messaging Presence Protocol (XMPP) implementation project. XMPP [
This paper illustrates integrated methodic for formalizing initial requirements and creating requirements formal model which can be applied after detailing for symbolic verification and generation of symbolic test scenarios and further executable test sets. Functioning XMPP server called Apache Vysper is used as a system under test (SUT) in this project.
Example fragment of XMPP initial requirements version is shown in Fig. 2:
Each requirement in Fig. 2 has a corresponding criteria chain or a test procedure (Fig. 3). Test procedure contains pre- and post- conditions as well as actions for covering the requirement.
For example, the ReqXMPP0003 requirement: «Server must allow sending/receiving messages between clients» has the corresponding TestProсXMPP0003 test procedure which covers this requirement.
Pre-condition: Clients have been initialized on the server.
Step 1. The first client sends a message to the second client.
Step 2. The server confirms message dispatch.
Step 3. The second client receives the message from the first client.
Post-condition: The message has been successfully delivered.
UCM diagram is used in the project as a requirements model. UCM diagram shown in Fig. 4 describes communication between XMPP server and XMPP client.
The trace marked with green color on the diagram corresponds to the TestProcXMPP0003 test procedure.
Note that requirement fulfillment can be traced by its steps: 1. Four events Login1, Login2, Confirm_Login1 and Confirm_Login2 (both clients logging in to the server and get confirmation from the server) altogether compose a precondition for the send_message event - sending a message from the first client to the second client (Precondition: Clients have been initialized on the server). 2. The confirm_send event is the server's confirmation of message dispath. 3. The consume_message event means that the second client has successfully received the message and post-condition has been achieved: the message has been successfully delivered. The fact, that the EndPoint1 point has been reached, means the end of the test procedure and successful fulfillment of the ReqXMPP0003 requirement.
A scenario generated from a formal model in UCM format and corresponding to the
test procedure can be automatically presented as a symbolic test scenario in MSC
[
If criteria chains checking requirements fulfillment are formulated and agreed with customer for all requirements, it provides criteria for functionality checking of the whole software product.
Checking criteria chains for each constructive requirement means checking its semantics from customer’s point of view, of course only after all criteria procedures had been approved by the customer. Implementation of such check is rather complex task if it is not fully automated.
UCM models of requirements may have complicated structured view (Fig. 6). For example, UCM model of the ReqXMPP0007 requirement: «Server must allow client to unsubscribe other client at any time» is represented in Figure 6 and contains encapsulated UCM diagram.
The test procedure corresponding to the ReqXMPP0007 requirement model contains joint sequence of events from both diagrams in its behavioral scenario (Fig. 7):
Symbolic MSC scenario uses signals with identification parameters of the jid1
and jid2 communicating clients, i.e. the described behavior can be spread on a number
of clients. Allowed restrictions on region of admissible values for any parameter shall
be controlled by means of static and dynamic control [
Means of automated model correctness checking are provided by VRS/TAT [
The criterion of error in the specification of the requirement is the fact that the criteria chain is unreachable and this fact is detected during the verification process (Fig. 8). The reason of test scenario unreachability (or failing) detected during verification process lies in incorrect formulation of the ReqXMPP0016 requirement (Fig.9). The problem is that it is not enough to enter a room to be allowed to send messages in this room. In other words, an invitation received by a user shall not give him rights to use this room.
The corrected ReqXMPP0016 requirement is the following: «Client who received invitation to enter a room but didn’t enter a room can’t send messages to this room. Server shall response to the client with «error» message».
Changes in the semantics of requirement lead to corresponding correction of UCM model (Fig. 9), where the ReqXMPP0016 requirement is reachable.
Covered requirements are displayed on UCM model with colored path. There can be individual color for each requirement which is very useful for coverage analysis or model correction.
Providing the full coverage of all requirements implies proving the correctness of all behavioral scenarios kept in requirements. However this does not guarantee absence of some incorrect (not specified in requirements) behavior which can be a result of the environment not considered in behavioral model.
The described approach provides features of automated analysis of incorrect
behavior conditions [
The proposed approach was tested in industrial telecommunications projects of the Motorola Saint-Petersburg department of software development and allowed to automate the process of designing and developing functional tests. Due to automation it was possible to reduce the complexity of this process more than 5 times, while ensuring the guaranteed completeness of testing. 8
The proposed approach has the following advantages:
• Usage of formal methods is a good practice to guarantee the software quality.
• High abstraction level of formal model allows working with customer on the
development phase. It provides proving the model’s behavior correctness.
• Analyzing the behavior of all functionality modes mapped to requirement
specifications.
• Calculate permissible range of parameters used in the behavioral scenarios.
• For application or tests source code generation a detailing (technique of Lowering
[
Acknowledgments. The results of this work were obtained using ccNUMA system and RSC Tornado cluster in Supercomputer Center of Peter the Great St. Petersburg Polytechnic University. The work was financially supported by the Ministry of Education and Science of the Russian Federation in the framework of the Federal Targeted Programme for Research and Development in Priority Areas of Advancement of the Russian Scientific and Technological Complex for 2014-2020 (№ 14.584.21.0022, ID RFMEFI58417X0022).