Formal Specifications in Software Development
by Karel Richta
At the Department of Computer Science and Engineering of the Czech
Technical University in Prague, a research project is being carried out
that aims at providing techniques and tools for software development based
on formal specifications.
Present CASE (Computer Aided Software Engineering) systems are usually
based on an architecture consisting of set of tools integrated through
their common access of a centralised repository. This repository maintains
a potentially large amount of information that is organised to provide
different but mutually consistent views of the software under development.
Each tool is dedicated to documenting a different aspect of the system
under design and may employ advanced visualisation techniques as part of
this system description.
On the other hand formal methods for software specification and development
can be utilized to create more comprehensive, shorter, unambiguous and
better structured technical descriptions - a formal specification.
The advantage of CASE tools is their ability to serve as the base for
verification and prototyping of a designed system. CASE graphical techniques
may improve the readability of complex formal specifications. This is one
of a few disadvantages of formal specifications and more user friendly
interface are desired. We try a combination of CASE Data Flow Diagrams
(DFDs) with formal specifications in a VDL-like language (VDL - Vienna
Description Language) in the process of stepwise refinement developed on
the basis of formal specification in VDL. There are two known stepwise
refinement methods: a functional decomposition and a data refinement.
Present CASE systems support usually only functional decomposition.
The data model is developed separately and usually there is no tool for
the corresponding parallel data refinement. All functions are assumed to
utilize common data types specified by the data model. DFD hierarchy is
not a real specification, it documents syntactic aspects only. Upper level
functions are not specified completely and only leafs of the DFD hierarchy
define the semantics of the lowest level functions (primitive functions)
by so called minispecifications. So the designer cannot divide his job
into succeeding steps, which can be verified with respect to each other.
In the process of stepwise refinement, every step (including the first
one) constitutes a complete specification of a problem. Subsequent steps
are refinements of previous ones, they use more complicated (sophisticated)
data types, the details of which are hidden from upper levels and the verification
among refinement steps is possible.
Versions seem to be the analogy in the CASE systems. Each version is
a complete specification, but subsequent ones are more detailed. If the
DFD technique is to be used for description of a specified abstract data
type (ADT), the data flows have to express only the argument types. Data
stores summarize the state of a system. Functions need not be connected
directly in the DFD - but only through data stores. Function dependency
has to be described by a lower level DFD or by a minispecification.
As an example we used the Time-table Creation Support System (TCSS),
which we created as a part of our university information system. TCSS has
to hold data about time-tables, eg, in a data store TIME-TABLE. Therefore,
all processes are grouped closed to the data store TIME-TABLE. Each object
of the this type is a set of time-table items describing details of any
state of a time-table. The actual contents of the TIME-TABLE data store
represents the current state of the time-table. In the early stage of analysis
the user requires to be able to print time-table ordered by groups. TCSS
has to support a function PrintG (version 1). The results of PrintG are
time-tables grouped by groups. This mapping can be extracted from a general
time-table. Then the function PrintG can be rigorously specified by the
formula in VDL.
On the more detailed level of TCSS analysis it was discovered that time-tables
(reported by PrintG) have to be distributed to individual departments.
In this context, a new entity called stream was introduced. The stream
is a set of groups, that belong to the same department. For each stream
there exists a textual explanation of a stream content. Therefore TCSS
has to support a new version of reports (now called PrintG' version 1.1),
where time-tables are sorted by streams and completed by text explanations
associated to streams. The state of TCSS has to be enhanced by data stores
for streams and explanations, the function PrintG' has to be expressed
for new environments. One advantage that formal specifications yield is
a possibility to verify correctness of versions with respect to each other.
To verify the correctness of PrintG, refinement of PrintG means to prove
an appropriate formula. When the proof is finished successfully, we can
be sure that the function PrintG' is the correct refinement of PrintG.
Formal specifications can contribute a number of useful features to
the CASE area. The same is true vice versa, of course. We tried to indicate
here only two aspects of a combination of CASE tools and formal methods
- the semantics of CASE DFD tool has to be defined more precisely with
the help of formal methods, and formal definition can serve for a verification
of stepwise refinement process. Necessary equipment for this is a sufficiently
powerful theorem prover based on the same formal method. Another condition
is that the CASE tool has to enable manipulation with information in a
data repository by an external utility (eg for formal checks).
Please contact:
Karel Richta - Czech Technical University
Tel: +420 2 24357487
E-mail: richta@cs.felk.cvut.cz
