MOVES Seminar July 11, 2006
Temporal Assertions for Sequential and Concurrent Programs
Volker Stolz
Abstract:
In this talk we present an extension of the well-known concept of assertions.
Temporal assertions allow the specification and validation of modal
safety properties of an application at runtime. We see this as a
necessary step in enforcing the growing number of implicit requirements
of software specifications, which are often only informally defined
in the documentation of application program interfaces (API) and
are beyond the reach of type checkers, compilers, or model checkers.
Also we show how our techniques can be applied to existing programs
without modifying the source code. Although, like assertions, our
approach cannot prove the absence of errors, it gives the programmer
a more powerful means of automatically checking assumptions about
his program at runtime.
Temporal assertions allow the specification and validation of modal
safety properties of an application at runtime. We see this as a
necessary step in enforcing the growing number of implicit requirements
of software specifications, which are often only informally defined
in the documentation of application program interfaces (API) and
are beyond the reach of type checkers, compilers, or model checkers.
Also we show how our techniques can be applied to existing programs
without modifying the source code. Although, like assertions, our
approach cannot prove the absence of errors, it gives the programmer
a more powerful means of automatically checking assumptions about
his program at runtime.
