Temporal assertions for sequential and concurrent programs
Volker Stolz · 2007
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. It can also be used to look for behaviour that indicates the potential for problems, that is, that might be used to predict future errors. An example is the Lock-order Reversal pattern which indicates a potential deadlock in a concurrent program. Our parametrised propositions approach gives us a convenient way to handle dynamic