Question

List the components of a formal specification language in software engineering and describe their roles in detail.

Answer 1

TECHNIQUES OF FORMAL SPECIFICATION

A majority formal methods rely on some well-known, or cafully des igned,
mathematical foundations such as typed set theory (Z), logic of partial fun ctions (VDM),
many-sorted first-order logic <IOTA, OBJ), initial algebras (Larch) and the like . Other
techniques adopt a less formal approach, their main objective being the possibility to
use the specification lan guage as some kind of high-level programming language which
may be executed directly (i.e., after interpretation or compilation). A number of such
languages have been proposed, some of them not even attempting fo rmal verification.

Languages of this kind are often used for rapid prototyping in order to demonstrate
t he be havior of t he specifi ed system; such prototypes are usually discarded in favor of
full -fledged applications . This group of languages will not be covered in this paper.
From the mathematical point of view, specificat ionts) corresponds to lan guage
modulets ), and execut ing the specificat ion means that we are able to prove
mechanical ly certain kinds of formulas of the theory defined by the speci fi cat ion .
In ot her words. one approach to executability follows the philosophy of stepwise
refinement, and implements one specification with anot he r, more detailed one. Each
successive level of specification contains more design decisions made, until eventually a
specification is obtained which is sufficiently detailed to be considered a program. An
outstanding example of the refinement phi losophy is the Ina J o specification method.
More often, however, executability is taken in the se nse that an algorithmic
procedure exists for t ransforming specificat ions into executable programs, without
intermediate refinement ste ps. This transformation may then be performed
mechanically, using an Interpreter or a compil er . Interpreters and/or compilers exist for
a small number of met hods only; often they implement only a subset of the language.

A hybrid approach is exemplified by the two-tiered Larch specifications, where
specifications are first written in an implementat ion-independe nt, shared language.
These specifications are the implemen ted with more detailed specifications 'Written in
an implemen tation-specific lan guage, closely corresponding to the programming
language which will be used for actual coding.

It should be noted that most specificat ion languages emphasize brevity and
clarity rather than executebility. This facilitates both 'Writing specifications and their
mechanical verification, usually with the aid of a manual, user-assisted, or partially
automated theorem prover (fully automated provers are not yet available).

The amount of information which must be maintained in today 's medium-and
large-scale software project s necessitat es the use of automated assistence, e.g., syntaxdirected
editors, code management techniques, version cont rol systems , etc. Note that
t he large amount of information is also the main reason for the inability of classical
structured methodologies to deal successfully with such software projects. Although
form al methods reduce the quantity of information to be handled, at least in the early
design stages, they would certainly benefit from having some form of machine support.

As most formal methods utilize some nonstandard symbols, a dedicated
documentation system may be considered a conditio sine qua non, although this need is
easily fulfilled by modern word-processing software and typesetting systems. The aid of
a syntax-directed editor is almost a necessity, and the next level of support could
involve sophist icated syntactic and semantic checkers, in which knowledge of both
aspects of the specificat ion language used would be embodied. Theorem provers are
used for verification, eit her manual or with some degree of user interactive guidance.
Finally, code generato rs transform the specificat ions into executable code. At present,
most formal methods have only limited machine assistance, up to the level of theorem
proving, while only a few are supported by code gene rato rs. However, one may "benefit
from the use of fo rmal methods without the use of sophist icated support tools. The
advantages of formality are too significant to await the development of a fully
supported method" .

As always, the integration and interoperability of these tools play a crucial role
in their effectiveness. If tools are designed separate ly, without proper communication
mechanisms built-in right from the start, their usability will be significan tly reduced.

An integrated design environment should be equipped with dedicated tools
for performing various tasks . A simple collection of tools is hot enough: for maximum
effecti veness good coordina tion should exist among various tools , and the tran sition
between tasks should be smooth. Only then will the designer be freed of most , if not all,
housekeeping fun ctions, so that she/he can concentrate on specifi cation. An ideal des ign
environment should support all activities in each phase of software design ; an
interesting attempt in that direction is described by Blum .

Support and coordination for team development is also a very important issue,
given the size and complexity of even modest projects today. This includes mostly
version control, and (to a lesser exte nt ) some support for multiuser operation. Fonnal
specifications are still designed by rather small teams, hence the usual problems of
concurrency, recovery and the like are not too significant .

Reusability is one of the key issues in all modern software design
methodologies, and formal methods are no exception. Libraries of predefined
constructs, describing commonly used modules (whatever they may be called in any
particular language) enable the specifier to concentrate on the particularities of the
system being modeled - without having to reinvent the wheel each time. Moreover, as
specificat ions found in these libraries are usually written by the aut hors of the
language themselves, they are usually well designed and thoroughly tested. The
specifier may use them as examples of good style, after which her/his 0 w'0 specificat ions
may be patterned. This is often hard to find in classical software systems, since most of
the code written by experienced programmers is copyrighted and unavailable, while
textbooks contain mostly toy codes, unfit for real- size projects . It should be noted
that a number of quite good formal libraries exist, but the organizations which have
these are unwilling to make them widely available because of commerci al reasons .

