检索结果-内蒙古大学图书馆

ACM COMPUTING SURVEYS 2009年第4期41卷 21:1-21:54页

作者： Jhala, Ranjit Majumdar, Rupak Univ Calif San Diego Dept Comp Sci & Engn La Jolla CA 92093 USA Univ Calif Los Angeles Los Angeles CA USA

We survey recent progress in software model checking.

关键词： Languages Verification Reliability software model checking enumerative and symbolic model checking abstraction counterexample-guided refinement safety liveness

来源：评论

学校读者我要写书评

暂无评论

software model checking for resources race

引用

CLUSTER COMPUTING-THE JOURNAL OF NETWORKS software TOOLS AND APPLICATIONS 2017年第1期20卷 179-193页

作者： Wang, Hong Zhang, Tao North China Elect Power Univ Sch Control & Comp Rd Beinong 2 Beijing 100206 Peoples R China Chinese Acad Sci Technol & Engn Ctr Space Utilizat Beijing 100096 Peoples R China

The difficulty of finding resources race is well known. Such errors are hard to be detected, because they often happen irregularly and reproduce difficultly. Especially, the kind race conflicts exist among processes, threads, and interrupts. This paper provided a novel approach to detect the resources race, namely software model checking. It constructed Boolean program and Promela models for resources race. Furthermore, the Promela models have been tested by using the model checker, SPIN. software model checking can detect resources race in concurrent program without running, although the program had used timing control or mutual exclusion lock to avoid the race. Furthermore, it can find deadlock also, if the program use the mutual locks in a wrong way.

关键词： Resources race software model checking Predicate abstraction Boolean program Premela SPIN

来源：评论

学校读者我要写书评

暂无评论

software model checking SystemC

引用

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS 2013年第5期32卷 774-787页

作者： Cimatti, Alessandro Narasamdya, Iman Roveri, Marco Fdn Bruno Kessler I-38050 Trento Italy

SystemC is an increasingly used language for writing executable specifications of systems-on-chip. The verification of SystemC, however, is a very difficult challenge. Simulation features great scalability, but can miss important defects. On the other hand, formal verification of SystemC is extremely hard because of the presence of threads, and the intricacies of the communication and scheduling mechanisms. In this paper, we explore formal verification for SystemC by means of software model checking techniques, which have demonstrated substantial progress in recent years. We propose an accurate model of SystemC and three complementary encodings of SystemC to finite-state processes, sequential and threaded programming models. We implement the proposed approaches in a tool chain and carry out a thorough experimental evaluation using several benchmarks taken from the literature on SystemC verification, and experimenting with different state-of-the-art software model checkers. The results clearly show the applicability and efficiency of the proposed approaches. In particular, the results show the effectiveness of the threaded and of the finite-model encodings to prove and disprove properties, respectively.

关键词： CEGAR sequentialization software model checking SystemC

来源：评论

学校读者我要写书评

暂无评论

software model checking: The VeriSoft approach

引用

FORMAL METHODS IN SYSTEM DESIGN 2005年第2期26卷 77-101页

作者： Godefroid, P Bell Labs Lucent Technol Lisle IL 60532 USA

Verification by state-space exploration, also often referred to as model checking, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communication protocols). Unfortunately, traditional model checking is restricted to the verification of properties of models, i.e., abstractions, of concurrent systems. We discuss in this paper how model checking can be extended to analyze arbitrary software, such as implementations of communication protocols written in programming languages like C or C++. We then introduce a search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code. During the past five years, VeriSoft has been applied successfully for analyzing several software products developed in Lucent Technologies, and has also been licensed to hundreds of users in industry and academia. We discuss applications, strengths and limitations of VeriSoft, and compare it to other approaches to software model checking, analysis and testing.

关键词： software model checking systematic testing program verification

来源：评论

学校读者我要写书评

暂无评论

software model checking for Distributed Systems with Selector-Based, Non-blocking Communication 13

Software Model Checking for Distributed Systems with Selecto...

引用

28th IEEE/ACM International Conference on Automated software Engineering (ASE)

作者： Artho, Cyrille Hagiya, Masami Potter, Richard Tanabe, Yoshinori Weitl, Franz Yamamoto, Mitsuharu AIST RISEC Amagasaki Hyogo Japan

ISBN: (纸本)9781479902156

Many modern software systems are implemented as client/server architectures, where a server handles multiple clients concurrently. Testing does not cover the outcomes of all possible thread and communication schedules reliably. software model checking, on the other hand, covers all possible outcomes but is often limited to subsets of commonly used protocols and libraries. Earlier work in cache-based software model checking handles implementations using socket-based TCP/IP networking, with one thread per client connection using blocking input/output. Recently, servers using non-blocking, selector-based input/output have become prevalent. This paper describes our work extending the Java PathFinder extension net-iocache to such software, and the application of our tool to modern server software.

关键词： software model checking caching software verification distributed systems non-blocking input/output selector-based input/output

来源：评论

学校读者我要写书评

暂无评论

software model checking of UDP-based Distributed Applications 2

Software Model Checking of UDP-based Distributed Application...

引用

International Symposium on Computing and Networking CANDAR

作者： Sebih, Nazim Weitl, Franz Artho, Cyrille Hagiya, Masami Tanabe, Yoshinori Yamamoto, Mitsuharu Univ Tokyo Tokyo Japan Chiba Univ Chiba Japan AIST RISEC Amagasaki Hyogo Japan Natl Inst Informat Tokyo Japan

ISBN: (纸本)9781479941520

