Supporting error propagation modeling with Java PathFinder

OData support
Kocsis Imre
Department of Measurement and Information Systems

System diagnosis is a necessity in enormous IT infrastructures. These IT systems consist of both hardware and software components. A component’s failure may cause a system-wide error. If every component’s error propagation property is enlisted, engineers are able track system errors to their source by utilizing error propagation techniques in case of a system failure. Although analyzing a failure is useful, preventing it is more important. By simulating input errors, engineers are able to draw conclusions about the system-wide effects of the cause of error.

There are techniques which might be useful to create these component scoped error propagation rules. Model checking is one of these techniques. The problem with this specific type of verification is its application for real life situations. There are model checking tools which verify a specific input. These inputs usually are abstract software models, like UPPAAL or Promela. One of the exceptions is Java PathFinder. It is a software verification tool which verifies Java bytecode instead of an abstract model. PathFinder has an extraordinary feature enabling us to verify software which communicates with the outside (network, file system, etc.). This feature is achieved by swapping the standard Java classes to altered, model checking enabled ones. Although support for applying network layer abstraction exists, analyzing error propagation by Java PathFinder is difficult and rudimentary.

My goal is to prepare Java PathFinder to support error propagation modeling. Since errors may propagate from node to node by network communication, PathFinder must be prepared to check networked software. There are known issues considering model checking network based applications. These problems must be eliminated if possible. If not, premises are necessary. I show and compare several possible solutions in this document.


Please sign in to download the files of this thesis.