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