VDM'91 Formal Software Development Methods

Formal specification methods have not been embraced wholeheartedly by the software development industry. We believe that a large part of industry's reluctance is due to semantic gaps that are encountered when attempting to integrate formal specification with other stages of the software development process. Semantic gaps necessitate a dramatic shift in a programmer's mode of thought, and undergoing many such shifts during the development of a software system is inefficient We identify semantic gaps in the software development process and show how they can be minimized by an approach called metamorphic programming that operates in-the-large and in-the-small. The main contribution that metamorphic programming makes to formal specification is to clarify the ways in which specifications can be merged smoothly into the software development lifecycle.

An important goal of software engineering is to exploit commonalities in system design in order to reduce the complexity of building new systems, support large-scale reuse, and provide automated assistance for system development. A significant roadblock to accomplishing this goal is that common properties of systems are poorly understood. In this paper we argue that formal specification can help solve this problem. A formal definition of a design framework can identify the common properties of a family of systems and make clear the dimensions of specialization. New designs can then be built out of old ones in a principled way, at reduced cost to designers and implementors.To illustrate these points, we present a formalization of a system integration technique called implicit invocation. We show how many previously unrelated systems can be viewed as instances of the same underlying framework. Then we briefly indicate how the formalization allows us to reason about certain properties of those systems as well as the relationships between different systems.

The variants of specification languages used with the Vienna Development Method (VDM) offer a rather expressive notion of types. Higher order function types, recursively defined types, and a notion of union types which does not require injection and projection are all included, not to mention subtypes characterized by arbitrary predicates.Besides this, VDM specifications are in general not executable so dynamic type checking does not make sense. However, proof of their total consistency (satisfiability), as advocated by Cliff Jones [5], covers all type checking including what is usually considered “dynamic”, e.g. index range checks. In addition, it ensures other desirable properties such as termination of recursively defined functions.In this paper, we identify a number of general problems concerning automatic type checking of VDM specifications and the relation to consistency proofs. The authors are currently investigating different ways of handling the problems and the presentation includes outlines of some of these.

We provide a rigorous development of a structure sharing unification algorithm from an abstract algorithm of established correctness. This is done by a mixture of transformation and posit- and-prove techniques. From this, some conclusions are drawn about a practical approach to rigorous development and the way in which it should be supported.

Both formal methods and structured methods in software development have disadvantages inherent to the class of methods they belong to. A better method may be composed by taking the best of a formal method and the best of a structured method and constructing one, new method. In this paper two approaches to transforming data flow diagrams, the main system representation resulting from SA, to constructs in VDM are described. Each approach can be used as a basis for a combined SA/VDM method. A comparison is made between the two presented models by analyzing their characteristics. Some conclusions on the usability of the combination of SA and VDM are presented.

A model-oriented method for algebraic specifications is described, using the design language COLD-1 as notation. The method is based upon standard algebraic concepts, such as equivalence relations, congruence relations and homomorphisms. The method makes a clear distinction between the abstract type being defined and the model used as representation. The advantage of this approach is that the problem of implementation bias does not apply and that the operations of the model do not need to satisfy a property usually termed representation invariant. As such, the method deviates in an essential way from model-oriented methods like VDM and Z. Conceivable tool support for the method is briefly sketched.

Fairness abstractions are useful for reasoning about computations of nondeterministic programs. This paper presents proof rules for reasoning about three fairness notions and one safety assumption with an automated theorem prover. These proof rules have been integrated into a mechanization of the Unity logic [8,9] and are suitable for the mechanical verification of concurrent programs. Mechanical verification provides greater trust in the correctness of a proof.The three fairness notions presented here are unconditional, weak, and strong fairness [6]. The safety assumption is deadlock freedom which guarantees that no deadlock occurs during the computation. These abstractions are demonstrated by the mechanically verified proof of a dining philosopher's program, also discussed here.

This paper deals with the specification of communicating systems and their stepwise transformation into occam-like programs. For communicating systems a model similar to Hoare's CSP is used. First a specification language is given, which is particularly suitable for describing communicating systems. A quite simple readiness semantics allows to specify the users' wishes in an exact but easily expressible manner. Secondly aspects of a development approach are shown, how to achieve programs satisfying these specifications. For this purpose transformation rules are given whose applicability can be checked syntactically. Their correctness can be proved on the basis of readiness semantics and predicative semantics for the programming language. The main characteristics of the approach are illustrated by examples.

Prototyping formal specifications can help capture accurately the requirements of real-world problems. We present a software system, called EZ, that generates executable prototypes directly from certain Z specifications. We first describe how nonmodular Z specifications can be mapped to search systems in C-Prolog. We then add modularity (schema referencing) and other features. A short comparison is made to other existing Z prototyping systems, with possibilities for future work being suggested.

