Software Engineering-Formal Methods Concepts


The aim of this section is to present the main concepts involved in the mathematical specification of software systems, without encumbering the reader with too much mathematical detail. To accomplish these, we use a few simple examples.

Example 1: A Symbol Table. A program is used to maintain a symbol table. Such a table is used frequently in many different types of applications. It consists of a collection of items without any duplication. An example of a typical symbol table is shown in figue. It represents the table used by an operating system to hold the names of the users of the system. Other examples of tables include the collection of names of staff in a payroll system, the collection of names of computers in a network communications system, and the collection of destinations in a system for producing railway timetables.

Assume that the table presented in this example consists of no more than MaxIds members of staff. This statement, which places a constraint on the table, is a component of a condition known as a data invariant.

A data invariant is a condition that is true throughout the execution of the system that contains a collection of data. The data invariant that holds for the symbol table just discussed has two components: (1) that the table will contain no more than MaxIds names and (2) that there will be no duplicate names in the table. In the case of the symbol table program, this means that, no matter when the symbol table is examined during execution of the system, it will always contain no more than MaxIds staff identifiers and will contain no duplicates.

Another important concept is that of a state. In the context of formal methods, a state is the stored data that a system accesses and alters. In the example of the symbol table program, the state is the symbol table.

The final concept is that of an operation. This is an action that takes place in a system and reads or writes data to a state. If the symbol table program is concerned with adding and removing staff names from the symbol table, then it will be associated with two operations: an operation to add a specified name to the symbol table and an operation to remove an existing name from the table. If the program provides the facility to check whether a specific name is contained in the table, then there would be an operation that would return some indication of whether the name is in the table.

An operation is associated with two conditions: a precondition and a postcondition. A precondition defines the circumstances in which a particular operation is valid. For example, the precondition for an operation that adds a name to the staff identifier symbol table is valid only if the name that is to be added is not contained in the table and also if there are fewer than MaxIds staff identifiers in the table. The postcondition of an operation defines what happens when an operation has completed its action. This is defined by its effect on the state. In the example of an operation that adds an identifier to the staff identifier symbol table, the postcondition would specify mathematically that the table has been augmented with the new identifier.

Example 2: A Block Handler. One of the more important parts of a computer's operating system is the subsystem that maintains files created by users. Part of the filing subsystem is the block handler. Files in the file store are composed of blocks of storage that are held on a file storage device. During the operation of the computer, files will be created and deleted, requiring the acquisition and release of blocks of storage. In order to cope with this, the filing subsystem will maintain a reservoir of unused (free) blocks and keep track of blocks that are currently in use. When blocks are released from a deleted file they are normally added to a queue of blocks waiting to be added to the reservoir of unused blocks. This is shown in figure. In this figure, a number of components are shown: the reservoir of unused blocks, the blocks that currently make up the files administered by the operating system, and those blocks that are waiting to be added to the reservoir. The waiting blocks are held in a queue, with each element of the queue containing a set of blocks from a deleted file.

For this subsystem the state is the collection of free blocks, the collection of used blocks, and the queue of returned blocks. The data invariant, expressed in natural language, is
No block will be marked as both unused and used.
All the sets of blocks held in the queue will be subsets of the collection of currently used blocks.
No elements of the queue will contain the same block numbers.
The collection of used blocks and blocks that are unused will be the total collection of blocks that make up files.
• The collection of unused blocks will have no duplicate block numbers.
• The collection of used blocks will have no duplicate block numbers.

Some of the operations associated with these data are
An operation that adds a collection of blocks to the end of the queue.
An operation that removes a collection of used blocks from the front of the queue and places them in the collection of unused blocks.
An operation that checks whether the queue of blocks is empty.

The precondition of the first operation is that the blocks to be added must be in the collection of used blocks. The postcondition is that the collection of blocks must be added to the end of the queue.

The precondition of the second operation is that the queue must have at least one item in it. The postcondition is that the blocks must be added to the collection of unused blocks.

The final operation—checking whether the queue of returned blocks is empty— has no precondition. This means that the operation is always defined, regardless of what value the state has. The postcondition delivers the value true if the queue is empty and false otherwise.

Example 3: A Print Spooler. In multitasking operating systems, a number of tasks make requests to print files. Often, there are not enough printing devices to satisfy all current print requests simultaneously. Any print request that cannot be immediately satisfied is placed in a queue awaiting printing. The part of an operating system that deals with the administration of such queues is known as a print spooler.

In this example we assume that the operating system can employ no more than MaxDevs output devices and that each device has a queue associated with it. We will also assume that each device is associated with a limit of lines in a file which it will print. For example, an output device that has a limit of 1000 lines of printing will be associated with a queue that contains only files having no more than 1000 lines of text. Print spoolers sometimes impose this constraint in order to forbid large print jobs that may occupy slow printing devices for exceptionally long periods. A schematic representation of a print spooler is shown in figure.

Referring to the figure, spooler state consists of four components: the queues of files waiting to be printed, each queue being associated with a particular output device; the collection of output devices controlled by the spooler; the relationship between the output devices and the maximum file size that each can print; and the relationship between the files awaiting printing and their size in lines. For example, figure shows that the output device LP1 which has a print limit of 750 lines has two files ftax and persons awaiting printing, and that the size of the files are 650 lines and 700 lines, respectively.

The state of the spooler is represented by the four components: queues, output
devices, limits, and sizes. The data invariant has five components:
Each output device is associated with an upper limit on print lines.
Each output device is associated with a possibly nonempty queue of files awaiting printing.
Each file is associated with a size.
Each queue associated with an output device contains files that have a size less than the upper limit of the output device.
There will be no more than MaxDevs output devices administered by the spooler.

A number of operations can be associated with the spooler. For example,
An operation that adds a new output device to the spooler together with its associated print limit.
An operation that removes a file from the queue associated with a particular output device.
An operation that adds a file to the queue associated with a particular output device.
An operation that alters the upper limit of print lines for a particular output device.
An operation that moves a file from a queue associated with an output device to another queue associated with a second output device.

Each of these operations corresponds to a function of the spooler. For example, the first operation would correspond to the spooler being notified of a new device being attached to the computer containing the operating system that administers the spooler.

As before, each operation is associated with a precondition and a postcondition. For example, the precondition for the first operation is that the output device name does not already exist and that there are currently less than MaxDevs output devices known to the spooler. The postcondition is that the name of the new device is added to the collection of existing device names, a new entry is formed for the device with no files being associated with its queue, and the device is associated with its print limit.

The precondition for the second operation (removing a file from a queue associated with a particular output device) is that the device is known to the spooler and that at least one entry in the queue is associated with the device. The postcondition is that the head of the queue associated with the output device is removed and its entry in the part of the spooler that keeps tracks of file sizes is deleted.

The precondition for the fifth operation described (moving a file from a queue associated with an output device to another queue associated with a second output device) is
The first output device is known to the spooler.
The second output device is known to the spooler.
The queue associated with the first device contains the file to be moved.
The size of the file is less than or equal to the print limit associated with the second output device.

The postcondition is that the file is removed from one queue and added to another queue.

In each of the examples noted in this section, we introduce the key concepts of formal specification. But we do so without emphasizing the mathematics that are required to make the specification formal. In the next section, we consider these mathematics.
Share this article :
 
Copyright © 2012. Best Online Tutorials | Source codes | Programming Languages - All Rights Reserved