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

Efficient software model checking of data structure properties

ACM SIGPLAN NOTICES 2006年第10期41卷 363-381页

作者： Darga, Paul T. Boyapati, Chandrasekhar Univ Michigan Dept Elect & Comp Sci Ann Arbor MI 48109 USA

This paper presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate all red-black tree states (within some given bounds) and check every red-black tree operation (such as insert, delete, or lookup) on every red-black tree state. Our key idea is as follows. As our checker checks a red-black tree operation o on a red-black tree state s, it uses program analysis techniques to identify other red-black tree states s'(1), s'(2), ... , s'(k) on which the operation o behaves similarly. Our analyses guarantee that if o executes correctly on s, then o will execute correctly on every s'(i). Our checker therefore does not need to check o on any s'(i) once it checks o on s. It thus safely prunes those state transitions from its search space, while still achieving complete test coverage within the bounded domain. Our preliminary results show orders of magnitude improvement over previous approaches. We believe our techniques can make model checking significantly faster, and thus enable checking of much larger programs and complex program properties than currently possible.

关键词： verification reliability languages software model checking program analysis

来源：评论

学校读者我要写书评

暂无评论

Translation-based Verification of Web Services Composition via ZING

Translation-based Verification of Web Services Composition v...

引用

2010 International Conference on Intelligent Computing and Integrated Systems

作者： Xiangyu Luo~(1,2),Jingjing Lu~1,Kaile Su~(3,4),Rongsheng Dong~1 1 School of Computer and Control,Guilin University of Electronic and Technology,Guilin,China 2 School of software,Tsinghua University,Beijing,China 3 Key laboratory of High Confidence software Technologies(Peking University),Ministry of Education,Beijing,China 4 Institute for Integrated and Intelligent Systems,Griffith University,Brisbane,Australia

BPEL4WS(BPEL for short) is a standard business process execution language for Web services *** formally verify the correctness and reliability of Web services compositions,we propose an Input/Output Labelled Transition System(I/OLTS) as the intermediate formal model,which is well adapted to model BPEL constructs and handle faults, events,terminations,message correlation and *** be able to automatically verify Web services compositions via a model checker,we first develop a translation procedure to translate BPEL language into I/OLTS,and then develop another translation procedure to translate the I/OLTS model into the input language of ZING,a software model checker developed by *** translation-based verification process for Web services composition is illustrated by a case study.

关键词： Web services BPEL4WS I/OLTS software model checking ZING

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Adding Nesting Structure to Words

引用

JOURNAL OF THE ACM 2009年第3期56卷 16:1-16:43页

作者： Alur, Rajeev Madhusudan, P. Univ Penn Dept Comp & Informat Sci Philadelphia PA 19104 USA Univ Illinois Dept Comp Sci Urbana IL 61801 USA

We propose the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include executions of structured programs, annotated linguistic data, and HTML/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata-finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts;the class is closed under union, intersection, complementation, concatenation, Kleene-*, prefixes, and language homomorphisms;membership, emptiness, language inclusion, and language equivalence are all decidable;and definability in monadic second order logic corresponds exactly to finite-state recognizability. We also consider regular languages of infinite nested words and show that the closure properties, MSO-characterization, and decidability of decision problems carry over. The linear encodings of nested words give the class of visibly pushdown languages of words, and this class lies between balanced languages and deterministic context-free languages. We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words ( or equivalently, a visibly pushdown language), and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics. We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they co

关键词： Theory Verification Pushdown automata software model checking tree automata XML processing

来源：评论

学校读者我要写书评

暂无评论

software Reliability through Theorem Proving

引用

DEFENCE SCIENCE JOURNAL 2009年第3期59卷 314-317页

作者： Murthy, S. G. K. Sekharam, K. Raja Def Res & Dev Lab DRDL Grp 4&5 Hyderabad Andhra Pradesh India

Improving software reliability of mission-critical systems is widely recognised as one of the major challenges. Early detection of errors in software requirements, designs and implementation, need rigorous verification and validation techniques. Several techniques comprising static and dynamic testing approaches are used to improve reliability of mission critical software; however it is hard to balance development time and budget with software reliability. Particularly using dynamic testing techniques, it is hard to ensure software reliability, as exhaustive testing is not possible. On the other hand, formal verification techniques utilise mathematical logic to prove correctness of the software based on given specifications, which in turn improves the reliability of the software. Theorem proving is a powerful formal verification technique that enhances the software reliability for mission- critical aerospace applications. This paper discusses the issues related to software reliability and theorem proving used to enhance software reliability through formal verification technique, based on the experiences with STeP tool, using the conventional and internationally accepted methodologies, models, theorem proving techniques available in the tool without proposing a new model.

关键词： software reliability formal methods software testing software model checking software theorem proving stanford temporal theorem prover (STeP) autopilot software