High level Petri nets have tokens with values, traditionally called colors, and transitions that produce tokens in a functional way, using the consumed tokens as arguments of the function application. Large nets should be designed in a topdown approach and therefore we introduce a hierarchical net model which combines a data flow diagram technique with a high level Petri net model. We use Z to specify this net model, which is in fact the metamodel for specific systems. Specific models we specify partly by diagrams and partly in Z. We give some advantages and disadvantages of using Z in this way. Finally we show how to specify systems by means of an example.

The work presented here concerns abstract specification of type checking for a specification language VDM-SL of the Vienna Development Method. Where previous work has focussed on rejection of “obviously” ill-typed specifications we do, in addition, consider acceptance of “obviously” well-typed expressions.The presentation includes essential parts of the definition of several well-formedness predicates for increasingly advanced type analyses. In order to emphasize the similarities and symmetries, the different predicates are defined in terms of a single, parameterized predicate.In other work, an independent definition of (type) consistency of VDM-SL specifications has been put forward. We discuss the necessary conditions for the correctness of our type checking with respect to this definition.

The notion of behavioural extension is important for system evolution, incremental design and, inheritance in object-orientation. Behavioural extension as relations between CSP processes is investigated. A number of different extension relations are developed motivated by some examples of behavioural extension from the telecoms domain. Each extension relation is characterised in terms of CSP operators and a number of algebraic laws stated. The results are then transferred to the action system approach to CSP and rules for behavioural extension in action systems are developed.

We consider type universes as examples of regular algebras in the area of the denotational semantics of programming languages. The paper concentrates on our method which was used implicitly in the studies of the domain universes underlying MetaSoft, cf. [BBP90], and BSI/VDM, cf. [TW90].Technically speaking the method allows to prove that a given algebra, e.g., an algebra of types, is regular. It is demonstrated by means of an example that the method applies even to universes which are essentially regular, i.e., which are neither cpo's, nor the images of the initial regular algebra.

This paper compares the finitary three-valued logic LPF and the infinitary two-valued logic MPLω, the logics underlying VDM SL and COLD-K. These logics reflect different approaches to reasoning about partial functions and bringing recursive function definitions into proofs. The purpose of the comparison is to acquire insight into the relationship between these approaches. A natural translation from LPF to MPLω is given. It is shown that what can be proved remains the same after translation, in case strictness axioms are added to LPF or removed from MPLω. The translation from LPF to MPLω is extended to recursive function definitions and this translation is next used to justify some ways of bringing the definitions of partial functions into proofs using LPF.

A major issue in software engineering is the mastery of sofware design. The increasing distributed programming facilities open lots of new possibilities but make the task of designers more complex. Our work is to contribute to a rational design of real-sized distributable applications. We propose an approach based on the VDM formal method as support for the design phase and based on the Conic distributed language and environment as target for the implementation. We apply successive refinements on a VDM model so as to modify its distributability. The refinements are formalized, their validity is proved and they are tactical tools for a support environment of distributable software design. We express the general architecture of the resulting application into Conic.

The paper presents an attempt to develop a totally correct shared-state parallel program in the style of VDM. Programs are specified by tuples of five assertions (P,R,W,G,E). The pre-condition P, the rely-condition R and the wait-condition W describe assumptions about the environment, while the guar-condition G and the eff-condition E characterise commitments to the implementation.The pre-, rely- and guar-conditions are closely related to the similarly named conditions in Jones' rely/guarantee method, while the eff-condition corresponds to what Jones calls the post-condition. The wait-condition is supposed to characterise the set of states in which it is safe for the implementation to be blocked; in other words, the set of states in which the implementation, when it becomes blocked, eventually will be released by the environment. The implementation is not allowed to be blocked during the execution of an atomic statement.Auxiliary variables are introduced to increase the expressiveness. They are used both as a specification tool; to characterise a program that has not yet been implemented, and as a verification tool; to show that a given algorithm satisfies a specific property. However, although it is possible to define historyvariables in this approach, the auxiliary variables may be of any type, and it is up to the user to define the auxiliary structure he prefers. Moreover, the auxiliary structure is only a part of the logic. This means that auxiliary variables do not have to be implemented as if they were ordinary programming variables.

The paper suggests a technique for representing partial recursive functions in Logic for Partial Functions. The technique preserves the least fixed point interpretation of such functions, and in this sense improves the technique hitherto applied to represent VDM specifications.

