共查询到20条相似文献,搜索用时 15 毫秒
1.
Jan Tobias Mühlberg Gerald Lüttgen 《International Journal on Software Tools for Technology Transfer (STTT)》2014,16(1):81-102
Software model checkers quickly reach their limits when being applied to verifying pointer safety properties in source code that includes function pointers and inlined assembly. This article introduces a novel technique for checking pointer safety violations, called symbolic object code analysis (SOCA), which is based on bounded symbolic execution, incorporates path-sensitive slicing, and employs the SMT solver Yices as its execution and verification engine. Extensive experimental results of a prototypic SOCA Verifier, using the Verisec suite and almost 10,000 Linux device driver functions as benchmarks, show that SOCA performs competitively to modern source-code model checkers, scales well when applied to real operating systems code and pointer safety issues, and effectively explores niches of pointer-complex software that current software verifiers do not reach. 相似文献
2.
Alastair F. Donaldson Daniel Kroening Philipp Rümmer 《Formal Methods in System Design》2011,39(1):83-113
Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with
small “scratch-pad” memories. The price for increased performance is higher programming complexity – the programmer must manually
orchestrate data movement using direct memory access (DMA) operations. Programming using asynchronous DMA operations is error-prone,
and DMA races can lead to nondeterministic bugs which are hard to reproduce and fix. We present a method for DMA race analysis in C programs.
Our method works by automatically instrumenting a program with assertions modeling the semantics of a memory flow controller.
The instrumented program can then be analyzed using state-of-the-art software model checkers. We show that bounded model checking
is effective for detecting DMA races in buggy programs. To enable automatic verification of the correctness of instrumented
programs, we present a new formulation of k-induction geared towards software, as a proof rule operating on loops. Our techniques are implemented as a tool, Scratch, which we apply to a large set of programs supplied with the IBM Cell SDK, in which we discover a previously unknown bug.
Our experimental results indicate that our k-induction method performs extremely well on this problem class. To our knowledge, this marks both the first application of
k-induction to software verification, and the first example of software model checking in the context of heterogeneous multicore
processors. 相似文献
3.
In this paper we define a requirements-level execution semantics for object-oriented statecharts and show how properties of
a system specified by these statecharts can be model checked using tool support for model checkers. Our execution semantics
is requirements-level because it uses the perfect technology assumption, which abstracts from limitations imposed by an implementation.
Statecharts describe object life cycles. Our semantics includes synchronous and asynchronous communication between objects
and creation and deletion of objects. Our tool support presents a graphical front-end to model checkers, making these tools
usable to people who are not specialists in model checking. The model-checking approach presented in this paper is embedded
in an informal but precise method for software requirements and design. We discuss some of our experiences with model checking.
Correspondence and offprint requests to: Rik Eshuis, Department of Computer Science, University of Twente, PO Box 217, 7500 AE Enschede, The Netherlands. Email: eshuis@cs.utwente.nl 相似文献
4.
Hubert Garavel Frédéric Lang Radu Mateescu Wendelin Serwe 《International Journal on Software Tools for Technology Transfer (STTT)》2013,15(2):89-107
CADP (Construction and Analysis of Distributed Processes) is a comprehensive software toolbox that implements the results of concurrency theory. Started in the mid-1980s, CADP has been continuously developed by adding new tools and enhancing existing ones. Today, CADP benefits from a worldwide user community, both in academia and industry. This paper presents the latest release, CADP 2011, which is the result of a considerable development effort spanning the last five years. The paper first describes the theoretical principles and the modular architecture of CADP, which has inspired several other recent model checkers. The paper then reviews the main features of CADP 2011, including compilers for various formal specification languages, equivalence checkers, model checkers, compositional verification tools, performance evaluation tools, and parallel verification tools running on clusters and grids. Finally, the paper surveys some significant case studies. 相似文献
5.
6.
The use of model checkers for automated software testing has received some attention in the literature: It is convenient because it allows fully automated generation of test suites for many different test objectives. On the other hand, model checkers were not originally meant to be used this way but for formal verification, so using model checkers for testing is sometimes perceived as a “hack”. Indeed, several drawbacks result from the use of model checkers for test case generation. If model checkers were designed or adapted to take into account the needs that result from the application to software testing, this could lead to significant improvements with regard to test suite quality and performance. In this paper we identify the drawbacks of current model checkers when used for testing. We illustrate techniques to overcome these problems, and show how they could be integrated into the model checking process. In essence, the described techniques can be seen as a general road map to turn model checkers into general purpose testing tools. 相似文献
7.
The BLAST static verification tool is one of the open-source verifiers of software written in C. The paper describes principles of BLAST implementation, the limitations revealed in the course of its practical use in the verification of the Linux operating system drivers, and an attempt to improve BLAST in the framework of the Linux Driver Verification (LDV) project [3]. 相似文献
8.
Domagoj Babić Alan J. Hu 《International Journal on Software Tools for Technology Transfer (STTT)》2009,11(4):325-338
Despite many advances, today’s software model checkers and extended static checkers still do not scale well to large code
bases when verifying properties that depend on complex interprocedural flow of data. An obvious approach to improve performance
is to exploit software structure. Although a tremendous amount of work has been done on exploiting structure at various levels
of granularity, the fine-grained shared structure among multiple verification conditions has been largely ignored. In this
paper, we formalize the notion of shared structure among verification conditions and propose a novel and efficient approach
to exploit this sharing by safely reusing facts learned while checking one verification condition to help solve the others.
Experimental results show that this approach can improve the performance of verification, even on path- and context-sensitive
and dataflow-intensive properties. 相似文献
9.
Yunja Choi 《Formal Methods in System Design》2007,30(3):199-216
Model checking has become a promising technique for verifying software and hardware designs; it has been routinely used in
hardware verification, and a number of case studies and industrial applications show its effectiveness in software verification
as well. Nevertheless, most existing model checkers are specialized for limited aspects of a system, where each of them requires
a certain level of expertise to use the tool in the right domain in the right way. Hardly any guideline is available on choosing
the right model checker for a particular problem domain, which makes adopting the technique difficult in practice, especially
for verifying software with high complexity.
In this work, we investigate the relative pitfalls and benefits of using the explicit model checker Spin on commercial Flight Guidance Systems (FGSs) at Rockwell-Collins, based on the author's prior experience with the use of
the symbolic model checker NuSMV on the same systems. This has been a question from the beginning of the project with Rockwell-Collins.
The challenge includes the efficient use of Spin for the complex synchronous mode logic with a large number of state variables, where Spin is known to be not particulary efficient. We present the way the Spin model is optimized to avoid the state space explosion problem and discuss the implication of the result. We hope our experience
can be a useful 21 reference for the future use of model checking in a similar domain. 相似文献
10.
11.
Pascal Cuoq Benjamin Monate Anne Pacalet Virgile Prevosto 《International Journal on Software Tools for Technology Transfer (STTT)》2011,13(5):405-417
We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies
specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory
locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky:
the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional
dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional
dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate
a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked
using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was
written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes
place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been
implemented on top of the WP plug-in in the development version of the tool. 相似文献
12.
Matthew B. Dwyer John Hatcliff Robby Venkatesh Prasad Ranganath 《Formal Methods in System Design》2004,25(2-3):199-240
Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems. In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on (a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lock-acquisition and release in a program (building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time over existing approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL?X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers. 相似文献
13.
This paper presents VyrdMC, a runtime verification tool we are building for concurrent software components. The correctness criterion checked by VyrdMC is refinement: Each execution of the implementation must be consistent with an atomic execution of the specification. VyrdMC combines testing, model checking, and Vyrd, the runtime refinement checker we developed earlier. A test harness first drives the component to a non-trivial state which serves as the starting state for a number of simple, very small multi-threaded test cases. An execution-based model checker explores for each test case all distinct thread interleavings while Vyrd monitors executions for refinement violations. This combined approach has the advantage of improving the coverage of runtime refinement checking at modest additional computational cost, since model checkers are only used to explore thread interleavings of a small, fixed test program. The visibility and detailed checking offered by using refinement as the correctness criterion differentiate our approach from simply being a restricted application of model checking. An important side benefit is the reduction in program instrumentation made possible if VyrdMC is built using a model checker with its own virtual machine, such as Java PathFinder [Guillaume Brat, Klaus Havelund, Seung-Joon Park, and Willem Visser. Model Checking Programs. In IEEE International Conference on Automated Software Engineering (ASE), September 2000]. We are investigating the use of two different model checkers for building VyrdMC: Java PathFinder, an explicit-state model checker and Verisoft, a “stateless” model checker [P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997]. 相似文献
14.
System quality is a key issue in modern systems development. Tool support is essential for checking the system quality efficiently. This is particularly true with respect to the dynamic interactions of the processes within a system. A first generation of checkers – model checkers – provide a basic technology for the verification of process-based systems.Conventional model checkers bear two drawbacks concerning mainly their user-friendliness which impede their broad application. First, model checkers in general do not support the graphical representation of rules (specifications). Although a model may be described with a graphical notation, the specification which has to be checked against the model is generally still text-based. This makes the usage of the checker difficult for process modeling experts. Second, the expressiveness concerning the verification model semantics to be checked is limited to states which are connected by transitions. However, many system development models (e.g. the business process model we use as example) embrace more element types. These are unsupported by the conventional model checkers resulting in a loss of verification precision.The checking system we present in this paper integrates both novelties: the graphical notation for a user-friendly specification and an extended specification language together with a corresponding verifier which supports the checking of many different types of elements (although the paper presents the approach with only two types). The integration is realized by an XML-based transformation system which links the graphical editor to the checking tool. 相似文献
15.
16.
Hendrik Post Carsten Sinz Wolfgang Küchlin 《Software Testing, Verification and Reliability》2009,19(2):155-172
Modular software model checking of large real‐world systems is known to require extensive manual effort in environment modelling and preparing source code for model checking. Avinux is a tool chain that facilitates the automatic analysis of Linux and especially of Linux device drivers. The tool chain is implemented as a plugin for the Eclipse IDE, using the source code bounded model checker CBMC as its backend. Avinux supports a verification process for Linux that is built upon specification annotations with SLICx (an extension of the SLIC language), automatic data environment creation, source code transformation and simplification, and the invocation of the verification backend. In this paper technical details of the verification process are presented: Using Avinux on thousands of drivers from various Linux versions led to the discovery of six new errors. In these experiments, Avinux also reduced the immense overhead of manual code preprocessing that other projects incurred. Copyright © 2008 John Wiley & Sons, Ltd. 相似文献
17.
18.
19.
A symbolic manipulator for automated verification of reactive systems with heterogeneous data types 总被引:1,自引:0,他引:1
In this paper, we present the design and implementation of the Composite Symbolic Library, a symbolic manipulator for model checking systems with heterogeneous data types. Our tool provides a common interface for different symbolic representations, such as BDDs, for representing Boolean logic formulas and polyhedral representations for linear arithmetic formulas. Based on this common interface, these data structures are combined using a disjunctive composite representation. We propose several heuristics for efficient manipulation of this composite representation and present experimental results that demonstrate their performance. We used an object-oriented design to implement the Composite Symbolic Library. We imported the CUDD library (a BDD library) and the Omega Library (a linear arithmetic constraint manipulator that uses polyhedral representations) to our tool by writing wrappers around them which conform to our symbolic representation interface. Our tool supports polymorphic verification procedures which dynamically select symbolic representations based on the input specification. Our symbolic representation library can be used as an interface between different symbolic libraries, model checkers, and specification languages. We expect our tool to be useful in integrating different tools and techniques for symbolic model checking, and in comparing their performance. 相似文献
20.
Model-driven development (MDD) deals with complexities of modern software development by using models. Their verification is one of the opportunities of MDD, since it can be performed in the early stages of the development. The prevailing trend in verification of MDD models has been to translate them to an input language of one of the existing tools, most notably model checkers. Such an approach has advantages; for instance, we can use tools that achieved a higher level of maturity, including SPIN, NuSMV and Java PathFinder. However, the input languages of model checkers are typically not compatible with MDD models, which can make the translations very complex and difficult to maintain. Moreover, it is more difficult to take advantage of specific features of the structure and semantics of models to, e.g., speed up analysis. In this paper, we depart from the translational trend and present more direct and dedicated approach. We use an MDD language, namely UML-RT (used in IBM Rational Software Architect RealTime Edition), and we introduce a verification method built around its main features such as hierarchical structures, action code and asynchronous communication. In our method we use a formalization tailored to UML-RT models. This enables very easy transformation of models, but also reduces the necessary translations of verification results and directly supports the most important features of UML-RT. The proposed method includes an on-the-fly model checking algorithm based on the original CTL labeling. This algorithm is further optimized to include lazy composition. In the paper, we present all necessary components of the checking algorithms. Additionally, we also show the results of experiments with our implementation using several UML-RT models and CTL formulas. The experiments provide some evidence of the viability of a language-specific analysis of MDD models and of the effectiveness of our optimizations in certain cases. 相似文献