Program Monitoring

Course material for part II of CS 119 - Reliable Software: Testing and Monitoring

Caltech, third term 2008, Tuesday/Thursday 1:00-2:30, Jorgensen 74

All slides in power point format: allslides-ppt.zip

Teacher

Klaus Havelund, Phone (cell): 650-814-0677, Email: klaus.havelund@jpl.nasa.gov

Teaching Assistant

Mihai Florian, Phone: 626-395-3552, Email: mflorian@cs.caltech.edu

Part I

Part I on testing is taught by Alex Groce

Acknowledgements

acknowledgements

Overview

This course offers an introduction to the theory and practice of program monitoring, or runtime verification as we shall call it (since this is becoming recognized as a term for the field). Runtime verification is the study of how to design artifacts for monitoring and analyzing program executions. Such artifacts can be used for a variety of purposes, including testing/program understanding and fault protection. Although programmers have written more or less ad-hoc monitors since the birth of the computer, only recently (last decade) has this areas achieved a status as a field on its own. In this course we shall specifically focus on notations for specifying properties of Java programs, and frameworks for monitoring such. The course will initially address the issue of program instrumentation using aspect oriented programming. At the end of the course the student will have gained insight into the important problems in the field and will have encountered a core selection of solutions for monitoring programs. The course will enable the student to apply monitoring in software development as well as initiate research in this field. Although the course focuses on Java, the ideas extend to other languages.

Course Assignment (deadline June 13 - midnight)

During the course 5 techniques for specifying program monitors were presented: The student is asked to specify each of the 3 properties about the Java API introduced in notes 2 and 3 (from lectures 2 and 3) in each of the 5 specification frameworks, resulting in ideally 15 specifications. The student should submit a package consisting of (i) a final 10-15 page report summarizing the experience, and (ii) a zip file containing the written specifications and example programs illustrating their violation, deadline June 13 midnight, US westcoast time.

Please send the final report + zip file to both:
Update: The second sub-task (checking that input stream gets closed) of the first assignment problem (URLConnection) in note2 has been cancelled (see the note). A simplified non-obligatory problem is formulated in the note.

Lecture Plan

Lecture 1, April 28 - Introduction

Lecture 2, May 6 - Introduction to AspectJ

Lecture 3, May 8 - Monitoring with AspectJ

Lecture 4, May 13 - Propositional Extended Regular Expressions

Lecture 5, May 15 - Parameterized Regular Expressions in JavaMOP

Lecture 6, May 20 - Context Free Grammars in JavaMOP

Lecture 7, May 22 - Temporal Logic in JavaMOP

Lecture 8, May 27 - Super Logics

Lecture 9, May 29 - Specification Free Monitoring

Summary of resources, including optional, mentioned above for each lecture:

Resources

We will study 3 systems: AspectJ (lectures 2-3), JavaMOP (lectures 5-7,) and RuleR (lecture 8). Reading material will be added as the course progresses. Note that each lecture entry above points to all resources needed for that lecture. The list below will become a complete list for the course.

Reading

Systems

Optional Resources

Reading

Systems