by Sebastian Wilms
Abstract:
Software systems fail. Although software developers mostly try their very best to avoid errors in software systems, failures are unavoidable. Sometimes the failures are catastrophic, resulting in financial loss or even danger to human safety. Often the faulty behavior leads to the system being in an invalid state, which may cause follow-up errors later on. Yet, invalid states of a system can be detected using class invariants. Class invariants express the valid states of a software system and must not be violated. Through exhaustive testing, these invariants can then be tested to ensure that they hold. Invariant checking may thus avoid failure. Unfortunately, existing approaches for invariant checking require extensive manual intervention in where/how to place the invariants in the code. Invariants only need to be validated in situations where its validity is affected. This requires careful placement of invariants checks in the code - a placement that needs to be reconsidered every time the code changes or the invariant changes. The only alternative is to validate the invariants continuously at every step of the software execution. However, doing so is unscalable. This thesis presents a novel, tool-supported approach for invariant checking that automatically decides when to validate invariants in a manner that is significantly more scalable compared to placing invariants everywhere and in a manner that is guaranteed correct. Apart from defining the invariant, no additional user interaction is required. The approach avoids the invariant placement problem by observing the software system execution and triggering an invariant check only if the software system state changed in a relevant manner. By observing the execution and recognizing state changes of a software system during runtime, we are able to drastically reduce the number of performed invariant checks. The proposed approach has been implemented for the Java programming language but is, in principle, applicable to other languages also. We evaluated its correctness, performance and scalability on several open source case studies.
Reference:
Instant Incremental Class Invariant Checking for Java Virtual Machines (Sebastian Wilms), Master's thesis, Johannes Kepler University (JKU), Linz, Austria, 2013.
Bibtex Entry:
@MastersThesis{Wilms2013,
author = {Sebastian Wilms},
title = {Instant Incremental Class Invariant Checking for Java Virtual Machines},
school = {Johannes Kepler University (JKU), Linz, Austria},
year = {2013},
abstract = {Software systems fail. Although software developers mostly try their
very best to avoid errors in software systems, failures are unavoidable.
Sometimes the failures are catastrophic, resulting in financial loss
or even danger to human safety. Often the faulty behavior leads to
the system being in an invalid state, which may cause follow-up errors
later on. Yet, invalid states of a system can be detected using class
invariants. Class invariants express the valid states of a software
system and must not be violated. Through exhaustive testing, these
invariants can then be tested to ensure that they hold. Invariant
checking may thus avoid failure. Unfortunately, existing approaches
for invariant checking require extensive manual intervention in where/how
to place the invariants in the code. Invariants only need to be validated
in situations where its validity is affected. This requires careful
placement of invariants checks in the code - a placement that needs
to be reconsidered every time the code changes or the invariant changes.
The only alternative is to validate the invariants continuously at
every step of the software execution. However, doing so is unscalable.
This thesis presents a novel, tool-supported approach for invariant
checking that automatically decides when to validate invariants in
a manner that is significantly more scalable compared to placing
invariants everywhere and in a manner that is guaranteed correct.
Apart from defining the invariant, no additional user interaction
is required. The approach avoids the invariant placement problem
by observing the software system execution and triggering an
invariant check only if the software system state changed in
a relevant manner. By observing the execution and recognizing state
changes of a software system during runtime, we are able to drastically
reduce the number of performed invariant checks. The proposed approach
has been implemented for the Java programming language but is, in
principle, applicable to other languages also. We evaluated its correctness,
performance and scalability on several open source case studies.},
file = {:MSc Theses\\2013 Sebastian Wilms\\Wilms - Instant Class Invariant Checking for Java-preprint.pdf:PDF},
owner = {AK117794},
timestamp = {2015.09.22},
}