Instant Incremental Class Invariant Checking for Java Virtual Machines (bibtex)
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},
}
Powered by bibtexbrowser