This web page contains additional information on the thesis manuscript of Leonard Lensink.
It contains both
code that is referred to in the different articles, as well as some background information that did not make it
into the articles that have been submitted to journals and conferences. It also describes how the three articles
that are based on research on the reentrant readers-writers algorithm relate to each other. The contents of this
web page will be incorporated into the introduction of the final version of my thesis.
This page is subdivided into sections that correspond with the
articles that make up the thesis. The code that can
be found here is of varying quality: Some of it is cleaned up and some of it still contains useless bits or may
differ slightly from code snippets in the articles.
describes a formal model and proof of a scheduling algorithm that
is used in Smartcard Personalization
machines by Cybernetix. It contains a state transition model, a functional model and semantic attachments that
were used to graphically display simulation runs of the scheduling algorithm. The models are here.
This article is
about a piece of C++ code, implementing reentrant read-write
locks. This piece of code was
used in the Qt library. We have constructed Uppaal models to model check the algorithm and the PVS model
that was used to verify a suggested solution to the bugs found in the algorithm. The Uppaal and PVS models
can be found here.
continues the research started in the previous article. Besides
looking at deadlock, it also examines
whether starvation can occur. Furthermore, instead of using Uppaal as the model checker, it employs Spin,
because the Promela language is closer to the original C++ code. The Spin models and PVS models can
be downloaded here.
In contrast to the previous article, where the models were
constructed to verify a specific algorithm,
this article describes a more general approach to derive models in PVS from Promela models. It provides
a framework that can be used to prove properties of concurrent programs. The framework was derived from
the PVS model from the previous article. The elements that are used are described in the article.
The article uses the bakery algorithm as a running example. The application of that framework to the running
example can be found here.
This article describes
how PVS models can be used to generate Java programs along with
These annotations allow verification of the generated code in order to verify that the code that is generated
satisfies the specifications. Some more information on the translation process can be found in this technical
NASA report, with some more technical details here. A general overview of the ideas and techniques behind
the translator can be found here.
The translator from PVS to Why to Java (and an XML representation
of the translated program in Why) was
fully developed by me, with the exception of some of the code for first version of the Why to Java translation,
which was written by César Muñoz. Code to add semantic attachments was added at a later date by a student
visiting NIA. The code my translator as used in this chapter can be found here. The core of the translation
from PVS to Why can be found in the file perico\lib\pvs2why.lisp, with as entry function pvs2why-theory.
The core of the translation from Why to Java can be found in the file perico\lib\why2java.lisp, with as entry
The article uses examples from the PVS AirStar model that was
developed by NASA Langley. The models
and the generated Java code can be found here.
Students visiting NIA are adding more functionality to the
prototype translator. If you are interested in using
the code for new projects, it is best to check with César Muñoz, Alwyn Goodloe from NASA Langley or me
to find out what the status of the latest version is.