
Home

Research

Papers

Future Events

Workshops

Invited presentations

Program committees

Contact me

|
|
Research
Runtime Verification
My main interest is the development of runtime monitoring techniques,
including the design of powerful monitoring logics, and algorithms for detecting
concurrency errors such as deadlocks and various forms of data races.
The most recent work includes the RMOR monitoring tool for monitoring C programs against state machines
using aspect oriented techniques.
Previous work includes the very powerful
Eagle
temporal monitoring logic, implemented in the Eagle Flier trace checker. Eagle supports
user definable logics and combinators, using recursive fixpoint rules and parameterization with
formulas as well as with data. Real-time logics can be defined in few lines of Eagle.
Model Checking
I conceptualized and developed during 1998 the first prototype of
the Java PathFinder model checker,
Java PathFinder 1
(JPF1), a
translator from Java to Promela, the modeling language of the SPIN model
checker. JPF1 translates a large non-trivial subset of Java 1.0 into
Promela, allowing model checking of the Java program.
I was later involved in the initial phase of the development of
Java PathFinder 2
(JPF2-...), the second generation of Java PathFinder.
The current Java PathFinder project
has been run by Willem Visser.
JPF2 is written in Java and model checks Java bytecode directly.
I worked for during 1996-1997 at Aalborg University Center with Kim Larsen. Here I studied
various protocols from Bang & Olufsen using the UPPAAL real-time model checker. We found
a bug that had gone unexplained for 10 years, although its precense was known. The error became
important due to a transition from hand-held remote controls to automated control.
Formal Specification Languages
During the years of 1984-1991, I was part of the language design team of the
RAISE project. There are two websites for this project (at least):
RAISE in Denmark and
RAISE in Macau.
RAISE stands for Rigorous Approach to Industrial Software Engineering, and is a
formal software development method, including the very powerful wide-spectrum formal specification
language RSL. It even has
tools developed by UNU/IIST.
What is RSL more specifically?
There are many ways to present it. Here is one:
RSL is a derivation of VDM.
Take a standard imperative
programming language;
add pre-post conditions;
predicate logic;
notation for manipulating sets, lists and maps;
algebraic specification;
funtional programming;
process algebra; and a module system, and melt it into a unified language.
Support it with a framework for refining high level specifications into low-level code.
If that sounds
too much, then try it, it's in fact not that complicated, and it's a lot of fun.
If you want to know more, contact my colleagues
from the past
Jan Storbank Pedersen (jnp@terma.com),
Chris George, or the ultimate source
Dines Bjoerner, my first real boss after studies,
that started all this.
I have unfortunately (by my own fatal choice) been away from this since 1991 when I started my PhD.
Here I tried to build an RSL-like language on top of the Concurrent ML
(CML) programming language.
See also the book that I co-authored (wrote the majority of):
"The RAISE Specification Language", The RAISE Language Group, Prentice-Hall,
that is being used at several academic instutions for teaching students about formal
methods.
It can be acquired from
TERMA.
Theorem Proving
I worked during 1994-1996 on theorem proving, trying to prove programs correct
using the PVS theorem prover.
I wanted to understand what it really means
to prove a program correct. I have to say, I believe I got chemically addicted to
the Q.E.D. text appearing after each finished PVS proof. Is it possible? I think it is.
I had time to do proofs, was sitting in Paris, having expressos, generating Q.E.Ds,
and generally feeling pretty good about life. Several visits to SRI, my
first entry into the United States.
Programming Language Semantics
My master thesis and Ph.D. thesis at
DIKU
(Datalogisk Institut ved Koebenhavn's Universitet), University of Copenhagen, both contained a large
bulk of programming language semantics work. My master thesis was supervised by
Neil Jones (the man that made partial evalution work)
and resulted in a refinement of an abstract denotational semantics for a small programming language,
into a compiler-like denotational semantics, in six steps, each step being more concrete than the former.
This work consolidated my interest in functional programming.
My Ph.D. thesis (see my papers) was focused on development of an operational
semantics and temporal logic for a process algebra with a fork operator instead of the traditional parallel
operator as found in CCS and CSP. It was called the Fork Calculus (FC).
Why doing this? .. well my real goal was to develop a temporal logic for
Concurrent ML (CML), and CML has a fork operator and not a parallel
operator (CML = ML + fork-based concurrency). Believe it or not, but that changes a great deal when it comes
to temporal logic for such a language. In order to understand the consequences I had, for practical
reasons, to study the problem at a calculus level. An influence was
Extended ML (EML= ML + axioms). I attempted to develop an Extended CML
(ECML = CML + axioms). My thesis towards the end (after a lot of Fork Calculus theory)
contains a proposal for such a language.
My supervisors were Klaus Grue (formal supervisor) and
Kim Guldstrand Larsen, and I was
hosted at Ecole Normale Superieure in Paris with Patrick Cousot,
very complicated setup, but it worked (it was impossible to pull me out of Paris).
Klaus grue is known for his MAP theory,
a unifying framework for computer science and mathematics
, combining set theory and the lambda calculus. Kim Larsen is the guy behind the
UPPAAL real time model checker, and Patrick Cousot and Radhia Cousot
conceptualized abstract interpretation.
Free website templates
|
|