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
Phone (cell): 650-814-0677, Email: firstname.lastname@example.org
Phone: 626-395-3552, Email: email@example.com
on testing is taught by Alex Groce
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.
- aspect oriented programming in AspectJ (lectures 2 + 3)
- regular expressions in JavaMOP (lectures 4 + 5)
- context free grammars in JavaMOP (lecture 6)
- temporal logic in JavaMOP (lecture 7)
- rule-based monitors in RuleR (lecture 8)
Please send the final report + zip file to both:
- Klaus Havelund : firstname.lastname@example.org
- Mihai Florian : email@example.com
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 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:
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
- AspectJ (aspect oriented programming)
(monitoring oriented programming)
(rule-based runtime verification)
The Racer Tool
(data race detection for Java)
(an extension of AspectJ with regular expressions)
(one of the first systems, supporting past time temporal logic)
(combines AspectJ with future time temporal logic)
(context-free, combined with intersection; this class is a
superset of context-free languages)