Research areas


Relational databases

I have designed an experimental relational database management system for the PDP-11 mini computers. This design had much in common with the design of the well-known System R which was independently developed a few years later for IBM main frames.

I have also developed an extremely space efficient algorithm for the evaluation of database queries expressed in the relational calculus, and I have made facilities to build tailor-made simple natural language interfaces for this relational database management system.

The development of the query evaluation algorithm was my first formal software development activity; I used just classical first-order logic and elementary set theory to formally specify the query evaluation problem and to verify the correctness of the algorithm.


Programming language semantics and compiler construction

I have been involved in the design of the programming language CHILL (CCITT HIgh Level Language) and the construction of a compiler for it. My main contributions to the compiler construction have been the global design of the compiler, an analysis of typing in CHILL, a description of CHILL by means of an attribute grammar for the benifit of the recognition phase of the compiler, and the detailed design of the translation phase of the compiler by means of VDM (Vienna Development Method). The official language definition has been strongly influenced by parts of this work.

For the translation phase, I have devised a new approach where code generation is driven by simulation of the execution on an abstract machine. This approach allows for many trivially justifiable local optimizations. The starting-point of the rigorous design of the translation phase was the formal definition of CHILL to which I have contributed as well. The design of the translation phase turned out to be highly reusable when the compiler had to be adapted to new target machines.


Reusability of software components

I have been involved in a study of ways to formally specify general-purpose software components and to build up and interrogate libraries of formally specified software components. My contributions include among other things reviews of several existing methods for specifying software components and an approach to matching of specifications that is suited for retrieving appropriate specifications from a library of specifications of available software components.


VDM

I have been involved in the ESPRIT project VIP (VDM for Interfaces of the PCTE). The VIP project has produced a formal definition of the interfaces of the PCTE (Portable Common Tool Environment). My contribution has been the design and definition of the specification language used in this project. This language, known as VVSL (VIP VDM Specification Language), extends VDM-SL (VDM Specification Language) with features for specifying interfering operations and for modular structuring of specifications. The approach to the specification of interfering operations encompasses the approach of rely- and guarantee-condition pairs proposed earlier. To the best of my knowledge, VVSL is still the only language for writing modularly structured VDM specifications with a sound mathematical basis for its modular structuring features.

I have elaborated my contribution to the VIP-project in a Ph.D. thesis entitled ``Syntax and Semantics of VVSL''. A mathematical framework for the semantics of specification languages, specializations and generalizations of this framework needed for the semantics of VVSL, and a formal semantics of VVSL based on this framework are presented. The practical use of the language is further demonstrated by two detailed case studies which provide comprehensive pictures of the relational approach to databases and transaction management in database systems. Many unmentioned assumptions in most work on databases have been made explicit in these specifications. A major revision of my Ph.D. thesis has been published as a book entitled ``Logic and Specification''.

Cliff Jones and I have written an article in which a detailed presentation is given of the typed version of LPF used with VDM and of extensions for base types and type formers used in VDM, subtypes via type invariants, recursively defined types and functions, etc. Different from earlier presentations of this typed version of LPF, the proof rules given here constitute a complete proof system. New induction rules for recursively defined types and functions permit to take the least fixpoint semantics of their definitions into account.


COLD

Loe Feijs, Hans Jonkers and I have written a textbook, entitled ``Notations for Software Design''. It will enable practitioners in software development to develop a working knowledge of a wide variety of formal textual notations for describing software systems, and to use and apply these notations effectively. It also explains practical ways of exploiting them in conjunction with commonly-used, generally informal, graphical notations. Detailed case studies, concerning a vending machine and a computer-controlled railway system, are used to show the notations in action.


SDL

At UNU/IIST (United Nations University, International Institute for Software Technology), I set up the research programme DesCaRTeS (Design Calculi and Research for Telecommunications Systems). This research programme aimed at achieving advances in the areas of validation of SDL specifications and verification of design steps made using SDL. Work related to this research programme includes the following.

A semantics for a simplified version of SDL, based on an extension of discrete time process algebra, has been proposed. This version, called phiSDL, essentially covers all behavioural aspects of SDL.

Timed frames, which are closely related to the kind of transition systems used for the operational semantics of discrete time process algebra, have been studied in a general algebraic setting. TFL, an expressive first-order logic has been proposed for timed frames. A timed frame model for basic discrete time process algebra with finite linear recursion has been defined. This lays the foundation of a transformation of phiSDL specifications to timed frames. Thus, we can basically check whether a system described in phiSDL satisfies a property expressed in TFL.

A next step may be to look for a fragment of TFL that is suitable to serve as a logic for phiSDL and to adapt an existing model checker to phiSDL and this logic. A fragment of duration calculus may be considered as well, since a semantic link between duration calculus formulae and timed frames has been established.

An equational theory capturing the basic algebraic properties of asynchronous dataflow networks has been presented and a process algebra model for this theory has been given. This process algebra model has been adapted to deal with SDL-like dataflow. The result is meant to be the underlying model of a more abstract semantics for phiSDL, which could facilitate devising rules of reasoning for phiSDL.


Process algebra

Jos Baeten and I have written a monograph on timed process algebra in the style of ACP, entitled ``Process Algebra with Timing''. The book concerns an algebraic approach to concurrency and represents a large body of relevant theory about the time-dependent behaviour of reactive and distributed systems. It covers important issues, such as absolute versus relative timing and continuous versus discrete time scale. It is one of the results of a systematic study of issues relevant to dealing with time-dependent behaviour of processes in the setting of ACP.

