Prof Howard Barringer - research
Since 1980, Howard's research has been focussed on the development and application of non-standard logics for the modelling and analysis of computational systems, an activity falling under the umbrella heading of formal methods for computer science.
Inspired by the now seminal paper of Pnueli on the application of temporal logic for analysing computer programs, and his own work developing compositional proof systems for the Ada tasking, from 1980 to 1986 Howard attacked the problem of obtaining compositional specification and verification methods for concurrent and distributed computation using temporal logic. The work resulted in general methods for obtaining compositional temporal logic-based program proof systems.
Using logical specification directly as an executable model for simulation and rapid prototyping was in its infancy in the context of predicate logic during the 1980s. Techniques for the direct execution of temporal logic, or interpretation as a programming method, did not exist. In collaboration with Gabbay, Howard developed the imperative view of temporal logic, thereby enabling temporal rule based programming methods. This manifested itself as MetateM at Manchester and Imperial. The ideas underlying the work, continue to feature in their current research in logic, modelling and analysis of evolvable systems.
Since 2000, there has been growing international interest in developing formally based run-time verification methods. A wide variety different languages and logics have been proposed for specifying and analyzing properties of program state or event traces, each with characteristics that make it more or less suitable for expressing various classes of trace properties. In collaboration with colleagues at NASA Ames and JPL, we invented the very general purpose Eagle logic and the lower-level RuleR system, into which one can encode virtually all proposed run-time verification trace logics and languages.
Major challenges for formal methods arise from the need for significantly increased levels of autonomy, adaptability and evolvability in software and hardware systems as society lurches into the 21st century driven by advanced technology, computational control and information processing --- the ubiquitous computing environment. Traditional formal methods, which in effect demand a full specification or formal model of the overall system behaviour in order to perform correctness analyses of the model, statically during development, are no longer appropriate. Evolvable systems typically require some form of dynamic analysis that is undertaken throughout the lifetime of the computing system. A significant programme of research is developing logical foundations for such complex systems. The research is heavily influenced by early ideas embedded in MetateM, Eagle and RuleR.