Overview

This example briefly demonstrates the process of formalizing a given specification for the purpose of generating test descriptions, referred to as test frames, and the generation of test frames.

The automatic test frame generation portion of this example is from the Ph.D. research of Michael Donat.

Other more detailed examples are also available:

• Applying an Automated Test Description Tool to Testing Based on System Level Requirements
• Automatically Generated Test Frames from an S Specification of Separation Minima for the North Atlantic Region
• Automatically Generated Test Frames from a Q Specification of ICAO Flight Plan Form Instructions

This example also demonstrates the difference between formalizing a specification and modelling it. For this example, generating test frames requires only that the logical relationships between conditions be formalized. Therefore, modelling the requirements at a deeper level of detail is unnecessary (for the purpose of generating test frames).

The Requirements

The requirements for this example are for a simple boiler vessel. The system is to monitor certain aspects of the vessel and be consistent with the following requirements:

1. If the vessel temperature is above 514 degrees C, the vessel pressure is above 78 PSI, or the vessel temperature is above 480 degrees C and the vessel pressure is above 52 PSI, then the vessel state shall be CRITICAL.
The heat source for the vessel shall be extinguished upon receipt of a "shutdown" command from the operator or when the vessel state becomes CRITICAL.
An alert shall be signalled to the operator when the vessel state becomes CRITICAL or when a sensor malfunction is detected.
The operator is procedurally required to notify the control system that he is actively monitoring the system at least once every five minutes whenever the vessel is being heated or the vessel is in a CRITICAL state.
If an operator notification has not been received within the last five minutes when operator notifications are required, then a warning shall be signalled to the operator.
If a warning is not acknowledged within 30 seconds of being signalled, then the heat source for the vessel shall be extingished.

The Formal Specification

We distinguish a formal specification from a model. A formal specification typically contains a small amount of formal detail, such as the specification below. For example, the condition "the vessel is being heated" presents no formal model about what it means to be a vessel, or how heat affects a vessel. It is simply either true or false. The interpretation of this condition is the responsibility of the test engineer. In contrast, a model of a set of requirements typically contains a great deal of formal detail, such as a mathematical representation of the temporal aspects of the above requirements. A formal specification evolves into a model as more formal detail is added.

A formal specification, in S, of the above requirements is (vessel.s):

%include startup.s

temp, pressure : num;
critical : bool;

R1 :=
	if temp > 514 \/ pressure > 78
		\/ (temp > 480 /\ pressure > 52)
	then critical;

"Receipt of shutdown" : bool;
"extinguish heat source" : bool;

R2 :=
	if "Receipt of shutdown" \/ critical
	then "extinguish heat source";

"Sensor malfunction" : bool;
"alert signalled to the operator" : bool;

R3 :=
	if critical \/ "Sensor malfunction"
	then "alert signalled to the operator";

"The vessel is being heated" : bool;
"operator is procedurally required to notify the
	control system that he is actively monitoring the system at
	least once every five minutes" : bool;

R4 :=
	if "The vessel is being heated" \/ critical
	then
	"operator is procedurally required to notify the
	control system that he is actively monitoring the system at
	least once every five minutes";

"Operator notifications are required" :=
	"The vessel is being heated" \/ critical;

"An operator notification has not been received
	within the last five minutes" : bool;
"warning signalled to operator" : bool;

R5 :=
	if "An operator notification has not been received
			within the last five minutes" /\
		"Operator notifications are required"
	then "warning signalled to operator";

"A warning is not acknowledged within
	30 seconds of being signalled" : bool;

R6 :=
	if "A warning is not acknowledged within
		30 seconds of being signalled"
	then "extinguish heat source";

Vessel := R1 /\ R2 /\ R3 /\ R4 /\ R5 /\ R6;

The definition of Vessel represents the formalization of the given requirements.

Automatically Generated Test Frames from a Formal Specification

Test frames are produced from a formal specification by identifying which conditions are responses of the system (indicated by a predicate beginning with a lower case letter) and which are stimuli. They are then re-assembled into a set of test classes. A set of test frames is generated for each test class.

Test frames for the formal specification can be produced using the TCG tool and are shown below. The HTML for this page was generated with the command

Test Class 1

temp > 514 \/ pressure > 78 \/ temp > 480 /\ pressure > 52 ==> critical

--Test Frame 1:

--Test Frame 2:

--Test Frame 3:

Test Class 2

"Receipt of shutdown" \/
  "A warning is not acknowledged within 30 seconds of being signalled" ==>
  "extinguish heat source"

--Test Frame 1:

--Test Frame 2:

Test Class 3

temp > 514 \/ pressure > 78 \/ temp > 480 /\ pressure > 52 ==>
  "extinguish heat source" /\
    "alert signalled to the operator" /\
      "operator is procedurally required to notify the
	control system that he is actively monitoring the system at
	least once every five minutes"
  

--Test Frame 1:

--Test Frame 2:

--Test Frame 3:

Test Class 4

"Sensor malfunction" ==> "alert signalled to the operator"

--Test Frame 1:

Test Class 5

"The vessel is being heated" ==>
  "operator is procedurally required to notify the
	control system that he is actively monitoring the system at
	least once every five minutes"
  

--Test Frame 1:

Test Class 6

"An operator notification has not been received within the last five minutes" /\
  "The vessel is being heated" \/
  "An operator notification has not been received within the last five minutes"
    /\ (temp > 514 \/ pressure > 78 \/ temp > 480 /\ pressure > 52) ==>
  "warning signalled to operator"

--Test Frame 1:

--Test Frame 2:

--Test Frame 3:

--Test Frame 4: