Temporal assertions for sequential and concurrent programs

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.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2006

Author dc:creator

• Stolz, Volker

Contributors dc:contributor

• Indermark, Klaus

• info:eu-repo/classification/ddc/004
• Assertion
• Temporale Logik
• Informatik
• runtime verification
• temporal logic

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123989%22

OAI identifier oai:identifier

oai:publications.rwth-aachen.de:62419