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 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, the development of an
imperative process algebra with abstraction, a study of the role that this imperative process algebra can play in describing
models of parallel computation and complexity measures for them, the development of a process algebra that concerns the timed behaviour of systems with a known spatial distribution and that provides a truly algebraic mechanism for asynchronous communication in space-time, 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).
Non-classical logics
My work in the area of non-classical logics includes a study of
various properties of an interesting
expansion of the paraconsistent logic
LP, the presentation of a
classical-logic view of the first-order
version of this logic, an application of this logic to
query answering in inconsistent
databases, a study of various properties of an interesting
expansion of first-order Belnap-Dunn
logic, an application of a minor variation of this logic to
query answering in inconsistent databases
with null values, and a study of the
interdefinability of expansions
of Belnap-Dunn logic.
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.