|
John Derrick |
|
Contact Details |
|||||||
Professor of Computer Science |
|
|||||||||
Teaching
Interests
I currently teach a 3rd year and MSc course on the Theory of Distributed Systems. This covers an introduction to process algebra, CSP, as well as the theory and use of refinement. In general my teaching interests are in formal methods, specification, design and testing.
Research
Interests
My research interests are in
specification, design and testing using formal methods. Much of the
work has been conducted as part of a group applying formal techniques
to problems in distributed systems, although my own interests have
broadened out to general problems in formal specification. In
particular, I have a specific interest in the use and theory of refinement
in specifications languages. This covers both state-based languages
such as Z and B, as well as process algebraic approaches, eg as found
in CSP and LOTOS.We did a significant amount of work on formal specification and verification of distributed multimedia systems and the use of viewpoints in Open Distributed Processing. More recent interests have looked at the application of model checking techniques to the Erlang functional programming language, this ties in with the above work on specification since we use an abstraction of Erlang to the muCRL process algebra in order to verify liveness properties of OTP Erlang code.
Research themes include the following:
- Refinement in state-based systems
- Integrated formal methods
- Viewpoint specification using formal methods
- Formal methods, their semantics and interrelationships
- Property-based testing and model checking of Erlang code
- Testing of formal specifications
- Specification and verification of non-functional requirements (eg QoS)
- True concurrency semantics for process algebras
- Type management in distributed systems
- Applications of temporal and deontic logics (eg to multimedia and enterprise specification)
- Policy specification
- Frameworks for distributed systems: architectural semantics, specification templates, object orientation, interfaces.
I am recently held a Leverhulme Research Fellowship for two years.
Current
Projects
Current interests and projects include the following:
- Refinement of state-based systems - an overview of work in this area, much of it done in collaboration with Eerke Boiten and Graeme Smith
- RefineNet - the UK Refinement Network funded by the EPSRC
- FORSE - Formally-based tool support for Erlang development - a joint project with the University of Kent
- ProTest - Property-based testing for Erlang - an EU FP7 STREP coordinated by the Univeristy of Sheffield
- Integrated specification notations - a Royal Society and British Council funded project with Heike Wehrheim
- Z to SAL - building a model-checker for Z
Past
Projects
The home pages of the projects:
- FORTEST - the UK Testing Network funded by the EPSRC
- Cross Viewpoint Consistency in ODP
- V-QoS
- OpenViews
- FORCES
- Design Support Environments for Distributed Systems
- Policy specification
- A constructive framework for partial specification
I have worked with a number of colleagues, at Kent these including: David Akehurst, Clara Benac-Earle, Howard Bowman, Eerke Boiten, Behzad Bordbar, Charles Briscoe-Smith, Jeremy Bryans, Marius Bujorianu, Jovan Cakic, Peter Linington, Ralph Miarka, Maarten Steen, Chris Taylor and Gill Waters.
PhD
positions
If you are interested in undertaking a PhD in any of the above topics, please contact me. A list of possible dissertation topics can be found here. Alternatively, if you have a particular theme in mind, I would be interested in hearing of it.
Grants
Funding and support for the group has been provided by the EU, EPSRC, the Royal Society, British Council, British Telecom, APM, Eurocontrol, and the DTI.
Here is a list of grants held. These include recent EPSRC research projects mentioned above and also work on distributed systems design environments, viewpoints in ODP, consistency checking and a collaboration with Lancaster University on performance analysis. A new EPSRC grant on Model Driven Architecture will begin later in 2009, this is a joint project with King's College, London.Conferences
and events
I am involved in the following:
- I am Vice-chair of IFIP
Working Group 6.1 (Architectures and Protocols for Distributed
Systems), and on the steering committees of FMOODS, FORTE/PSTV and
TESTCOM.
- I am on the steering committees of a number of IFIP international conferences including FMOODS (Formal Methods for Open Object-based Distributed Systems); TestCom and FORTE.
- A member of the programme committee for a number of conferences, including the International Conference of Z Users; the Integrated Formal Methods (IFM) series of conferences.
- Conference chair for FORTE/PSTV in 2007; IFM in 2004; and FMOODS in 1997. Workshop chair for Formal Methods 2008 in Turku.
- Program committee member for ASM'04
- I have just finished being on the Panel for the BCS Distinguished Dissertations scheme
- Chair of the BCS FACS sub-group on refinement
I organised Integrated
Formal Methods 2004 at Kent in Easter 2004, and FMOODS at Kent in
July 1997. I was co-chair of
the St-eve
workshop at FME'03 on State-oriented vs. Event-oriented thinking in
Requirements Analysis, Formal Specification and Software Engineering.
With Eerke Boiten, I run the series of International Refinement Workshops. These events have included the following:
the Refinement
Workshop, at FME/FLOC in Copenhagen in July 2002.
The refinement
workshop at ICFEM conference in Manchester in 2005. The meeting co-located with ICFEM 2006
in October 2006. We then co-located with
FM 2008 in Turku.
The next meeting will be held at FM2009 in Eindhoven. More details of these meetings are available: here. Each meeting gives rise to a special issue of a journal, past issues have appeared in Formal Aspects of Computing and Science of Computer Programming.
I am a member of the Verification and Testing research group.
Recent
Publications
Books
Recent books include the following:
- Refinement in Z and Object-Z: Foundations and Advanced Applications by John Derrick and Eerke Boiten. (Springer FACIT series, ISBN 1-85233-245-X.) Reviews in STVR; in Journal of Logic and Computation.
- Formal Methods for Distributed Processing (with Howard Bowman) provides a state of the art survey of the field was published by Cambridge University Press.
- Integrated Formal Methods 2004, proceedings edited jointly with Eerke Boiten and Graeme Smith, LNCS, Springer.
- Formal Techniques for Networked and Distributed Systems - FORTE 2007, edited jointly with Juri Vain, LNCS 4574, Springer.
Journal guest editors
- Guest editor of Science of Computer Programming in 2009 (to appear) containing papers from the 2008 refinement workshop;
- Guest editorships of editions of Formal Aspects of Computing in 2005 and 2008 containing selected papers from the refinement workshops;
- Guest editor for an edition of Formal Aspects of Computing, volume 18(1), March 2006, on formal methods and testing.
- Guest editor for an edition of Formal Aspects of Computing, volume 17(4), December 2005, containing selected papers from IFM'04.
- Guest editor for an edition of Software and System Modeling (SoSyM), May 2005.
- Guest editor for an edition of Formal Aspects of Computing, 15(1), November 2003, containing selected papers from REFINE 2002.
- Guest editor for an edition of IEEE Transactions on Software Engineering, volume 26(7), 2000.
- Guest editor for an edition of Software Testing, Verification and Reliability, volume 10(4), 2000.
- Guest editor for an edition of Computer Science Education, volume 10(3), 2000.
Other publications
A list of Journal and Conference publications is also available: