IFIP Working Group 2.2
Beijing Seminar
28 September - 4 October 1996.

Abstracts of the lectures

Egidio Astesiano

Integrating Data and Process Specifications

We present an approach to the formal specification of systems (reactive/dynamic/concurrent), which extends some of the key ideas and techniques of the algebraic specification of abstract data types. The approach covers the various phases of the specification process, from requirement to design, via implementation steps.

As a distinguishing feature, compared to others, the method does not just combine the specification of usual static data types with some paradigm for describing processes, but qualifies processes as particular data, abstractly characterised by their dynamic properties.

Indeed: the models of a specification are classes of many-sorted structures (usually many-sorted first-order, possibly partial, structures) and processes are modelled by labelled transition systems, identifying a process state with a dynamic element in a structure, where the activity of dynamic elements is characterised by transition predicates.

As a consequence of the above two key assumptions, we have the benefits of the algebraic approach and of the various techniques flourished around labelled transition systems, plus some extra bonus due to the combination; in particular

The main target of the method is not the specification of algorithms or programs, but of possibly large systems; thus we are very much concerned with the software engineering aspects of the specification process. Currently we are investigating the relationship between formal and informal aspects,following what we have called a "two-rail approach". The method has been developed in the years since '84 and applied in various significant test cases and examples, also in cooperation with industries.

Jaco de Bakker

Semantics for 27 Languages

The aim of our lecture series is to provide an introduction to the following book:
J.W. de Bakker and E.P. de Vink, Control Flow Semantics, The MIT Press, 1996

Linear Semantics for a Schematic Parallel Language

We start with some motivation for the use of metric structures in semantics, emphasizing as objectives our wish to We then use a (schematic or uninterpreted) process description language L0 with interleaving concurrency as a vehicle to illustrate the methodology:

Linear Semantics for a Shared-Variable Parallel Language

By way of recalling the main ideas of the first lecture, we begin with a brief discussion of some further examples of schematic languages, mentioning concepts such as process creation or backtracking. Next, we introduce the class of interpreted or state-based languages. As first example we take L1, a language with assignment, conditionals and the while statement. Though seemingly quite different from L0, the semantic models for L1 use much of the earlier machinery. As new feature we introduce states as mappings from individual variables to their values. We also encounter the control flow tools of resumptions (in the design of O) and of continuations (for D). The main example here is the language L2, obtained from L1 by extending it with shared-variable parallelism. The associated O is now no longer compositional, and new ideas are in order to design the compositional semantics D for L2. The question as to how O and D are related is briefly addressed, also touching upon the problem of full abstractness.

Egon Boerger

Formal Specification and Verification of Pipelining in RISC Architectures

A formal specification of Hennessy's and Patterson's RISC architecture DLX and of the usual pipelining scheme (taking care of structural hazards, data hazards and control hazards) is given by a series of stepwise refined evolving algebras. The correctness proof is outlined.

The lecture is based on joint work with S. Mazzanti (University of Pisa) which is in the process of being submitted for publication. It presupposes only some basic understanding of what a computer architecture is.

He Jifeng

Deriving Handshake Modules for a Multi-Target Hardware Compiler

This talk adopts the CSP framework for deriving a compilation scheme from a simple imperative language to handshake protocols. Handshake modules are processes that communicate with one another using two-phase handshake protocols. The handshake modules generated by the compilation scheme can be implemented as asynchronous or clocked circuits. The derivation techniques have been applied to a current language which is a superset of the language discussed.

Lesli Lamport

The Formal Specification of Computer Systems with TLA+

Part 1. Ordinary Mathematics

The largest source of complexity in the specification of most real systems lies in describing data structures and operations on them. TLA+ handles this complexity by combining the concepts of ordinary mathematics with module structure. This will be illustrated by showing how BNF grammars can be defined in TLA+.

Part 2. Reactive Systems

Specifying reactive systems requires describing the temporal ordering of events. We do this by using the Temporal Logic of Actions (TLA), which adds to ordinary mathematics a new class of variables (flexible variables) and temporal operators. This will be illustrated by specifying some very simple system.

Jay Strother Moore

A Mechanically Checked Proof of the AMD5K86 Floating Point Division Algorithm

ACL2 is a reimplemented extended version of the Boyer and Moore theorem prover, intended for large scale verification projects. We describe a recent application of this new theorem prover. ACL2 was used to prove the correctness of the floating-point division algorithm for the AMD5K86, the first Pentium-class microprocessor produced by Advanced Micro Devices, Inc. This required formalizing and deriving much of the "folklore" of floating-point arithmetic. We describe the algorithm, the theorem proved, and some of the key lemmas.

Peter David Mosses

CoFI: The Common Framework Initiative for Algebraic Specification and Software Development

The Common Framework Initiative for Algebraic Specification (CoFI---may be pronounced like `coffee') is an open international collaboration. The main immediate aim is to design a coherent family of algebraic specification languages, based on a critical selection of constructs from the many previously-existing such languages---without sacrificing conceptual clarity of concepts and firm mathematical foundations. The long-term aims include the provision of tools and methods for supporting industrial use of the CoFI languages.

After motivating the CoFI we outline its aims and scope, and sketch one general design decision that has already been taken. Up-to-date information about the progress of the CoFI and details of the language design proposals are available from the CoFI Home Page on WWW, URL: http://www.brics.dk/Projects/CoFI. (The lecturer is the overall coordinator of the Common Framework Initiative.)

Theory and Practice of Action Semantics

Action Semantics is a framework for the formal description of programming languages. Its main advantage over other frameworks is pragmatic: action-semantic descriptions (ASDs) scale up smoothly to realistic programming languages. This is due to the inherent extensibility and modifiability of ASDs, ensuring that extensions and changes to the described language require only proportionate changes in its description. (In denotational or operational semantics, adding an unforeseen construct to a language may require a reformulation of the entire description.)

After sketching the background for the development of action semantics, we summarize the main ideas of the framework, and provide a simple illustrative example of an ASD. We identify which features of ASDs are crucial for good pragmatics. Then we explain the foundations of action semantics, and survey recent advances in its theory and practical applications. Finally, we assess the prospects for further development and use of action semantics.

The action semantics framework was initially developed at the University of Aarhus by the lecturer, in collaboration with David Watt (University of Glasgow). Groups and individuals scattered around five continents have since contributed to its theory and practice.

Madhavan Mukund

SPIC Mathematical Institute, India

Automated verification in a temporal logic framework

During the past ten or fifteen years, temporal logic has become a very basic tool for specifying properties of reactive systems. For finite-state systems, it is possible to use techniques based on Buchi automata to verify if a system meets its specifications. This is done by synthesizing an automaton which generates all possible models of the given specification and then verifying if the given system refines this most general automaton. In these lectures, we present a self-contained introduction to the basic techniques used for this automated verification.

The lectures assume some familiarity with basic ideas in automata theory and mathematical logic. However, both temporal logic and Buchi automata will be introduced from scratch.

Ernst-Ruediger Olderog (joint work with Michael Schenke)

Design of Real-Time Systems

The transformational approach to the stepwise design of communicating systems is extended to cover real-time. The design starts from requirements formulated in a subset of Duration Calculus, developed by Zhou Chaochen and others, and aims at the specification of distributed communicating programs in a timed OCCAM-like programming language implementing the real-time requirements. The approach uses mixed term techniques where syntax pieces of Duration Calculus and the program specification language SLtime are mixed in a semantically correct manner. The transformation rules are applied to such mixed terms and replace more and more parts of the original requirements by parts of SLtime.

Paritosh K. Pandya

Proving Compiling Correctness using Refinement Algebra

In this lecture, we will describe Hoare's refinement algebra approach to proving the correctness of compiler specifications. In refinement algebra, an inequation p refines q captures the fact that the observable behaviour of program q is as good or better than that of p. Thus, q can be used in place of p in all situations. A set of inequational algebraic laws axiomatise the refinement order. They serve as a basis for carrying out provably correct transformations of programs. They allow proofs of refinement of systems to be given by simple inequational rewriting. Such proofs are transparent and easy to check mechanically. Moreover, the laws often serve as an algebraic definition of the semantics of the programming language.

We will present some of the laws from a refinement algebra for Dijkstra's guarded command programs. We will show how these laws can be used to prove the correctness of a compiling specification for the guarded command language.

In this approach, a compiler is specified as a relation between the source and the target programs. The relation is presented as a set of Horn Clauses, where each clause specifies one way of compiling a construct in terms of the compilation of its components. The semantics of the machine programs is encoded as an interpreter written in the source language. Compiling correctness ensures that for any source program, the interpretation of its related target code gives a refinement of the original source program. Techniques such as simulation allow this proof to be carried out using the laws of refinement algebra.

Amir Pnueli

Verification of a Fully Expressive Temporal Logic - Algorithmic methods

We will introduce the full branching-time temporal logic CTL*, and present algorithmic methods for verifying properties of finite-state systems specified by this logic.

Deductive Verification of the Full Logic

Deductive rules and methods are presented for verifying CTL*-specified properties of infinite-state systems. This extends the temporal methodology for linear-time TL.

Willem-Paul de Roever

Survey of Simulation and Data Refinement Techniques

This survey focuses first on the basic concepts in data refinement, observability and interface refinement, and then on how to prove data refinement using simulation methods. Next soundness and (in)completeness of various simulation methods are discussed. Subsequently we focus on (the need for) abstraction relations, and discuss syntactic characterization of simulation using predicate logic. If time permits the proof of a simple example is given.

Specification statements represent the maximal program satisfying a given Hoare-triple. A major challenge for simulation consists of expressing the weakest lower level specification simulating a given higher level specification w.r.t. a given relation between these two levels of abstraction. The solutions to this challenge for upward and downward simulation in both partial and total correctness frameworks reduce the task of proving data refinement to proving validity of certain Hoare-triples.

Compositionality in Real-time Shared Variable Concurrency

Whereas for distributed communication of multitude of, even compositional, proof systems for real-time exist for real-time shared variable concurrency the picture is quite bleak. This is the more astonishing because it can be argued that hard real-time systems are based on shared variable concurrency. The papers by Abada and Lamport, and Schneider, Bloom and Marzullo form notable exceptions. The former contains a characterization of real-time shared variable concurrency in TLA, whereas the latter presents a noncompositional method for characterizing this concept using proof outlines. In the present paper we present a compositional Hoare style proof system for timed exclusive write and multiple read accesses to shared memory which is based on a compositional semantics which is fully abstract, hence containing the minimal amount of information required for its characterization. Moreover this axiomatization is sound and relatively complete.

Andrzej Tarlecki

Institutions: an abstract framework for formal specifications

Over the recent years the theory and practice of formal software specification and development have both benefited and suffered from a wealth of useful logical system proposed to underly specific approaches. To overcome many of the resulting problems, Goguen and Burstall introduced the notion of an institution, as a certain formalisation of the informal concept of a logical system. It turned out that much of the theory developed in the area of algebraic specification can be done in the context of an arbitrary institution, thus abstracting away from the details of a specific logical system. In this lecture I will attempt to present both basic motivations and intuitions which led to the development of this notion as well as the way institutions are used in the theory of software specification and development. In particular, I will discuss how the work on algebraic specifications in an arbitrary institution provides a formal basis to support a methodology for the systematic development of correct programs from specifications by means of verified refinement steps.

Formal development of modular software systems in Extended ML

Extended ML is a framework for the formal development of software systems in the Standard ML programming language from high-level specifications of their required input/output behaviour. It strongly supports the development of modular systems consisting of an interconnected collection of generic and reuseable units, and has a well-developed mathematical basis in the theory of algebraic specifications. The Extended ML specification language is a simple extension of Standard ML, in which more information may be supplied in module interfaces (axioms in ML signatures) and less information is required in module bodies (axioms in place of code in ML structure/functor bodies). The Extended ML formal development methodology establishes a number of ways of proceeding from a given specification of a programming task towards a finished Standard ML program. Each such step (modular decomposition, etc.) gives rise to one or more proof obligations which must be discharged in order to establish the correctness of that step. This will be an introduction to Extended ML giving a user's-eye view of its main features, and including a look at some of the technical details under the bonnet.

Zhou Chaochen

An Introduction to Duration Calculus

The Duration Calculus (abbreviated DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses the real numbers to model time, and Boolean-valued (i.e. {0,1}-valued) functions over time to model states and events of real-time systems. The duration of a state in a time interval is the accumulated presence time of the state in the interval. DC extends interval logic with a calculus to specify and reason about properties of state durations.

The research of DC was introduced in the ProCoS project (ESPRIT BRA 3104 and 7071), when the project was investigating formal techniques for designing safety critical real-time systems. In a project case study of a gas burner system, it was realised that state duration had not been well studied yet as an essential measurement of real-time behaviour of computing systems. A research of a logic for state durations was therefore initiated by the project in 1990. The first paper of DC was published in 1991, and dozens of papers of DC have been published since then, which cover developments of logical calculi, their applications and mechanical support tools. The success of DC also stimulates similar research in other formal approaches.

This talk will emphasize mathematical models of real-time systems adopted by DC and their formalizations in interval logic.


WG 2.2 (darondeau@irisa.fr)