来源：评论

学校读者我要写书评

暂无评论

Cache-based model checking of Networked Applications: From Linear to Branching Time 09

Cache-based Model Checking of Networked Applications: From L...

引用

24th IEEE/ACM International Conference on Automated software Engineering

作者： Artho, Cyrille Leungwattanakit, Watcharin Hagiya, Masami Tanabe, Yoshinori Yamamoto, Mitsuharu AIST Res Ctr Informat Secur Tokyo Japan Univ Tokyo Dept Comp Sci Tokyo Japan Chiba Univ Dept Math & Informat Chiba Japan

ISBN: (纸本)9780769538914

Many applications are concurrent and communicate over a network. The non-determinism in the thread and communication schedules makes it desirable to model check such systems. However, a simple state space exploration scheme is not applicable, as backtracking results in repeated communication operations. A cache-based approach solves this problem by hiding redundant communication operations from the environment. In this work, we propose a change from a linear-time to a branching-time cache, allowing us to relax restrictions in previous work regarding communication traces that differ between schedules. We successfully applied the new algorithm to real-life programs where a previous solution is not applicable.

关键词： software model checking software verification networking input/output caching

来源：评论

学校读者我要写书评

暂无评论

software model checking Based on Game Semantics and CSP

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年第6期128卷 105-125页

作者： Dimovski, Aleksandar Lazic, Ranko Univ Warwick Dept Comp Sci Coventry CV4 7AL England

We present an approach for software model checking based on game semantics and CSP. Open program fragments are compositionally modelled as CSP processes which represent their game semantics. This translation is performed by a prototype compiler. Observational equivalence and verification of properties are checked by traces refinement using the FDR tool. The effectiveness of our approach is evaluated on several examples.

关键词： software model checking Game semantics CSP process algebra FDR refinement checker

来源：评论

学校读者我要写书评

暂无评论

Efficient model checking of networked applications 46th

引用

46th International Conference on Tools in Europe

作者： Artho, Cyrille Leungwattanakit, Watcharin Hagiya, Masami Tanabe, Yoshinori AIST RCIS Tokyo Japan Univ Tokyo Tokyo 1138654 Japan AIST RCVS CVS Tokyo Japan

ISBN: (纸本)9783540698234

Most applications today communicate with other processes over a network. Such applications are often multi-threaded. The non-determinism in the thread and communication schedules makes it desirable to model check such applications. When model checking such a networked application, a simple state space exploration scheme is not applicable, as the process being model checked would repeat communication operations when revisiting a given state after backtracking. We propose a solution that encapsulates such operations in a caching layer that is capable of hiding redundant communication operations from the environment. This approach is both more portable and more scalable than other approaches, as only a single process executes inside the model checker.

关键词： software model checking network communication software testing caching

来源：评论

学校读者我要写书评

暂无评论

Memory model sensitive bytecode verification

引用

FORMAL METHODS IN SYSTEM DESIGN 2007年第3期31卷 281-305页

作者： Huynh, Thuan Quang Roychoudhury, Abhik Natl Univ Singapore Dept Comp Sci Singapore 117548 Singapore Univ Maryland Dept Comp Sci College Pk MD 20742 USA

Modern concurrent programming languages like C# and Java have a programming language level memory model, which captures the set of all allowed behaviors of programs on any implementation platform-uni- or multi-processor. Such a memory model is typically weaker than Sequential Consistency and allows reordering of operations within a program thread. Therefore, programs verified correct by assuming Sequential Consistency (that is, each thread proceeds in program order) may not behave correctly on certain platforms! One solution to this problem is to develop program checkers which are memory model sensitive. In this paper, we develop a bytecode level invariant checker for the programming language C#. Our checker identifies program states which are reached only because the C# memory model is more relaxed than Sequential Consistency. It employs partial order reduction strategies to speed up the search. These strategies are different from standard partial order reduction methods since our search also considers execution traces containing bytecode re-orderings. Furthermore, our checker identifies (a) operation re-orderings which cause undesirable states to be reached, and (b) simple program modifications-by inserting memory barrier operations-which prevent such undesirable re-orderings.

关键词： software model checking programming language memory models bytecode verification

来源：评论

学校读者我要写书评

暂无评论

MMC: the Mono model Checker

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第1期190卷 149-160页

作者： Ruys, Theo C. Aan de Brugh, Niels H. M. Univ Twente Fac EEMCS Formal Methods & Tools Grp Enschede Netherlands

The Mono model Checker (MMC) is a software model checker for CIL bytecode programs. MMC has been developed on the Mono platform. MMC is able to detect deadlocks and assertion violations in CIL programs. The design of MMC is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MMC is comparable to JPF. This paper introduces MMC and presents its main architectural characteristics.

关键词： software model checking verification MMC MONO,. NET CLI bytecode

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：