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

IEEE TRANSACTIONS ON software ENGINEERING 2009年第1期35卷 46-66页

作者： Zave, Pamela Cheung, Eric AT&T Labs Res Florham Pk NJ 07932 USA

In many IP media services, the media channels are point-to-point, dynamic and set up with the participation of one or more application servers, even though the media packets themselves travel directly between media end points. The application servers must be programmed so that the media behavior is globally correct, even though the servers may attempt to manipulate the same media channels concurrently and without knowledge of each other. Our proposed solution to this problem of compositional media control includes an architecture-independent descriptive model, a set of high-level programming primitives, a formal specification of their compositional semantics, a signaling protocol, an implementation, and a partial verification of correctness. The paper includes a performance analysis, a comparison to related work, and principles for making other networked applications more compositional.

关键词： Distributed applications domain-specific architectures protocol design protocol verification software/program verification networks streaming media multimedia services telecommunications feature interaction

来源：评论

学校读者我要写书评

暂无评论

Automatic detection and masking of nonatomic exception handling

引用

IEEE TRANSACTIONS ON software ENGINEERING 2004年第8期30卷 547-560页

作者： Fetzer, C Felber, P Högstedt, K Tech Univ Dresden Inst Syst Architecture Dept Comp Sci D-01062 Dresden Germany Inst EURECOM F-06904 Sophia Antipolis France AT&T Labs Res Florham Pk NJ 07932 USA

The development of robust software is a difficult undertaking and is becoming increasingly more important as applications grow larger and more complex. Although modern programming languages such as C++ and Java provide sophisticated exception handling mechanisms to detect and correct runtime error conditions, exception handling code must still be programmed with care to preserve application consistency. In particular, exception handling is only effective if the premature termination of a method due to an exception does not leave an object in an inconsistent state. We address this issue by introducing the notion of failure atomicity in the context of exceptions. We propose practical techniques to automatically detect and mask the nonatomic exception handling situations encountered during program execution. These techniques can be applied to applications written in various programming languages that support exceptions. We perform experimental evaluation on both C++ and Java applications to demonstrate the effectiveness of our techniques and measure the overhead that they introduce.

关键词： software engineering software/program verification reliability testing and debugging error handling and recovery reliability testing tools

来源：评论

学校读者我要写书评

暂无评论

Automated Capture of Experiment Context for Easier Reproducibility in Computational Research

引用

COMPUTING IN SCIENCE & ENGINEERING 2012年第4期14卷 48-56页

作者： Davison, Andrew P. Ctr Natl Rech Sci Unite Neurosci Informat & Complexite Neuroinformat Grp Orsay France

Published scientific research that relies on numerical computations is too often not reproducible. For computational research to become consistently and reliably reproducible, the process must become easier to achieve, as part of day-to-day research. A combination of best practices and automated tools can make it easier to create reproducible research.

关键词： reliability reusable libraries reusable software scientific computing software/program verification numerical calculation Scientific computing Automation Best Practices

来源：评论

学校读者我要写书评

暂无评论

The design of a multicore extension of the SPIN model checker

引用

IEEE TRANSACTIONS ON software ENGINEERING 2007年第10期33卷 659-674页

作者： Holzmann, Gerard J. Bosnacki, Dragan CALTECH Jet Prop Labs Lab Reliable Software Pasadena CA 91109 USA Eindhoven Univ Technol NL-5600 MB Eindhoven Netherlands

We describe an extension of the SPIN model checker for use on multicore shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can, in some cases, be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multicore algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code and are compatible with most existing verification modes such as partial order reduction, the verification of temporal logic formulas, bitstate hashing, and hash-compact compression.

关键词： software/program verification model checking models of computation logics and meanings of programs distributed programming

来源：评论

学校读者我要写书评

暂无评论

A taxonomy and catalog of runtime software-fault monitoring tools

引用

IEEE TRANSACTIONS ON software ENGINEERING 2004年第12期30卷 859-872页

作者： Delgado, N Gates, AQ Roach, S Microsoft Corp Bellevue WA 98007 USA Univ Texas Dept Comp Sci El Paso TX 79902 USA