We extend exhaustive verification of networked applications to applications using the User Datagram Protocol (UDP). UDP maximizes performance by omitting flow control and connection handling. High-performance services often offer a UDP mode in which they handle connections internally for optimal throughput. However, because UDP is unreliable (packets are subject to loss, duplication, and reordering), verification of UDP-based applications becomes an issue. Even though unreliable behavior occurs only rarely during testing, it often appears in a production environment due to a larger number of concurrent network accesses. Our tool systematically tests UDP-based applications by producing packet loss, duplication, and reordering for each packet. It is built on top of net-iocache for the Java PathFinder model checker. We have evaluated the performance of our tool in a multi-threaded client/server application and detected incorrectly handled packet duplicates in a file transfer client.

关键词： software model checking Java PathFinder Testing of Distributed Systems User Datagram Protocol Unreliable Network IO

来源：评论

学校读者我要写书评

暂无评论

software model checking with Uninterpreted Functions

Software Model Checking with Uninterpreted Functions

引用

作者： Bueno, Denis University of Michigan

学位级别：博士

software model checkers attempt to algorithmically synthesize an inductive proof that a piece of software is safe. Such proofs are composed of complex logical assertions about program variables and control structures, and are computationally expensive to produce. Our unifying motivation is to increase the efficiency of verifying software control behavior despite its dependency on data. Control properties include important topics such as mutual exclusion, safe privilege elevation, and proper usage of networking and other APIs. These concerns motivate our techniques and evaluations. Our approach integrates an efficient abstraction procedure based on the logic of equality with uninterpreted functions (EUF) into the core of a modern model checker. Our checker, called euforia, targets control properties by treating a program’s data operations and relations as uninterpreted functions and predicates, respectively. This reduces the cost of building inductive proofs, especially for verifying control relationships in the presence of complex but irrelevant data processing. We show that our method is sound and terminates. We provide a ground-up implementation and evaluate the abstraction on a variety of software verification benchmarks. We show how to extend this abstraction to memory-manipulating programs. By judicious abstraction of array operations to EUF, we show that we can directly reason about array reads and adaptively learn lemmas about array writes leading to significant performance improvements over existing approaches. We show that our abstraction of array operations completely eliminates much of the array theory reasoning otherwise required. We report on experiments with and without abstraction and compare our checker to the state of the art. Programs with procedures pose unique difficulties and opportunities. We show how to retrofit a model checker not supporting procedures so that it supports modular analysis of programs with non-recursive procedures. This t

关键词： software model checking Equality with uninterpreted functions Thesis

来源：评论

学校读者我要写书评

暂无评论

Towards automated software model checking using graph transformation systems and Bogor

引用

Journal of Zhejiang University-Science A(Applied Physics & Engineering) 2009年第8期10卷 1093-1105页

作者： Vahid RAFE Adel T.RAHMANI Department of Computer Engineering Iran University of Science and Technology

Graph transformation systems have become a general formal modeling language to describe many models in software development *** modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software *** even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their *** this paper,we present a new solution to verify graph transformation systems using the Bogor model *** attributed graph grammars(AGG)-like graph transformation systems are translated to Bandera intermediate representation(BIR),the input language of Bogor,and Bogor verifies the model against some interesting properties defined by combining linear temporal logic(LTL) and special-purpose graph *** results are encouraging,showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.

关键词： Graph transformation Verification Bogor Attributed graph grammars （AGG） software model checking

来源：评论

学校读者我要写书评

暂无评论

Modular software model checking for Distributed Systems

引用

IEEE TRANSACTIONS ON software ENGINEERING 2014年第5期40卷 483-501页

作者： Leungwattanakit, Watcharin Artho, Cyrille Hagiya, Masami Tanabe, Yoshinori Yamamoto, Mitsuharu Takahashi, Koichi Chiba Univ Dept Math & Informat Fac Sci Inage Ward Chiba 2630022 Japan Natl Inst Adv Ind Sci & Technol ogy AIST Res Inst Secure Syst Amagasaki Hyogo 6610974 Japan Univ Tokyo Dept Comp Sci Bunkyo Ku Tokyo 1138656 Japan Res Org Informat & Syst Natl Inst Informat Chiyoda Ku Tokyo 1018430 Japan

Distributed systems are complex, being usually composed of several subsystems running in parallel. Concurrent execution and inter-process communication in these systems are prone to errors that are difficult to detect by traditional testing, which does not cover every possible program execution. Unlike testing, model checking can detect such faults in a concurrent system by exploring every possible state of the system. However, most model-checking techniques require that a system be described in a modeling language. Although this simplifies verification, faults may be introduced in the implementation. Recently, some model checkers verify program code at runtime but tend to be limited to stand-alone programs. This paper proposes cache-based model checking, which relaxes this limitation to some extent by verifying one process at a time and running other processes in another execution environment. This approach has been implemented as an extension of Java PathFinder, a Java model checker. It is a scalable and promising technique to handle distributed systems. To support a larger class of distributed systems, a checkpointing tool is also integrated into the verification system. Experimental results on various distributed systems show the capability and scalability of cache-based model checking.

关键词： software model checking software verification distributed systems checkpointing

来源：评论

学校读者我要写书评

暂无评论

Towards automatic software model checking of thousands of Linux modules-a case study with Avinux

引用

software TESTING VERIFICATION & RELIABILITY 2009年第2期19卷 155-172页

作者： Post, Hendrik Sinz, Carsten Kuechlin, Wolfgang Univ Tubingen Symbol Computat Grp Tubingen Germany

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 (C) 2008 John Wiley & Sons, Ltd.

关键词： software model checking integration and application of formal methods operating systems software verification model checking case study

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：