One of the largest research challenges in formal methods is finding compositional development methods to cope with systems which run in concurrent environments. This challenge becomes ever more pressing with the advent of many-core hardware.
- Reasoning about Separation Using Abstraction and Reification
- Extended version (with proofs) of the SEFM-15 invited paper above
- Cliff B. Jones, Balancing Expressiveness in Formal Approaches to Concurrency (freely available from Formal Aspects of Computing).
- Possible values: Exploring a concept for concurrency
- A complete re-formulation of the Rely/Guarantee ideas is given in Balancing Expressiveness in Formal Approaches to Concurrency and Laws and semantics for rely-guarantee refinement
- Taming Concurrency (EPSRC funded) working with Drs Nisansala Yatapanage and Andrius Velykis.
- Understanding concurrent programs using rely-guarantee thinking" (ARC funded)led by Prof Ian Hayes.
My Oxford research showed how the issue of interference could be handled in specifications and design verification by using Rely and Guarantee conditions (the two publications Specification and design of (parallel) programs; Development Methods for Computer Programs including a Notion of Interference between them show over 1000 citations in Google Scholar (2016) and even my thesis records over 3000 citations).
This research (complemented by many theses including Ketil Stoelen, Xu Qiwen and Pierre Collette) has proved successful and has led to a significant amount of recent research. It is however true that rely/guarantee reasoning is heavier than for sequential programs and the "pobl" research (Parallel Object-Based Language) was based on the observations that, for relatively simple concurrent programs, it is possible to use object-oriented concepts in order to constrain the interference which is possible and to virtually eliminate the necessity to reason directly about interference. The most useful references on the "pobl" work are:
- Specification and design of (parallel) programs
- Non-Interference Properties of a Concurrent Object-Based Language: Proofs Based on an Operational Semantics
- Process Algebra Arguments about an Object-Based Design Notation
We also had an EPSRC-funded project ("Splitting (software) atoms safely") that looked at Atomicity Refinement funded by EPSRC. In some sense, this is a developmental view of "linearizability". A couple of key publications here are:
Current research on concurrency includes looking at the links to separation logics - recent cooperation with Ian Hayes looks extremely promising. Some references are:
Formal methods support systems
The current focus of my interest around support tools is the AI4FM project. This is an EPSRC-funded "Responsive Mode" project with joint funding for Alan Bundy at Edinburgh University. Initially, it funded an RA and a PhD student at each site (Leo Frietas and Andrius Velykis at Newcastle; Gudmund Grov and Yuhui Lin at Edinburgh). Gudmund and Leo were then both appointed to Lectureships (but remain strongly involved in the project) and were replaced by Ewen Maclean and Iain Whiteside. The involvement of Andrew Ireland at Heriot-Watt is funded by his "Platform Grant" and Michael Butler from Southampton acts as an advisor to the project.
The thrust of the research is to find ways in which a system can learn strategic ideas from an interactive proof by an expert such that these ideas can be replayed to increase the automation of similar proofs.
Of course, AI ideas have provided invaluable heuristics for theorem proving but our observation (based on working with industry in projects like DEPLOY) is that what blocks the automatic discharge of many formal methods "proof obligations" is specific information about data structures and functions. An expert user can spot these more readily than an engineer: we want the system to "learn" from the expert so that he or she does not have to encore the same tricks in discharging a collection of "similar" proofs.
Recent publications in AI4FM include:
- Cliff B. Jones, Leo Freitas and Andrius Velykis, Ours is to reason why, 2013.
- Leo Freitas and Iain Whiteside, Proof Patterns of Formal Methods, submitted to FM-2014.
We have organised several public events and are currently planning a workshop at AVoCS-15.
In addition to the project web site, there is a mailing list on which we try to update interested people - you can ask to joint ai4fm-info over JiscMail.
Some history about my involvement with support tools for formal methods:
I first ran a project building a support system for formal methods in IBM in the early 70's. The resulting FDSS was sufficiently difficult to use that I'm not sorry it is no longer visible!
Between 1981 and 1987 my research focused mainly on the design and construction of support systems for formal methods, a topic that is still of interest to me.
The Manchester group was involved starting, in 1982, support system projects the largest of which was the Alvey-funded Software Engineering project (IPSE 2.5) which created a Theorem Proving Assistant, mural. See the book:
mural: A Formal Development Support System
C B Jones, K D Jones, P A Lindsay and R Moore, Springer Verlag, 1991 - now available on-line as pdf (thanks to Roberta Velykiene, this now has all of the figures visible).
The IPSE 2.5 project ran from 1984-88 and was the largest software engineering project funded by the ALVEY directorate. It was collaborative with a number of industrial organisations, most significantly ICL. Manchester University in collaboration with Rutherford Appleton Laboratory had a large team (10 Research Assistants at its peak) which constructed the mural theorem proving system. This system was designed as a major experiment in the construction of user interfaces which permitted the person using mural to construct the proof in exactly the steps that they chose.
A related book is:
- Proof in VDM: A Practitioner's Guide Written by J. C. Bicarregui, J. S. Fitzgerald, P. A. Lindsay, R. Moore and B. Ritchie. Published by Springer-Verlag in 1994 as part of the FACIT series. ISBN: 3-540-19813-X
Other publications relating to mural:
- "A Survey of Mechanical Support for Formal Reasoning" by P.A. Lindsay. Article published in the Software Engineering Journal, Volume 3, number 1 in January 1988.
- "Symbolic Execution: a Semantic Approach" by R. Kneuper. Article published in the journal Science of Computer Programming, Volume 15, number 3 (pages 207-250) in 1991.
- "Formal reasoning in an Integrated Project Support Environment" by P.A. Lindsay. Chapter 15 (pages 235-253) of Software Engineering Environments: Research and Practice, edited by K.H. Bennett. Published by Ellis Horwood Publishers in 1989.
- "Muffin: A User Interface Design Experiment for a Theorem Proving Assistant" by C. B. Jones and R. Moore. In proceedings VDM'88: VDM -- The Way Ahead, edited by R. Bloomfield, L. Marshall and R. Jones as part of the "Lecture Notes in Computer Science" series by Springer-Verlag. Volume 328, pages 337-375 (1988).
- "A Support System for Formal Reasoning: Requirements and Status" by C. B. Jones and P. A. Lindsay. In proceedings VDM'88: VDM -- The Way Ahead, edited by R. Bloomfield, L. Marshall and R. Jones as part of the "Lecture Notes in Computer Science" series by Springer-Verlag. Volume 328, pages 139-152 (1988).
- "Reasoning About VDM Developments Using The VDM Support Tool in Mural" by J. C. Bicarregui and B. Ritchie. In VDM '91: Formal Software Development Methods, Volume 551 of the series "Lecture Notes in Computer Science", edited by S. Prehn and W. J. Toetenel, published by Springer-Verlag. Pages 371-388 (1991).
RODIN & DEPLOY
I was involved in both the RODIN and DEPLOY projects - a key output of the latter is the DEPLOY book.
The "Infrastructure Transitions Research Consortium" brings together researchers at seven UK universities who are looking at modelling the way in which the infrastructures that are crucial to civilised life will respond to future transitions such as population and climate change. Not only have the physical infrastructures (Energy, Water, Transport and Waste) become more interconnected, but the interdependencies with ICT become ever more complex. I and my colleagues in Computing are looking at the ICT aspects of ITRC. We produced a Technical Report as input to the first major deliverable from ITRC - its " Fast Track Analysis". Roberta Velykiene was the first researcher involved from our group and her MPhil is visible here. Razgar Ebrahimy is now doing his PhD under ITRC funding.
I was overall project Director of DIRC.
Logics for reasoning about partial functions
Closely coupled with research into support systems for formal methods is a concern for the logics to be used in reasoning. Partial functions and operators are ubiquitous when specifying and reasoning about computer systems. It has been a long-term research interest of mine to look at logics that cope well with partial functions.
To see some of the options, paper "A Semantic Analysis of Logics that Cope with Partial Functions" might be a good starting point.
My approach has been to accept that a non-standard logic is required and our "Logic of Partial Functions" (LPF) is a development of Kleene's logic. The initial paper on LPF was A Logic Covering Undefinedness in Program Proofs by H. Barringer, J.H. Cheng and C. B. Jones; published in Acta Informatica
The above (and Jen Cheng's thesis) covered the untyped logic; the soundness of the typed version of LPF is tackled in A Typed Logic of Partial Functions Reconstructed Classically by C.B. Jones and C.A. Middelburg; published in Acta Informatica
On the usability of logics which handle partial functions by J. H. Cheng and C. B. Jones; pages 51-69 of 3rd Refinement Workshop, edited by C. Morgan and J. C. P. Woodcock; published by Springer-Verlag, 1991. This is also available as a technical report, UMCS-90-3-1.
A useful detailed result is in The Connection between Two Ways of Reasoning about Partial Functions John Fitzgerald and Cliff B. Jones; published in IPL.
Recent research with Matthew Lovert and Jason Steggles has looked at mechanisation issues and yielded:
Paper "Revising Basic Theorem Proving Algorithms to Cope with the Logic of Partial Functions" as well as Matthew's PhD thesis.
An excellent foundation for the logic used in Event-B is Matthias Schmalz's ETH thesis.
A paper that points out some dangers in "fudging" the issue of partial functions is:
Partial functions and logics: A warning by C. B. Jones; Information Processing Letters Vol 54, pp 65-67, 1995
Although I have always wanted to view work on formal methods as evolving, VDM (the "Vienna Development Method" played a large part in my professional work - I spent two long spells at the IBM Lab Vienna. In the first (1968-70) I worked on using the earlier operational semantics as a basis for compiler design; the second period (1973-76) saw the creation of the denotational semantics parts of VDM.
The first three books listed below are concerned with general use of VDM (Google Scholar shows over 2500 citations to the 1990 book in April 2011).
The last two books listed below are specific to the description of language semantics (see also my semantics library pages).
- Systematic Software Development using VDM
Written by C. B. Jones; Published by Prentice Hall International in 1990. (ISBN: 0-13-880733-7) - now available as a pdf (plus Teaching Notes as a pdf).
(Also translated into French by Michel Lemoine as VDM Une methode rigoureuse por le developpment du logiciel).
- Case Studies in Systematic Software Development
Edited by C. B. Jones and R. Shaw; Published by Prentice Hall International in 1990. (ISBN: 0-13-880733-7) - now available on-line as pdf
- Software Development: A Rigorous Approach
Written by C. B. Jones; Published by Prentice Hall International in 1980. (ISBN: 0-13-821884-6) - now available as a scanned pdf
(Translated into Polish by Teresa i Krzysztof Piaseccy as Konstruowanie oprogramowania metoda systematyczna.)
- The Vienna Development Method: The Meta-Language
Edited by D. Bjørner and C. B. Jones; Published by Springer-Verlag as Lecture Notes in Computer Science (Volume 61) in 1978.
- Formal Specification and Software Development
By D. Bjørner and C. B. Jones; Published by Prentice Hall International in 1982 - now available as a scanned pdf.
The specification language (VDM-SL) was one of the first to be standardized by ISO
I was co-founder of an EEC group organised four international symposia on VDM and related matters: the VDM-Europe then group agreed to widen its scope and is now called Formal Methods Europe (FME).
History of formal methods
I have long had an interest in recording and publishing material on the history of formal methods (this includes making source material available on-line). Peter Mosses' PLanCompS project gave me the excuse to pursue more work in this area. Working together with Troy is making it possible to contribute on the History of Formal Semantic Descriptions.