This study has also resulted in a new real time version of ACP with absolute timing that generalizes various other versions of ACP with timing in a smooth and natural way, an extension of this real time version of ACP with conditionals in which the condition depends on time, a version of ACP with timing that differs from the others by excluding urgency, an assessment of the merits of relative timing in process algebra, a new equivalence for processes with timing, an adaptation of a version ACP with timing to spatially located actions, and an extension of a version ACP with timing to a process algebra for hybrid systems. This work created the need of an extension of the customary approach to structural operational semantics using transition system specifications that takes variable binding operators into account.

My recent work on process algebra goes in other directions: the development and model-theoretic analysis of a first-order extension of ACP, the development of a process algebra with conditional expressions in which the conditions can be retrospective, the development of a process algebra with conditional expressions in which the conditions concern the enabledness of actions in the context in which a process is placed, the development of a process algebra in which processes have an implicit computational capital, the development of an algebra of interacting process components, the axiomatization of meadow enriched ACP process algebras and a study of the extent to which variable-binding operators which generalize associative operators of meadow enriched ACP process algebras fit in with an algebraic framework, the adaptation of a process algebra in which processes have their state to some extent visible by means of propositions to tolerance of self-contradictory states, the development of a process algebra that supports both arbitrary interleaving and interleaving according to some scheduling policy, a study of the use of Hoare logic in a process algebra setting, the development of a probabilistic process algebra that supports both arbitrary interleaving and interleaving according to some scheduling policy, demonstration of a completeness result for ACP with possibly infinite guarded recursive specifications, the development of an imperative process algebra with abstraction that is suitable for information-flow security analysis, the elaboration of a variant of the standard notion of branching bisimilarity for processes with discrete relative timing is proposed which is coarser than the standard notion, and work on thread algebra.


Thread algebra

Thread algebra is a specialized process algebra concerned with threads and multi-threading as found in programming languages such as Java and C#. My work on thread algebra includes: a study of interleaving strategies for threads, the development of a theory that covers basic issues concerning stored threads and their execution using thread algebra, a study of different ways to simulate Turing machines on Maurer machines using thread algebra, the modelling of micro-architectures with pipelined instruction processing using thread algebra, an extension of thread algebra with features of molecular dynamics, a study of the merits of program parallelization for speeding up instruction processing using a variant of thread algebra with synchronous cooperation, the development of a thread algebra for distributed multi-threaded programs with features for load balancing, a study of the role of the operating unit size in load/store architectures using thread algebra, an extension of basic thread algebra with a mechanism, called poly-threading, to handle fragmented program behaviours, an explanation of data linkage dynamics, an upgrade of molecular dynamics, by means of a term rewriting system with rule priorities, a study of shedding, i.e. automatic removal of links in dynamic data structures as soon as they will not be used once again by the program, in the setting of data linkage dynamics, a study of transmission protocols for instruction streams from threads to remote execution environments, and an extension of thread algebra with probabilistic features.


Program Algebra

Program algebra is an algebra of sequential programs in which sequential programs are looked upon as (finite or periodic infinite) single-pass instruction sequences. My work on program algebra includes: a study of the merits of indirect jump instructions, the design of an interpreter for a program notation that is close to existing assembly languages using program algebra and features of molecular dynamics, a study of the expressive power and execution mechanisms of programs that are sequences of instructions from a finite set, a study of the merits of dynamically instantiated instructions, a study of the semantical aspects of instruction sequence fragmentation, a study of the expressiveness of single-pass instruction sequences, the re-design and use of a collection of operators related to the processing of instruction sequences by an execution environment, a study of the behaviours produced by instruction sequences under execution, a study of the extent to which indirect jumps improve instruction sequence performance, the development of theory concerning non-uniform complexity in a setting in which the notion of single-pass instruction sequence is the central notion, the expression of the secure hash algorithm SHA-256 and the Karatsuba multiplication algorithm by single-pass instruction sequences, a demonstration of the role of backward jump instructions by means of instruction sequences that express the long multiplication algorithm, a quest for an equivalence relation on single-pass instruction sequences that captures to a reasonable degree the intuitive notion that two instruction sequences express the same algorithm, the design of a sound and complete Hoare-like logic of asserted single-pass instruction sequences, a demonstration of the role of auxiliary Boolean registers in single-pass instruction sequences that compute Boolean functions, a study of instruction sequence size bounded functional completeness of instruction sets for Boolean registers, the development of an axiom system for behavioural congruence of single-pass instruction sequences, a study of the complexity of the problem of deciding whether a single-pass instruction sequence correctly implements the non-zeroness test, a study of instruction sequences by which Turing machines can be simulated, a study of instruction sequences by which random access machines can be simulated, and a study of instruction sequence notations with probabilistic instructions.


Control Codes

Control code is a concept that is closely related to a frequently occurring practitioner's view on what is a program: code that is capable of controlling the behaviour of some machine. My work on control codes includes: the development of an approach to explain issues concerning control codes that are independent of the details of the behaviours that are controlled.


Theory of Number Systems

My work on abstract data type theory of number systems includes a study of involutive meadows and their partial variants (involutive meadows are roughly fields in which the multiplicative inverse of zero is zero), a study of non-involutive meadows (non-involutive meadows are roughly fields in which the multiplicative inverse of zero is a number different from zero), and a study of which meadows admit transformation of fractions into simple fractions (fractions of which neither the numerator nor the denominator contains a fraction).


Quantitative Methods in Finance

My work in the area of quantitative finance includes the formalization of a cumulative interest compliant conservation requirement for financial products in timed tuplix calculus, a specialized process algebra for financial behaviours, and an preparatory exploration of issues concerning reduced product set finance, the form of finance that the avoidance of interest gives rise to in Islamic finance.