FORMAL SYSTEM SPECIFICATION

Read Time:9 Minute, 12 Second

FORMAL SYSTEM SPECIFICATION

In recent years, formal techniques have emerged as a central issue in software engineering.

This is not accidental; the importance of precise specification, modelling, and verification is recognised to be important in most engineering disciplines.

Formal methods provide us with tools to precisely describe a system and show that a system is correctly implemented.

We say a system is correctly implemented when it satisfies its given specification.

The specification of a system can be given either as a list of its desirable properties (property-oriented approach) or as an abstract model of the system (model-oriented approach).

What is a Formal Technique?

A formal technique is a mathematical method to

specify a hardware and/or software system
verify whether a specification is realisable
verify that an implementation satisfies its specification
prove properties of a system without necessarily running the system, etc.

The mathematical basis of a formal method is provided by its specification language.

More precisely, a formal specification language consists of two sets—syn and sem, and a relation sat between them.

The set syn is called the syntactic domain, the set sem is called the semantic domain, and the relation sat is called the satisfaction relation.

For a given specification syn, and model of the system sem, if sat (syn, sem), then syn is said to be the specification of sem, and sem is said to be the specificand of syn.

The generally accepted paradigm for system development is through a hierarchy of abstractions.

Each stage in this hierarchy is an implementation of its preceding stage and a specification of the succeeding stage.

The different stages in this system development activity are requirements specification, functional design, architectural design, detailed design, coding, implementation, etc.

In general, formal techniques can be used at every stage of the system development activity to verify that the output of one stage conforms to the output of the previous stage.

Syntactic domains

The syntactic domain of a formal specification language consists of an alphabet of symbols and a set of formation rules to construct wellformed formulas from the alphabet.

The well-formed formulas are used to specify a system.

Semantic domains

Formal techniques can have considerably different semantic domains.

Abstract data type specification languages are used to specify algebras, theories, and programs.

Programming languages are used to specify functions from input to output values.

Concurrent and distributed system specification languages are used to specify state sequences, event sequences, state-transition sequences, synchronisation trees, partial orders, state machines, etc.

Satisfaction relation

Given the model of a system, it is important to determine whether an element of the semantic domain satisfies the specifications.

This satisfaction is determined by using a homomorphism known as semantic abstraction function.

The semantic abstraction function maps the elements of the semantic domain into equivalent classes.

There can be different specifications describing different aspects of a system model, possibly using different specification languages.

Some of these specifications describe the system’s behaviour and the others describe the system’s structure.

Consequently, two broad classes of semantic abstraction functions are defined— those that preserve a system’s behaviour and those that preserve a system’s structure.

Model versus property-oriented methods

Formal methods are usually classified into two broad categories

the socalled model-oriented
the property-oriented approaches.

In a modeloriented style, one defines a system’s behaviour directly by constructing a model of the system in terms of mathematical structures such as tuples, relations, functions, sets, sequences, etc.

In the property-oriented style, the system’s behaviour is defined indirectly by stating its properties, usually in the form of a set of axioms that the system must satisfy.

Let us consider a simple producer/consumer example.

In a property-oriented style, we would probably start by listing the properties of the system like—the consumer can start consuming only after the producer has produced an item, the producer starts to produce an item only after the consumer has consumed the last item, etc.

Two examples of property-oriented specification styles are axiomatic specification and algebraic specification.

In a model-oriented style, we would start by defining the basic operations, p (produce) and c (consume).

Then we can state that

S 1 + p ⇒ S,

S + c ⇒ S 1.

Thus model-oriented approaches essentially specify a program by writing another, presumably simpler program.

A few notable examples of popular model-oriented specification techniques are Z, CSP,CCS, etc.

It is alleged that property-oriented approaches are more suitable for requirements specification, and that the model-oriented approaches are more suited to system design specification.

The reason for this distinction is the fact that property-oriented approaches specify a system behaviour not by what they say of the system but by what they do not say of the system.

Thus, property-oriented specifications permit a large number of possible implementations.

Furthermore, property-oriented approaches specify a system by a conjunction of axioms, thereby making it easier to alter/augment specifications at a later stage.

On the other hand, model-oriented methods do not support logical conjunctions and disjunctions, and thus even minor changes to a specification may lead to overhauling an entire specification.