Mural is an interactive mathematical reasoning environment designed to assist the kind of theorem proving tasks that arise when following a formal methods approach to software engineering. It is the result of work carried out at Manchester University and the Rutherford Appleton Laboratory under the Alvey IPSE 2.5 project.Considerable design emphasis has been placed upon the user interface, using the power of workstation technology to present information and to give the user freedom of action backed up by careful dependency tracking. Through this emphasis on the user interface it is hoped to enable users to maintain their intuition of the problem domain and hence guide the proof in the right direction, whilst the mechanical symbolic manipulation of the machine can maintain the integrity of the proof.The Mural proof assistant is generic in that it can be instantiated for reasoning in a variety of logics. Logical theories are constructed in a hierarchical store where collections of declarations and axioms are structured along with derived rules and their proofs. Some effort has been spent on the instantiation of the proof assistant for the formal method VDM. This instantiation includes theories of the logic LPF upon which VDM is based, and of the basic types and functions of VDM.The system includes tools for the construction of VDM specifications and reifications between them and for the generation of the proof obligations that provide the basis of the formal verification of the refinement relationship. It also supports the construction of theories in the proof assistant where it is possible to reason about specifications, reifications and proof obligations. Though there are many more features that would be desirable in a complete environment for VDM, this degree of support has shown that the Mural proof assistant could be used as an integral part of a generic support environment including provision for the formal development of software.This paper concentrates upon the VDM support aspects of Mural: how users can build specifications and reifications between them; and how these are “translated” into Mural theories including the generation of the corresponding proof obligations.

In this paper we describe a new formal methods tool called EVES. EVES consists of a set theoretic language, called Verdi, and an automated deduction system, called NEVER. We present an overview of Verdi, NEVER, and the underlying mathematics; and develop a small program, to demonstrate the basic functionality of EVES.

This paper reports on an exercise to study how a typical fundamental property of a development technique, viz. transitivity of data-reification in VDM, is formally derived as a property of a method formalization in a meta-calculus, viz. DEVA. To this end, an existing DEVA-formalization of the VDM-reification has been generalized such that its axiom set becomes independent from the number of reification steps performed. This generalized formalization allows to prove transitivity of reification. The formalization and the transitivity proof are performed completely inside DEVA.

This paper gives a reconstruction of the classical pre- and postcondition technique from its roots and extends it with several features. A number of problems in connection with pre- and postcondition specifications are discussed and solutions presented. Problems that are discussed include: framing, dynamic object creation, non-atomic actions and user-friendly syntax. The technique as described is part of the specification language COLD-1 and has been used in several industrial applications.

This paper reports on the use of formal refinement in the development of a Transaction Processing (TP) mechanism for a secure database management system called SWORD. The SWORD specification, written in Z, defines the semantics of concurrent transactions which operate on shared databases without interfering. The specification is quite abstract: in contrast, our design for the TP mechanism (also specified in Z) is extremely complex since it achieves noninterference without using data locks. This paper describes our experience of using formal specification and refinement to develop the TP mechanism in a manner which is amenable to reasoning about its correctness.

In this paper we present and discuss specification, conceptual and technical design of a Serial Copy Management System (SCMS), devised to control copying of digital audio signals by DAT recorders. The specification and designs presented in this paper are written in the formal wide spectrum design language COLD-K. The work was performed in relation to the development of the Digital Audio Interface Standard.

Traditionally, substantial portion of database application semantics are captured through static and dynamic integrity constraints. The work reported in this paper exploits this fact by interpreting such database constraints as invariants and preand postconditions in the style of ’Z’ [ScPi87,Spi88].Database applications are specified by a conceptual modelling language close to TAXIS [MBW80], which has been enriched by constructs for a predicative specification style. Conceptual designs of database applications are formally analyzed for consistency and are refined, step by step, into efficient extended relational implementations. The reification of designs into implementations uses the formal framework of Abrial's Abstract Machines and generalized substitutions [Ab89].It is shown that a small set of standard refinement rules is sufficient for a wide class of refinements. Furthermore, it is argued that the proposed proof-based approach has significant advantages over the traditional database technique, which tests constraints expensively at transaction commit time.

This paper reports on results obtained by specifying the connection patterns within a small PBX using Z. We discuss techniques for specification of switching systems, including how to model the state space of a feature-rich switching system, how to use the schema calculus for organizing a complex operation set, and how to realize the potential benefits of a partial specification. We also outline a new approach to constructing a specification as a composition of partial specifications written in different formal languages.

A detailed example is given of how a formal specification language has been used to specify an international banking standard on message authentication. It illustrates how a specification language can be used to specify and validate a standard.

