The following technical report is available from http://aib.informatik.rwth-aachen.de:
Temporal assertions for sequential and current programs Volker Stolz AIB 2007-15
In this thesis, we present an extension to 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.