ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    facet.materialart.
    Unknown
    Directed Incremental Symbolic Execution (2011)
    In:  CASI
    Details
    Publication Date: 2019-07-27
    Description: The last few years have seen a resurgence of interest in the use of symbolic execution -- a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution and other path-sensitive analysis techniques to large systems remains challenging despite recent algorithmic and technological advances. An alternative to solving the problem of scalability is to reduce the scope of the analysis. One approach that is widely studied in the context of regression analysis is to analyze the differences between two related program versions. While such an approach is intuitive in theory, finding efficient and precise ways to identify program differences, and characterize their effects on how the program executes has proved challenging in practice. In this paper, we present Directed Incremental Symbolic Execution (DiSE), a novel technique for detecting and characterizing the effects of program changes. The novelty of DiSE is to combine the efficiencies of static analysis techniques to compute program difference information with the precision of symbolic execution to explore program execution paths and generate path conditions affected by the differences. DiSE is a complementary technique to other reduction or bounding techniques developed to improve symbolic execution. Furthermore, DiSE does not require analysis results to be carried forward as the software evolves -- only the source code for two related program versions is required. A case-study of our implementation of DiSE illustrates its effectiveness at detecting and characterizing the effects of program changes.
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN3850 , ARC-E-DAA-TN3025 , NF1676L-11683 , 32nd ACM SIGPLAN Conference on Programming; 4-8- Jun. 2011; San Jose, CA; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 2
    facet.materialart.
    Unknown
    Property Differencing for Incremental Checking (2014)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: This paper introduces iProperty, a novel approach that facilitates incremental checking of programs based on a property di erencing technique. Speci cally, iProperty aims to reduce the cost of checking properties as they are initially developed and as they co-evolve with the program. The key novelty of iProperty is to compute the di erences between the new and old versions of expected properties to reduce the number and size of the properties that need to be checked during the initial development of the properties. Furthermore, property di erencing is used in synergy with program behavior di erencing techniques to optimize common regression scenarios, such as detecting regression errors or checking feature additions for conformance to new expected properties. Experimental results in the context of symbolic execution of Java programs annotated with properties written as assertions show the e ectiveness of iProperty in utilizing change information to enable more ecient checking.
    Keywords: Computer Programming and Software
    Type: NF1676L-17478 , International Conference on Software Engineering; May 31, 2014 - Jun 07, 2014; Hyderabad; India
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 3
    facet.materialart.
    Unknown
    Development Context Driven Change Awareness and Analysis Framework (2014)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: Recent work on workspace monitoring allows conflict prediction early in the development process, however, these approaches mostly use syntactic differencing techniques to compare different program versions. In contrast, traditional change-impact analysis techniques analyze related versions of the program only after the code has been checked into the master repository. We propose a novel approach, De- CAF (Development Context Analysis Framework), that leverages the development context to scope a change impact analysis technique. The goal is to characterize the impact of each developer on other developers in the team. There are various client applications such as task prioritization, early conflict detection, and providing advice on testing that can benefit from such a characterization. The DeCAF framework leverages information from the development context to bound the iDiSE change impact analysis technique to analyze only the parts of the code base that are of interest. Bounding the analysis can enable DeCAF to efficiently compute the impact of changes using a combination of program dependence and symbolic execution based approaches.
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN13719 , International Conference on Software Engineering, New Ideas and Emerging Results (NIER) 2013; May 31, 2014 - Jun 07, 2014; Hyderabad; India
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 4
    facet.materialart.
    Unknown
    A Change Impact Analysis to Characterize Evolving Program Behaviors (2012)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: Change impact analysis techniques estimate the potential effects of changes made to software. Directed Incremental Symbolic Execution (DiSE) is an intraprocedural technique for characterizing the impact of software changes on program behaviors. DiSE first estimates the impact of the changes on the source code using program slicing techniques, and then uses the impact sets to guide symbolic execution to generate path conditions that characterize impacted program behaviors. DiSE, however, cannot reason about the flow of impact between methods and will fail to generate path conditions for certain impacted program behaviors. In this work, we present iDiSE, an extension to DiSE that performs an interprocedural analysis. iDiSE combines static and dynamic calling context information to efficiently generate impacted program behaviors across calling contexts. Information about impacted program behaviors is useful for testing, verification, and debugging of evolving programs. We present a case-study of our implementation of the iDiSE algorithm to demonstrate its efficiency at computing impacted program behaviors. Traditional notions of coverage are insufficient for characterizing the testing efforts used to validate evolving program behaviors because they do not take into account the impact of changes to the code. In this work we present novel definitions of impacted coverage metrics that are useful for evaluating the testing effort required to test evolving programs. We then describe how the notions of impacted coverage can be used to configure techniques such as DiSE and iDiSE in order to support regression testing related tasks. We also discuss how DiSE and iDiSE can be configured for debugging finding the root cause of errors introduced by changes made to the code. In our empirical evaluation we demonstrate that the configurations of DiSE and iDiSE can be used to support various software maintenance tasks
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN5972 , 28th IEEE International Conference on Software; Sep 23, 2012 - Sep 30, 2012; Trento; Italy
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 5
    facet.materialart.
    Unknown
    Improving Coverage of Test Cases Generated by Symbolic PathFinder for Programs with Loops (2014)
    In:  CASI
    Details
    Publication Date: 2019-07-20
    Description: Symbolic execution is a program analysis technique that is used for many purposes, one of which is test-case generation. For loop-free programs, this generates a test-set that achieves path coverage. Program loops, however, imply exponential growth of the number of paths in the best case and non-termination in the worst case. In practice, the number of loop unwindings needs to be bounded for analysis. We consider symbolic execution in the context of the tool Symbolic Pathfinder. This tool extends the model-checker Java Pathfinder and relies on its bounded state-space exploration for termination. We present an implementation of k-bounded loop unwinding, which increases the amount of user-control over the symbolic execution of loops. Bounded unwinding can be viewed as a naive way to prune paths through loops. When using symbolic execution for test-case generation, naively pruning paths is likely at the cost of coverage. In order to improve coverage of branches within a loop body, we present a technique that semi-automatically concretizes variables used in a loop. The basic technique is limited and we therefore present annotations to manually steer symbolic execution towards certain branches, as well as ideas on how the technique can be extended to be more widely applicable.
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN19779 , Java PathFinder Workshop 2014; Nov 07, 2014; Salt Lake City, UT; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 6
    facet.materialart.
    Unknown
    Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites (2015)
    In:  CASI
    Details
    Publication Date: 2019-08-13
    Description: Structural coverage metrics have traditionally categorized code as either covered or uncovered. Recent work presents a stronger notion of coverage, checked coverage, which counts only statements whose execution contributes to an outcome checked by an oracle. While this notion of coverage addresses the adequacy of the oracle, for Model-Based Development of safety critical systems, it is still not enough; we are also interested in how much of the oracle is covered, and whether the values of program variables are masked when the oracle is evaluated. Such information can help system engineers identify missing requirements as well as missing test cases. In this work, we add to the idea of checked coverage an analysis of requirements coverage to help provide insight to engineers as to whether the requirements or the test suite need to be improved. We implement our approach based on a dynamic backward slicing technique and evaluate it on several systems developed in Simulink. The results of our preliminary study show that even for systems with comprehensive test suites and good sets of requirements, our approach can identify cases where more tests or more requirements are needed to improve coverage numbers.
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN21000 , NASA Formal Methods International Symposium (NFM 2015); Apr 27, 2015 - Apr 29, 2015; Pasadena, CA; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unknown
    A Flexible and Non-instrusive Approach for Computing Complex Structural Coverage Metrics (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: Software analysis tools and techniques often leverage structural code coverage information to reason about the dynamic behavior of software. Existing techniques instrument the code with the required structural obligations and then monitor the execution of the compiled code to report coverage. Instrumentation based approaches often incur considerable runtime overhead for complex structural coverage metrics such as Modified Condition/Decision (MC/DC). Code instrumentation, in general, has to be approached with great care to ensure it does not modify the behavior of the original code. Furthermore, instrumented code cannot be used in conjunction with other analyses that reason about the structure and semantics of the code under test. In this work, we introduce a non-intrusive preprocessing approach for computing structural coverage information. It uses a static partial evaluation of the decisions in the source code and a source-to-bytecode mapping to generate the information necessary to efficiently track structural coverage metrics during execution. Our technique is flexible; the results of the preprocessing can be used by a variety of coverage-driven software analysis tasks, including automated analyses that are not possible for instrumented code. Experimental results in the context of symbolic execution show the efficiency and flexibility of our nonintrusive approach for computing code coverage information
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN21155 , International Conference on Software Engineering; May 16, 2015 - May 24, 2015; Florence; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unknown
    Generalized Abstract Symbolic Summaries (2009)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: Current techniques for validating and verifying program changes often consider the entire program, even for small changes, leading to enormous V&V costs over a program s lifetime. This is due, in large part, to the use of syntactic program techniques which are necessarily imprecise. Building on recent advances in symbolic execution of heap manipulating programs, in this paper, we develop techniques for performing abstract semantic differencing of program behaviors that offer the potential for improved precision.
    Keywords: Computer Programming and Software
    Type: Proceedings of the First NASA Formal Methods Symposium; 46-55; NASA/CP-2009-215407
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unknown
    Maintaining the Health of Software Monitors (2013)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: Software health management (SWHM) techniques complement the rigorous verification and validation processes that are applied to safety-critical systems prior to their deployment. These techniques are used to monitor deployed software in its execution environment, serving as the last line of defense against the effects of a critical fault. SWHM monitors use information from the specification and implementation of the monitored software to detect violations, predict possible failures, and help the system recover from faults. Changes to the monitored software, such as adding new functionality or fixing defects, therefore, have the potential to impact the correctness of both the monitored software and the SWHM monitor. In this work, we describe how the results of a software change impact analysis technique, Directed Incremental Symbolic Execution (DiSE), can be applied to monitored software to identify the potential impact of the changes on the SWHM monitor software. The results of DiSE can then be used by other analysis techniques, e.g., testing, debugging, to help preserve and improve the integrity of the SWHM monitor as the monitored software evolves.
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN12287
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 10
    facet.materialart.
    Unknown
    Helping System Engineers Bridge the Peaks (2014)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: In our experience at NASA, system engineers generally follow the Twin Peaks approach when developing safety-critical systems. However, iterations between the peaks require considerable manual, and in some cases duplicate, effort. A significant part of the manual effort stems from the fact that requirements are written in English natural language rather than a formal notation. In this work, we propose an approach that enables system engineers to leverage formal requirements and automated test generation to streamline iterations, effectively "bridging the peaks". The key to the approach is a formal language notation that a) system engineers are comfortable with, b) is supported by a family of automated V&V tools, and c) is semantically rich enough to describe the requirements of interest. We believe the combination of formalizing requirements and providing tool support to automate the iterations will lead to a more efficient Twin Peaks implementation at NASA.
    Keywords: Computer Programming and Software
    Type: ARC-E-DAA-TN14285 , International Conference on Software Engineering; May 31, 2014 - Jun 07, 2014; Hyderabad; India|International Workshop on the Twin Peaks of Requirements and Architecture; Jun 01, 2014; Hyderabad; India
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...