A goal of runtime software-fault monitoring is to observe software behavior to determine whether it complies with its intended behavior. Monitoring allows one to analyze and recover from detected faults, providing additional defense against catastrophic failure. Although runtime monitoring has been in use for over 30 years, there is renewed interest in its application to fault detection and recovery, largely because of the increasing complexity and ubiquitous nature of software systems. This paper presents a taxonomy that developers and researchers can use to analyze and differentiate recent developments in runtime software fault-monitoring approaches. The taxonomy categorizes the various runtime monitoring research by classifying the elements that are considered essential for building a monitoring system, i.e., the specification language used to define properties;the monitoring mechanism that oversees the program's execution;and the event handler that captures and communicates monitoring results. After describing the taxonomy, the paper presents the classification of the software-fault monitoring systems described in the literature.

关键词： assertion checkers runtime monitors specification specification language survey software/program verification

来源：评论

学校读者我要写书评

暂无评论

A Taxonomy of Buffer Overflow Characteristics

引用

IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING 2012年第3期9卷 305-317页

作者： Bishop, Matt Engle, Sophie Howard, Damien Whalen, Sean Univ Calif Davis Dept Comp Sci Davis CA 95616 USA Univ San Francisco Dept Comp Sci San Francisco CA 94117 USA Knobbe Martens Olson & Bear LLP Irvine CA 92614 USA Columbia Univ Dept Comp Sci New York NY 10027 USA

Significant work on vulnerabilities focuses on buffer overflows, in which data exceeding the bounds of an array is loaded into the array. The loading continues past the array boundary, causing variables and state information located adjacent to the array to change. As the process is not programmed to check for these additional changes, the process acts incorrectly. The incorrect action often places the system in a nonsecure state. This work develops a taxonomy of buffer overflow vulnerabilities based upon characteristics, or preconditions that must hold for an exploitable buffer overflow to exist. We analyze several software and hardware countermeasures to validate the approach. We then discuss alternate approaches to ameliorating this vulnerability.

关键词： Protection mechanisms software/program verification security and privacy arrays

来源：评论

学校读者我要写书评

暂无评论

Automated verification of an audio-control protocol using UPPAAL

引用

JOURNAL OF LOGIC AND ALGEBRAIC programMING 2002年 52-3卷 163-181页

作者： Bengtsson, J Griffioen, WOD Kristoffersen, KJ Larsen, KG Larsson, F Pettersson, P Yi, W Uppsala Univ Dept Informat Technol S-75105 Uppsala Sweden Dept Software Technol NL-1090 GB Amsterdam Netherlands IT Univ Copenhagen DK-2400 Copenhagen NV Denmark Aalborg Univ BRICS Dept Comp Sci DK-9220 Aalborg Denmark

In this paper we present a case-study in which the tool UPPAAL is extended and applied to verify an audio-control protocol developed by Philips. The size of the protocol studied in this paper is significantly larger than case studies, including various abstract versions of the same protocol without bus-collision handling, reported previously in the community of real-time verification. We have checked that the protocol will function correctly if the timing error of its components is bound to +/-5% and incorrectly if the error is +/-6%. In addition, using UPPAAL's ability of generating diagnostic traces, we have studied an erroneous version of the protocol actually implemented by Philips. and constructed a possible execution sequence explaining the error. During the case-study. UPPAAL was extended with the notion of committed locations. It allows for accurate modelling of atomic behaviours, and more importantly, it is utilised to guide the state-space exploration of the model checker to avoid exploring unnecessary interleavings of independent transitions. Our experimental results demonstrate considerable time and space-savings of the modified model checking algorithm. In fact, due to the huge time and memory-requirement. it was impossible to check a simple reachability property, of the protocol before the introduction of committed locations, and now, it takes only seconds. (C) 2002 Published by Elsevier Science Inc.

关键词： protocol verification requirements/specifications design tools and techniques software/program verification

来源：评论

学校读者我要写书评

暂无评论

Tool support for verifying UML activity diagrams

引用

IEEE TRANSACTIONS ON software ENGINEERING 2004年第7期30卷 437-447页

作者： Eshuis, R Wieringa, R Eindhoven Univ Technol Dept Technol Management NL-5600 MB Eindhoven Netherlands Univ Twente Dept Comp Sci NL-7500 AE Enschede Netherlands

