Logics for Program Analysis



Overview

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; they range from stream-based functional, single assignment and dataflow languages, through regular (and extended regular) expression based pattern-matching languages, to a whole host of modal and, in particular, linear-time temporal logics. The general framework of linear-time temporal logics (LTL) appeared most appropriate for our own work but none of the proposed temporal logics for run-time analysis, of which we were aware, provided the right combination of expressivity, naturalness, flexibility, effectiveness, and ease of use we desired. Of course, more often than not, it can be observed that the greater the expressivity of the property specification logic, the higher the computational cost for its analysis. As a consequence this has led researchers in the past to search for efficient algorithms for the evaluation of restricted sub-logics, e.g. pure past time LTL, pure future LTL, extended regular expressions, metric temporal logic, and so forth. In collaboration with colleagues at NASA Ames, we developed Eagle, a rule-based system for defining and implementing a range of finite trace monitoring logics, such as those mentioned just above. Eagle has been applied successfully in a number of NASA case studies.

From experiences gained with Eagle and reflections on the previous executable temporal logic MetateM and various normal forms used for implemented reasoning processes, we have proposed a simpler rule-based system, RuleR, which can be viewed as a lower-level abstract machine into which various monitoring specifications (from different languages) can be compiled (see also extended version of RuleR). The approach holds the promise for more efficiently rule execution, in comparison with the fairly costly interpretative style used in both Eagle and MetateM. An important feature of the system is the way rules may be switched on or off by the action of a rule, a feature strongly related to the more general forms of reactivity we are studying under the heading of Reactive Grammars.

Equipping trace monitoring logics with the ability to undertake action naturally leads to application in areas such as on-line fault diagnosis and recovery, and the more general notion of Evolvable Systems.

Publications

Personnel

People associated with activities in this area include:

  • Djihed Afifi
  • Joachim Baran
  • Howard Barringer
  • Dov Gabbay
  • Klaus Havelund
  • David Rydeheard

 



Contact Howard Barringer with comments or queries about the content of this website.
All material copyright ©The University of Manchester. Last update October 2007.