We have implemented such a backwards stepping functionality for a platform that is notoriously difficult to debug or even write programs for: microcontrollers. If the program failed, stepping backwards can help find the bug that caused the failure. By keeping track of the nondeterministic choices the program makes during its execution, we can replay them, even backwards. When something goes wrong in a program’s execution, it is often difficult to determine the exact conditions that triggered a bug. A second option is to capture the nondeterminism. Additionally, we used it to find errors in published research. We conducted a user study to confirm GraphRedex is user friendly and helps uncover bugs. This helps developers see the wood for the trees when visualizing all possible execution paths of a program. We allow developers to choose what path in the state space graph they want to follow. Our tool contributes a novel exploration technique for dealing with state explosion: interactive exploration. In this dissertation, we present a tool called GraphRedex, which allows exploring the state space graph of nondeterministic programs. First, to embrace nondeterminism we must have the tools to deal with the state explosion it generates. In this dissertation we investigate the tree main ways programming systems can work with nondeterminism: embrace it, capture it, and avoid it. The chosen constructs greatly impact the nondeterminism the programmer has to deal with. There are constructs for acquiring input, starting concurrent threads and so on. Programming languages have nondeterminism introducing constructs to facilitate working in nondeterministic environments. Both humans and computers cannot deal with state explosion well. Typical debuggers only allow users the debug just one of the possible traces, while the failure may only manifest in very rare execution traces. If a failure occurs in one of the myriad of execution traces, it is difficult to find its root cause. This exponential state explosion is what makes working with nondeterminism so difficult. Even if there are only two possibilities per program step, there are 2^n possible executions of n steps. When writing the program, the developer must imagine all possible executions to prevent bugs. If a program is nondeterministic, the next state may be one of multiple possibilities. Although it leads to nondeterministic execution, we sometimes need it to fulfill real-world demands such as execution performance and high availability. Nondeterminism caused by concurrency stems from the unknown speed of each thread, the possibility of lost messages and so on. A word processor with deterministic input can simply present the user with their envisioned written document without them having to type it. If program input were to be deterministic, there would be no need for complex programs. This nondeterminism may arise from many sources, like user input and concurrency for example. Key words: Program.Ĭomputer programs need to deal with nondeterministic environments. The work is a continuation of an effort to formally analyze, using Spin, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications.
This work should be seen in a broader attempt to make formal methods applicable within NASA's areas such as space, aviation, and robotics. Hence, the Java program must have a finite and tractable state space. Jpf generates a Promela model with the same state space characteristics as the Java program. The Spin model checker will then look for deadlocks and violations of any stated assertions. The Java program may contain assertions, which are translated to similar assertions in the Promela model.
Jpf translates a given Java program into a Promela model, which then can be model checked using Spin. This paper describes a translator called Java PathFinder (Jpf), from Java to Promela, the modeling language of the Spin model checker.
0 kommentar(er)