We describe a tool that supports verification of workflow models specified in UML activity diagrams. The tool translates an activity diagram into an input format for a model checker according to a mathematical semantics. With the model checker, arbitrary propositional requirements can be checked against the input model. If a requirement fails to hold, an error trace is returned by the model checker, which our tool presents by highlighting a corresponding path in the activity diagram. We summarize our formal semantics, discuss the techniques used to reduce an infinite state space to a finite one, and motivate the need for strong fairness constraints to obtain realistic results. We define requirement-preserving rules for state space reduction. Finally, we illustrate the whole approach with a few example verifications.

关键词： analysis tools software/program verification model checking state diagrams workflow management

来源：评论

学校读者我要写书评

暂无评论

Assessing architectural drift in commercial software development: a case study

引用

software-PRACTICE & EXPERIENCE 2011年第1期41卷 63-86页

作者： Rosik, Jacek Le Gear, Andrew Buckley, Jim Babar, Muhammad Ali Connolly, Dave Univ Limerick Limerick Ireland Nomura Plc London England IT Univ Copenhagen Copenhagen Denmark IBM Dublin Software Lab Dublin Ireland

Objectives: software architecture is perceived as one of the most important artefacts created during a system's design. However, implementations often diverge from their intended architectures: a phenomenon called architectural drift. The objective of this research is to assess the occurrence of architectural drift in the context of de novo software development, to characterize it, and to evaluate whether its detection leads to inconsistency removal. Method: An in vivo, longitudinal case study was performed during the development of a commercial software system, where an approach based on Reflexion Modelling was employed to detect architectural drift. Observation and think-aloud data, captured during the system's development, were assessed for the presence and types of architectural drift. When divergences were identified, the data were further analysed to see if identification led to the removal of these divergences. Results: The analysed system diverged from the intended architecture, during the initial implementation of the system. Surprisingly however, this work showed that Reflexion Modelling served to conceal some of the inconsistencies, a finding that directly contradicts the high regard that this technique enjoys as an architectural evaluation tool. Finally, the analysis illustrated that detection of inconsistencies was insufficient to prompt their removal, in the small, informal team context studied. Conclusions: Although the utility of the approach for detecting inconsistencies was demonstrated in most cases, it also served to hide several inconsistencies and did not act as a trigger for their removal. Hence additional efforts must be taken to lessen architectural drift and several improvements in this regard are suggested. Copyright (C) 2010 John Wiley & Sons, Ltd.

关键词： software/program verification architecture consistency architecture degeneration reflection models

来源：评论

学校读者我要写书评

暂无评论

Using hammock graphs to structure programs

引用

IEEE TRANSACTIONS ON software ENGINEERING 2004年第4期30卷 231-245页

作者： Zhang, F D'Hollander, EH Platform Comp Inc Markham ON L3R 3T7 Canada Univ Ghent Dept Elect & Informat Syst B-9000 Ghent Belgium

Advanced computer architectures rely mainly on compiler optimizations for parallelization, vectorization, and pipelining. Efficient code generation is based on a control dependence analysis to find the basic blocks and to determine the regions of control. However, unstructured branch statements, such as jumps and goto's, render the control flow analysis difficult, time-consuming, and result in poor code generation. Branches are part of many programming languages and occur in legacy and maintenance code as well as in assembler, intermediate languages, and byte code. A simple and effective technique is presented to convert unstructured branches into hammock graph control structures. Using three basic transformations, an equivalent program is obtained in which all control statements have a well-defined scope. In the interest of predication and branch prediction, the number of control variables has been minimized, thereby allowing a limited code replication. The correctness of the transformations has been proven using an axiomatic proof rule system. With respect to previous work, the algorithm is simpler and the branch conditions are less complex, making the program more readable and the code generation more efficient. Additionally, hammock graphs define single entry single exit regions and therefore allow localized optimizations. The restructuring method has been implemented into the parallelizing compiler FPT and allows to extract parallelism in unstructured programs. The use of hammock graph transformations in other application areas such as vectorization, decompilation, and assembly program restructuring is also demonstrated.

关键词： program transformation structured programming compilers optimization parallel processing software/program verification correctness proofs

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：