Since the initial customer requirements undergo several changes as the development proceeds, the property-oriented style is generally preferred for requirements specification.

Operational Semantics

Informally, the operational semantics of a formal method is the way computations are represented.

There are different types of operational semantics according to what is meant by a single run of the system and how the runs are grouped together to describe the behaviour of the system.

Some of the commonly used operational semantics are :

Linear semantics:

In this approach, a run of a system is described by a sequence (possibly infinite) of events or states.

The concurrent activities of the system are represented by non-deterministic interleavings of the atomic actions.

For example, a concurrent activity a || b is represented by the set of sequential activities a; b and b; a.

This is a simple but rather unnatural representation of concurrency.

The behaviour of a system in this model consists of the set of all its runs.

To make this model more realistic, usually justice and fairness restrictions are imposed on computations to exclude the unwanted interleavings.

Branching semantics:

In this approach, the behaviour of a system is represented by a directed graph.

The nodes of the graph represent the possible states in the evolution of a system.

The descendants of each node of the graph represent the states which can be generated by any of the atomic actions enabled at that state.

Although this semantic model distinguishes the branching points in a computation, still it represents concurrency by interleaving.

Maximally parallel semantics:

In this approach, all the concurrent actions enabled at any state are assumed to be taken together.

This is again not a natural model of concurrency since it implicitly assumes the availability of all the required computational resources.

Partial order semantics:

Under this view, the semantics described to a system is a structure of states satisfying a partial order relation among the states (events).

The partial order represents a precedence ordering among events, and constrains some events to occur only after some other events have occurred; while the occurrence of other events (called concurrent events) is considered to be incomparable.

This fact identifies concurrency as a phenomenon not translatable to any interleaved representation.

Merits and limitations of formal methods

Formal specifications encourage rigour. It is often the case that the very process of construction of a rigorous specification is more important than the formal specification itself.

The construction of a rigorous specification clarifies several aspects of system behaviour that are not obvious in an informal specification.

Formal methods usually have a well-founded mathematical basis. Thus, formal specifications are not only more precise, but also mathematically sound and can be used to reason about the properties of a specification and to rigorously prove that an implementation satisfies its specifications.

Informal specifications may be useful in understanding a system and its documentation, but they cannot serve as a basis of verification. Even carefully written specifications are prone to error, and experience has shown that unverified specifications are comparable in reliability to unverified programs. automatically avoided when one formally specifies a system.

The mathematical basis of the formal methods makes it possible for automating the analysis of specifications. For example, a tableaubased technique has been used to automatically check the consistency of specifications. Also, automatic theorem proving techniques can be used to verify that an implementation satisfies its specifications. The possibility of automatic verification is one of the most important advantages of formal methods.

Formal specifications can be executed to obtain immediate feedback on the features of the specified system.

This concept of executable specifications is related to rapid prototyping.

Informally, a prototype is a “toy” working model of a system that can provide immediate feedback on the behaviour of the specified system, and is especially useful in checking the completeness of specifications.

It is clear that formal methods provide mathematically sound frameworks within which large, complex systems can be specified, developed and verified in a systematic rather than in an ad hoc manner.

However, formal methods suffer from several shortcomings, some of which are as following:

Formal methods are difficult to learn and use. The basic incompleteness results of first-order logic suggest that it is impossible to check absolute correctness of systems using theorem proving techniques.

Formal techniques are not able to handle complex problems. This shortcoming results from the fact that even moderately complicated problems blow up the complexity of formal specification and their analysis.

Also, a large unstructured set of mathematical formulas is difficult to comprehend. It has been pointed out by several researchers that formal specifications neither replace nor make the informal descriptions obsolete but complement them.

In fact, the comprehensibility of formal specifications is greatly enhanced when the specifications are accompanied by an informal description.

What is suggested is the use of formal techniques as a broad guideline for the use of the informal techniques. An interesting example of such an approach is reported by Jones in [1980].

In this approach, the use of a formal method identifies the necessary verification steps that need to be carried out, but it is legitimate to apply informal reasoning in presentation of correctness arguments and transformations.

Any doubt or query relating to an informal argument is to be resolved by formal proofs. In the following two sections, we discuss the axiomatic and algebraic specification styles. Both these techniques can be classified as the property oriented specification techniques.