1. |
Title: |
UPPAAL and SCSI Protocol Example |
|
Author: |
Andre Wong |
|
Abstract: |
Formal methods that are easy to use but with
limited flexibility are sometimes criticized as unnecessary. This
presentation will take a detailed look at a formal method that claims
to be user-friendly - UPPAAL. UPPAAL is a toolbox for modeling, simulating
and verifying real-time systems, and components of the UPPAAL toolbox,
the modeling language and the verification language will be discussed.
A SCSI bus protocol example is also presented to illustrate its various
features. There are discussions regarding advantages and tradeoffs in using
UPPAAL. Conclusions are drawn regarding to UPPAAL and "user-friendly" methods
in general.
|
|
Report: |
postscript (2111kB)
compressed postscript (299kB) |
|
Appendix: |
postscript (1986kB)
compressed postscript (172kB) |
|
|
|
2. |
Title: |
A Case Study: Production Cell with PROMELA/SPIN |
|
Authors: |
Dimi Paun and Bernd Biechele |
|
Abstract: |
In this project we develop a software controller
for a production cell system. The main objective is to find out if
PROMELA/SPIN is an appropriate environment for developing embedded real-time
systems. We describe the production cell hardware model and its requirements.
Subsequently we describe the model of a distributed and concurrent controller
for it. Furthermore we mention some required properties we could prove
with SPIN based on our model as well as those we could not prove.
We outline a transformation scheme of the PROMELA language to C code.
Finally we describe some experiences and draw conclusions.
|
|
Report: |
postscript (293kB) compressed
postscript (66kB) |
|
|
|
3. |
Title: |
Automatic Verification of Asynchronous Retransmission
Go-Back-N ARQ Protocols Using the Concurrency Workbench |
|
Authors: |
Hai Wang and Hwei Sheng Teoh |
|
Abstract: |
The Go-Back-N and Selective-Repeat automatic
repeat request (ARQ) protocols are widely used for error control in computer-communication
networks. They are nearly optimal for channels characterized by low
error rates and small propagation delays, and thus suitable for many classical
data transmission applications. However, these protocols are not
efficient for modern non-conventional channels with high error rates and/or
large propagation delays, such as mobile and satellite links. In
this talk, we present a family of new protocols, termed Asynchronous Retransmission
Go-Back-N ARQ protocols, which offer the potential for better performance
in environments characterized by high error rates and/or large propagation
delays. We verify that these protocols are deadlock-free using the
Concurrency Workbench. We also verify that all these new protocols
provide the same services to applications as the basic Go-Back-N
protocol, and all of them are equivalent to the basic Go-Back-N
protocol from the application point of view.
|
|
Report: |
postscript (206kB) compressed
postscript (43kB) |
|
Appendix: |
postscript (199kB)
compressed postscript (37kB) |
|
|
|
4. |
Title: |
Studying the Behaviour of Place/Transition
and Coloured Petri Nets - an Implementation Using LP |
|
Authors: |
Cathy Jansen and Alberto Paccanaro |
|
Abstract: |
Some elementary concepts on Equational Theories
and Term Rewriting Systems are introduced, followed by a brief review of
the main ideas of the Knuth-Bendix completion procedure. Then a formalization
of Place/Transition and Coloured Petri Nets as Term Rewriting Systems is
proposed, which allows the use of Rewriting Techniques for studying the
behaviour of such nets. We verify the relationships existing between Completion,
Theorem Proving and Term Simplification and some properties of the Petri
Nets, and show how such operations can be used to prove facts about the
nets. Particularly, the formalization proposed in this talk leads to an
efficient method for determining the movements of the tokens in the net,
and it allows a natural way of simplifying nets in order to express more
efficiently the movements of tokens when transitions are fired. The theory
has been implemented using LP, the Larch Prover, which has been used to
derive the results of the examples presented in this talk.
|
|
Report: |
postscript (633kB) compressed
postscript (91kB) |
|
|
|
5. |
Title: |
Integrating Object-Oriented Analysis and Formal
Specifications |
|
Author: |
Wei Ding |
|
Abstract: |
OO lacks a simple model theoretical foundation
for definition and discussion, so we need formal models for the object-oriented
programming paradigm. The major concern of this project is to describe
the current state of the art in some of the formalisms in object-oriented
analysis and design, their usage, and limitations.
|
|
Report: |
postscript (1107kB)
compressed postscript (118kB) |
|
|
|
6. |
Title: |
Formal Methods: More Than Just Proofs |
|
Author: |
Danny House |
|
Abstract: |
In this course we looked at tool support for
verifying that a design satisfies a specification, with emphasis on problems
involving concurrency. We sometimes hear that formal methods will
ensure that we build things right the first time. There are many
obstacles to be overcome before that glorious day, and in the mean time
formal methods are being used for much more than verification, including
automatic generation of tests and implementations from specifications,
software reuse, improved documentation, and design recovery. This
report describes some of the issues in these alternate applications of
formal methods, and some of the work being done to resolve these issues.
It also touches on some of the issues for verifying conformance that did
not arise during the course, including the choice of what to specify and
the meaning of conformance, scale of effort, support for revision, and
verifying implementations.
|
|
Report: |
postscript (341kB)
compressed postscript
(41kB) |
|
|
|