Model Checking is an automatic technique for verifying finite-state concurrent systems such as communication protocols and sequential circuit designs. It has a number of advantages over traditional approaches to this ...
详细信息
ISBN:
(纸本)9781424427932
Model Checking is an automatic technique for verifying finite-state concurrent systems such as communication protocols and sequential circuit designs. It has a number of advantages over traditional approaches to this problem that are based on simulation, testing, and deductive reasoning. Model checking tools are, however, not widely introduced into industry, and one of the reasons is that they are tricky and difficult to use for engineers. In this paper, we extend the functions of java pathfinder, a software model checker to verify executable java bytecode programs, and propose a graphical user interface with a high degree of usability. Our GUI depicts the state transition graphs of not only a whole program but also each thread as a result of verification. Users can get much information through the GUI, for example, the internal states of a program and the correspondence relation between the graphs, with interactive mouse operation. One of the key features of our GUI is a variable-value-based graph abstraction that allows users to focus upon an aspect they are interested in. Our GUI also has an intuitively easy-to-use interface for users to input linear temporal logic (LTL) formulae as a program specification based on the Specification Pattern System.
We present a novel technique that speeds up state-space exploration (SSE) for evolving programs with dynamically allocated data. SSE is the essence of explicit-state model checking and an increasingly popular method f...
详细信息
ISBN:
(纸本)9781605580791
We present a novel technique that speeds up state-space exploration (SSE) for evolving programs with dynamically allocated data. SSE is the essence of explicit-state model checking and an increasingly popular method for automating test generation. Traditional, non-incremental SSE takes one version of a program and systematically explores the states reachable during the program's executions to find property violations. Incremental SSE considers several versions that arise during program evolution: reusing the results of SSE for one version can speed up SSE for the next version, since state spaces of consecutive program versions can have significant similarities. We have implemented our technique in two model checkers: java pathfinder and the J-Sim state-space explorer. The experimental results on 24 program evolutions and exploration changes show that for non-initial runs our technique speeds up SSE in 22 cases from 6.43% to 68.62% (with median of 42.29%) and slows down SSE in only two cases for -4.71% and -4.81%.
There is an increasing number of agent-oriented programming languages that have working interpreters and platforms, with significant progress in the quality of such platforms over the last few years. With these platfo...
详细信息
ISBN:
(纸本)9780981738123
There is an increasing number of agent-oriented programming languages that have working interpreters and platforms, with significant progress in the quality of such platforms over the last few years. With these platforms becoming more popular, and multi-agent systems being increasingly used for safety-critical applications, the need for verification techniques that apply to systems written in such languages is proportionally intensified. Building on our previous work on model checking for a particular agent-oriented programming language, we have developed a new approach whereby model checking techniques can be used directly on a variety of such languages. The approach also supports the verification of multi-agent systems where individual agents have been programmed in different agent languages.
Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller stat...
详细信息
ISBN:
(纸本)9780769529776
Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that mitigates the problem of state explosion in code checking of primitive components with the java pathfinder in case the checked property is absence of concurrency errors. The key idea is to reduce parallelism in the calling protocol oil the basis of the information provided by static analysis searching for concurrency-related patterns in the component code;by a heuristic, some of the pattern instances are denoted as "suspicious". Then, the environment (needed to be available since java pathfinder checks only complete programs) is gene rated from a reduced calling protocol so that it exercises in parallel only those parts of the component's code that likely contain concurrency errors.
Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zam...
详细信息
Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce java, a proto pro verifikační metodu byl zvolen model checker java pathfinder, který je určen pro java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy.
暂无评论