Potential PhD topics in the area of Testing, Concurrency and Verification
Verification of Concurrent Algorithms
In order to fully exploit the concurrency, programmers develop very subtle lock-free algorithms which dispense with the need for wholesale locking on shared memory and data structures. The complexity of these algorithms means that checking their correctness with a high degree of confidence is extremely difficult.
This PhD looks at how we can verify such algorithms using a collection of techniques borrowed from formal methods. It looks at how to establish the important correctness criteria for modern architectures (including weak memory models), and then develop sound and complete proof methods for such criteria.
There are a wide variety of specific PhD projects available within this general area, including those concerned with linearizability, weak memory models, software transactional memory (STM), general correctness conditions (consistency, linearizability, opacity), and proof methods combined with testing.
Contact: John Derrick
Email: j.derrick@dcs.shef.ac.uk
Testing from Erlang code
Erlang is a concurrent functional
language with specific support
for the development of concurrent, distributed systems with
soft real-time requirements. Erlang was originally conceived within
Ericsson,
but now has a wider enthusiastic developer community, and is used in
companies
of all sizes, most commonly small teams within SMEs.
Its domain of application including telecoms and computer telephony but
also
covers banking, TCP/IP programming, 3D-modelling and more.
Testing of Erlang code is crucial, since it is often used within
business critical environments. Whilst there is some support for the
testing
process via OTPs test environment and the QuickCheck Erlang tool, there
is
considerable scope to provide further automation and support. This PhD
project will investigate this issue. Again there are a variety of specific PhD topics in this general area, including work on: security, model inference, test generation etc.
This will involve a wide range of work and approaches and students in
this area with a background in Erlang, formal methods and test
generation would be particularly suitable.
Contact: John Derrick
Email: j.derrick@dcs.shef.ac.uk
Refinement of State Based Systems
The project involves looking at the
theoretical and practical aspects of
refinement of state based systems, with an eye towards their use in
describing distributed systems. There are lots of possibilities of
topics
using languages such as Z, Object-Z, UML, temporal logics etc.
Contact: John Derrick
Email: j.derrick@dcs.shef.ac.uk
Relating Formal Specification
Languages
The use of different (formal)
languages in the description of one system
requires that we relate languages, their refinement relations, and
their
semantics. Research in this area centres on the interplay between
process
algebras and state-based techniques, and in particular how to integrate
or
translate between languages such as Z and Object-Z with LOTOS and CSP.
Contact: John Derrick
Email: j.derrick@dcs.shef.ac.uk
Property preserving development
Formal development of systems proceeds
stepwise, where every step is
motivated by a formal relation between the stages before and after that
step. This relation is normally expected to be the same,
viz. "correctness preservation" at every step.
This is not entirely realistic, however: preservation of correctness is
sometimes too strong (e.g. replacing mathematical integers by machine
ones), and sometimes too weak (e.g. not enforcing improvements in
executability or efficiency, or not preserving fairness or security).
This project will consider models of formal development in which the
various steps do not necessarily preserve the same properties, and how
these relations can be composed.
Contact: John Derrick
Email: j.derrick@dcs.shef.ac.uk