********************************************************************************************************************************

CLASSIFICATION OF FORMAL SPECIFICATION

Specification languages may be classified according to different characteris tics.
One of the classification criteria, and possibly the most important one, is based on the
mathematical foundation of these methods. According to this criterio n, we may
discriminate between model - and property -oriented languages . Model-oriented
languages provide a twofold description of system behavior: first, the data structures
(such as strings, numbers, sets, tuples, relations, sequences, etc) that const it ute the
sys tem state are described. Then, the operations that manipulate that state are defined
using assertions in a notation similar to first-order predicate calculus. These languages
are sometimes called constructive, and they include Z, YOM, Milner's CCS, Hoare's
esp, and others.

Property-oriented methods define the system in terms of properties that must
be satisfied in some or all of the system states. The latter include the so-called
axi omatic approaches, such as those embodied in specification languages IOTA, OBJ,
Larch, and Anna, as well as the so-called algebraic approaches, e.g., the one used in
LOTOS. However, the data structures are described here as well, the most common
being sets, lists, sequences, and other structures with a straightforward mathematical
interpretation. The desired set of properties is usually expressed as a set of equations.
Equations may be interpreted as directional rewrite rules, which may be used to
simplify a statement by reducing it to some canonical form. Term rewriting is one of
the most important research directions in connection with formal methods, as
witnessed by several conferences and special journal issues.

In another classification, the distinction is made between specificat ions that
8-1 V. B. MiSic, D. Velasevit I Formal Specifications in Software Developmen t
concentrate on internal structure of specificand objects <st ructu ral specifications), and
those that predominantly describe the observable behavior of these objects (be havioral
specifications). However. st ructural specifications often include some not ions of
specificand behavior, and vice versa, thus blurring the distinction betwee n the two
kinds of specifications.

As specification methods deal with large systems and data st ructures of
appropriate size and complexity, support for speci fication modulari zation and
st ructuring is essenti al. Some rather popular formal methods provide no such support,
or a limited amount only (as is the case with Z and VDM). This is often considered to be
their mai n defficiency, and extensions aimed to correct it have been reported, e.g., in
[38, 30). Most other methods have some provisio ns for modularization, usually in the
fonn of one or more of the so-called specification-building operators. In its simplest
form, one specification can import another one as a subspecification, enriching it with
additional sorts and operators. The entire model is organized then in the form of a
hierarchy (or , more generally, a directed, acyclic graph) of specificat ions . This is
somewhat similar to the inheritance mechanism of object-oriented languages. Other
met hods provide more sophisticated mechanisms for importing subspecifications ,
offe ring the possibility to redefine some of its sorts, or further constrai n their behavior
by redefining some of the applicable operators.

Another important mechanism is that of parameterization, "a process of
encapsulating a piece of software and abstracting from some names occuring in it . in
order to repl ace them in ot her contexts by different actual operato rs" . Together
with structuring and modularization support, parameterization frees the designer from
reinvent ing standard specifications, letting he rlhim concentrate on the particulars of
the problem at hand. As is the case with other software compone nts, standard
specifications may be distributed in the form of libraries, thus promot ing reusability.
Such libraries are sti ll not available for most specification techniques presented here;
instead, the specifier must resort to case studies and introductory or reference texts,
whatever is available.

Most specificat ion lan guages contain only declarations an d equations ; if
imperative andlor applicative style statements are included as well, the language is
considered to be a wide-spectrum one .

A number of languages concentrate on functional properties of the syst em
being modeled. while dynamic concepts (e.g., concurrency, real- time behavior,
reliability, security, performance), cannot be easily accounted for in these
specifications. Other languages have been specifically designed for systems in which the
dynamic component is crucial. Most of t hese are based on some exte nsion of the finite
state machine concept; among the most distinguished are the well-known CCS and CSP
formalisms, as well as a class of languages specialized for telecommunication systems,
such as LOTOS. Estelle and SOL . We should also ment ion Petri Nets, known
s ince the late 19605, and their numerous variations . Petri Nets have been a
particularly success ful formalism for real-time system specification and analysis, as
exemplified in both research and industrial projects . They have been coupled with ot he r
formal notations in order to extend versatility to a wider class of systems .

Instead of de.si gnlng a completely new language, some researchers have been
extending languages of the former group to incorporate some dynamic concepts.
Examples of such an approach (which we might call evolutive) are exte nsions of the Ina
Jo language with tempo. ' logic , and the Maude lan guage, which contains OBJ3 as
a fu nctional sublanguage I incorporates some novel concurrency concepts .

In other words , these languages may be considered attempts to get the best of both worlds
by augmenting already existing specifica tion languages with the desi red properties .
These issues are still new and more experience needs to be gathered before some
definitive conclusions can be made; it seems a promising avenue anyway, and important
results are to be expected.