Formal methods can be neatly woven in with less formal, but more widely-used, industrial-strength methods. We show how to integrate the Larch two-tiered specification method [GHW85a] with two used in the waterfall model of software development: Structured Analysis [Ros77] and Structure Charts [YC79]. We use Larch traits to define data elements in a data dictionary and the functionality of basic activities in Structured Analysis data-flow diagrams; Larch interfaces and traits to define the behavior of modules in Structure Charts. We also show how to integrate loosely formal specification in a prototyping model by discussing ways of refining Larch specifications as code evolves. To provide some realism to our ideas, we draw our examples from a non-trivial Larch specification of the graphical editor for the Miró visual languages [HMT+90].

The Software Engineering Department of HP Labs is developing and applying a small but powerful specification language, HP- SL. This project report provides an overview of the language, its supporting tools and the way in which it is being applied.

The purpose of this paper is to report on the development of a debugging tool for a Meta-IV-like language. The tool consists of a static semantics checker and a debugger. The meta-language includes a subset of the DDC Meta-IV language, but with some simplifications and enhancements. A strong typing system was added to improve the static semantics checker. The debugger itself is quite powerful and includes features allowing (for example) invariants to be attached to breakpoints, objects and types. This paper explains why the debugger was developed, gives a short overview of the meta-language by comparing it to DDC Meta-IV, and presents some important features of the debugger.

In ESPRIT project no. EP5570 called IPTES1 a methodology and a supporting environment for incremental prototyping of embedded computer systems is developed. As a part of this prototyping tool an interpreter for an executable subset of a VDM dialect is developed. Based on a comparative study of different notations inspired by VDM we have now selected an executable subset of the BSI/VDM-SL2 notation. This executable subset is interesting because it enables the designer to use loose specification. None of the executable VDM dialects which we have investigated contain as large a part of looseness as our subset does. In this article we will focus mainly on which constructs we have in this subset and how we have dealt with the looseness. Furthermore we will sketch the connection between the semantics of our subset and the semantics for the full BSI/VDM-SL.

The formal specification of OSI network management protocols presents a challenge as the structure and semantics of the information to be communicated across an interoperable interface is modelled as managed objects. It is necessary to integrate formal techniques into the specific object-oriented framework developed by the ISO management standards.This paper examines the suitability of VDM as a candidate formal description method for use in specifying the behaviour of OSI managed objects. To investigate the suitability of incorporating object-oriented concepts such as inheritance within VDM, a case study of a simplified Log managed object class is examined.

This paper is a project report, presenting a few results of the ESPRIT project ATES, concerned with formal software development. A programming and proof system, based on a high level, abstract language, able to express the specifications necessary to develop reliable software, in a program-to-proof approach is described. Within this approach, we want to conceive a program and introduce the elements necessary for its proof, at the same time. (Those formal proof elements consist in logical assertions expressing mathematically what an algorithm does and logical properties of the function realized by the algorithm). Those proof elements will be used by the system, to verify the correctness of an algorithm, guided by an interactive proof checker.

Practically all of the applications have realised their initial objectives, which is a substantial achievement. It is too early to pass comment on the longer term objectives, although work towards some of these has begun.At the current stage of the project some of the applications have just finished constructing their initial specifications while others are still in the process of doing so. Therefore the experiences documented in this project report only relate to the process of learning RAISE, constructing initial specifications, and using the first release of the documentation and the tools.To date, RAISE has shown itself to be a versatile approach to initial specification. However, there are detailed issues which have been raised as a result of the work over the current period. These are discussed below.

A formal specification of a complex programming language statement is presented. The subject matter was selected as being typical of the kind confronting a small software house. It is shown that formal specification notations may be applied, with benefit, to ‘messy’ problems. Emphasis is placed upon producing a specification which is readable by, and useful to a reader not familiar with formal notations.

With the tool Exspect one can design and simulate formal specifications of distributed systems by means of a formalism based on hierarchical colored Petri nets. A graphical tool set to support the specification process has been implemented. It consists of an editor that allows for hierarchical structuring, a type checker that verifies the rules of the type system and a simulator.

The HP-ST toolset allows a specifier to construct a specification document which contains mixed text and HP-SL specifications. The toolset can be used in either batch mode, when it is invoked as a collection of Unix commands, or in interactive mode, when it is invoked via an editing interface such as that provided by Emacs. Documents are LAT_EX files with LAT_EX-like annotations to control preprocessing.

The VDM-compiler is able to process a subset of the VDM specification language as described in the BSI Proto Standard [PS91]. The compilation includes parsing, check of context conditions and code generation. The target language is an intermediate tree language [SC83, VO83] for which different code generation modules exist. Thus the VDM-compiler can produce code for various machines.