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