Browsing by Author "ROYCHOUDHURY, Abhik"

Now showing 1 - 14 of 14
  • No Thumbnail Available
    Item
    Automated Path Generation for Software Fault Localization
    (2005-06-15T06:31:20Z) WANG, Tao; ROYCHOUDHURY, Abhik
    Localizing the cause(s) of an observable error lies at the heart of program debugging. Fault localization often proceeds by comparing the failing program run with some ``successful'' run (a run which does not demonstrate the error). An issue here is to generate or choose a ``suitable'' successful run; this task is often left to the programmer. In this paper, we present an efficient technique where the construction of the successful run as well its comparison with the failing run is automated. Our method constructs a successful program run which is close to the failing run in terms of a distance metric capturing control flow. The distance metric takes into account the sequence of statements executed in the two runs, and not just the set of statements executed. We use the distance metric to locate ``similar'' branch instances which appear in the failing and successful run with different outcomes. The program statements for such branches are returned as bug report. In our experiments with the Siemens benchmark suite we found that the quality of our bug report compares well with those produced by existing fault localization approaches where the programmer manually provides or chooses a successful run.
  • No Thumbnail Available
    Item
    Comprehensive Test Suite Augmentation
    (2011-11-08T07:27:54Z) BÖHME, Marcel; ROYCHOUDHURY, Abhik
    Test Suite Augmentation (TSA) is based on the assumption that an existing test suite T already determines whether a program P works properly. When P evolves to P0, a comprehensive set of test cases that witness the changed behavior shall be generated and augmented to T. We observe that a syntactic change may be propagated in different ways, thereby manifesting itself as different semantic changes (in terms of observable program behavior). We present a path exploration technique that seeks to generate one change revealing test case for every semantic change, rather than generate multiple test cases which execute the same change and propagate it in the same fashion to the program output. Our change-based path exploration technique 1) finds all paths that execute at least one changed statement, 2) finds all paths along which the impact of a syntactic change is propagated to at least one output statement and 3) generates for both programs P and P0 a comprehensive number of test cases, each of which exposes a different semantic change. If time is bounded during test generation, the semantic difference is computed over those change partitions that have been explored. Our method is not restricted by the number of changes across the two program versions being analyzed - there can be multiple changes across the program versions. The results from our experiments suggest that by covering the syntactic changes, or even by considering possible ways of propagating the effects of these syntactic changes - we cannot hope to uncover all possible differences in behavior across two program versions. In other words, analysis of both program versions is needed for generating a comprehensive new set of tests which can augment the test suite of the old program version. For our subject programs, our method of change execution, change propagation and semantic differencing, yields 6 times as many change-revealing test cases as opposed to tests generated by covering syntactic changes.
  • No Thumbnail Available
    Item
    Dynamic Slicing on Java Bytecode Traces
    (2007-03-19) WANG, Tao; ROYCHOUDHURY, Abhik
    Dynamic slicing is a well-known technique for program analysis, debugging and understanding. Given a program P and input I, it finds all program statements which directly/indirectly affect the values of some variables' occurrences when P is executed with I. In this paper, we develop a dynamic slicing method for sequential Java programs. Our technique proceeds by backwards traversal of the bytecode trace produced by an input I in a given program P. Since such traces can be huge, we use results from data compression to compactly represent bytecode traces. The major space savings in our method come from the optimized representation of (a) data addresses used as operands by memory reference bytecodes, and (b) instruction addresses used as operands by control transfer bytecodes. We show how dynamic slicing algorithms can directly traverse our compact bytecode traces without resorting to costly decompression. We also extend our dynamic slicing algorithm to perform ``relevant slicing''; th...
  • No Thumbnail Available
    Item
    Interacting Process Classes
    (2005-09-07T06:47:59Z) GOEL, Ankit; SUN, Meng; ROYCHOUDHURY, Abhik; THIAGARAJAN, P. S.
    Many reactive control systems consist of a large number of similar interacting objects; these objects can be often grouped into classes. Such interacting process classes appear in telecommunication, transportation and avionics domains. In this paper, we propose a modeling and simulation technique for interacting process classes. Our modeling style uses well-known UML notations to capture behavior. In particular, the control flow of a process class is captured by a state diagram, unit interactions between process objects by sequence diagrams and the structural relations are captured via class diagrams. The key feature of our approach is that our simulation is symbolic. We dynamically group together objects of the same class based on their past behavior. This leads to a simulation strategy that is both time and memory efficient and we demonstrate this on well-studied non-trivial examples of reactive systems. We also use our simulator for debugging realistic designs such as NASA's CTAS weather monitoring system.
  • No Thumbnail Available
    Item
    Managing Tenants in a Multi-tenant SaaS
    (2010-10-28T03:38:36Z) JU, Lei; BANERJEE, Ansuman; ROYCHOUDHURY, Abhik; SENGUPTA, Bikram
    A multi-tenant software as a service (SaaS) system has to meet the needs of several tenant organizations, which connect to the system to utilize its services. To leverage economies of scale through reuse, a SaaS vendor would, in general, like to drive commonality amongst the requirements across tenants. However, many tenants will also come with some custom requirements that may be a prerequisite for them to adopt the SaaS system. These requirements then need to be addressed by evolving the SaaS system in a controlled manner, while still supporting the requirements of existing tenants. In this paper, we study the challenges associated with engineering multi-tenant SaaS systems and develop a framework to help evolve and validate such systems in a systematic manner. We adopt an intuitive formal model of services. We show that the proposed formalism is easily amenable to tenant requirement analysis and provides a systematic way to support multiple tenant onboarding and diverse service management. We perform a substantial case study of an online conference management system.
  • No Thumbnail Available
    Item
    Modeling Out-of-Order Processors for WCET Analysis
    (2005-09-13T09:13:58Z) LI, Xianfeng; ROYCHOUDHURY, Abhik; MITRA, Tulika
    Estimating the Worst Case Execution Time (WCET) of a program on a given processor is important for the schedulability analysis of real-time systems. WCET analysis techniques typically model the timing effects of micro-architectural features in modern processors (such as the pipeline, cache, branch prediction, etc.) to obtain safe and tight estimates. In this paper, we model out-of-order processor pipelines for WCET analysis. The analysis is, in general, difficult even for a basic block (a sequence of instructions with single-entry and single-exit points) if some of the instructions have variable latencies. This is because the WCET of a basic block on out-of-order pipelines cannot be obtained by assuming maximum latencies of the individual instructions. Our timing estimation technique for a basic block proceeds by a fixed-point analysis of the time intervals at which the instructions enter/leave a pipeline stage. To extend our estimation to whole programs, we use Integer Linear Programming (ILP) to combine the timing estimates for basic blocks. Timing effects of instruction cache and branch prediction are also modeled within our pipeline analysis framework. This forms a combined timing analysis framework that captures out-of-order pipeline, cache, branch prediction as well as the mutual interaction among these micro-architectural features. The accuracy of our analysis is demonstrated via tight estimates obtained for several benchmarks.
  • No Thumbnail Available
    Item
    Path Exploration based on Symbolic Output
    (2011-03-17T06:36:18Z) QI, Dawei; NGUYEN, Hoang D. T.; ROYCHOUDHURY, Abhik
    Efficient program path exploration is important for many software engineering activities such as testing, debugging and verification. However, enumerating all paths of a program is prohibitively expensive. In this paper, we develop a partitioning of program paths based on the program output. Two program paths are placed in the same partition if they derive the output similarly, that is, the symbolic expression connecting the output with the inputs is the same in both paths. Our grouping of paths is gradually created by a smart path exploration. Our experiments show the benefits of the proposed path exploration in test-suite construction. Our path partitioning produces a semantic signature of a program — describing all the different symbolic expressions that the output can assume along different program paths. To reason about changes between program versions, we can therefore analyze their semantic signatures. In particular, we demonstrate the applications of our path partitioning in debugging of software regressions.
  • No Thumbnail Available
    Item
    Program Transformations for Predictable Cache Behavior
    (2009-05-25T06:47:26Z) HUYNH, Bach Khoa; JU, Lei; CHATTOPADHYAY, Sudipta; ROYCHOUDHURY, Abhik
    Real-time embedded software developers need to balance the dual (and seemingly conflicting) concerns of efficiency and predictability. Efficiency concerns are typically addressed by tuning the application and its underlying processing platform through a variety of techniques such as generating custom instructions in the instruction set, or configuring the processing platform. However, timing predictability remains a difficult goal to achieve, specifically in the presence of performance-enhancing micro-architectural features such as data caches. Presence of data caches can cause vast variation in the execution time for even programs with a single path. In this paper, we study a new approach to achieve predictable cache behavior (without large performance degradation) in data-intensive embedded applications. Our approach is to rewrite a given application into a “cache-efficient” style, where the data memory accesses are tracked and transformed to systematically reduce data cache conflicts. Our program transformation leads to lesser execution time variation in the transformed program (across program inputs as well as across cache configurations). We also develop a new Worst-case Execution Time (WCET) analysis method for data caches, and show that it leads to tighter WCET estimates for cache-efficient programs. Our experiments indicate that adopting the cache-efficient style of programming for data-intensive embedded software can help balance the dual concerns of efficiency and predictability.
  • No Thumbnail Available
    Item
    Safety Proofs of Presistence Analysis
    (2010-10-28T03:45:30Z) HUYNH, Bach Khoa; JU, Lei; ROYCHOUDHURY, Abhik
    Caches are widely used in modern computer systems to bridge the increasing gap between processor speed and memory access time. On the other hand, the presence of caches, especially data caches, complicates the static worst case execution time (WCET) analysis. Correctness and tightness of WCET estimates are of crucial importance for system level design of embedded systems. In this report, we show that the originally proposed persistence analysis is both unsafe and pessimistic for worst-case cache behavior modeling.We propose a new update and join functions for persistence analysis and prove their soundness. Furthermore, we extend the semantics of memory block persistence, and propose a scope-aware persistence analysis which combines access pattern analysis and abstract interpretation. The dynamic behavior of a memory access is captured by its temporal scope (the loop iterations where a given memory block is accessed for a given data reference) during address analysis. Temporal scopes as well as loop hierarchy structure (the static scopes) are integrated and utilized to achieve a more precise abstract cache state modeling. We also prove the correctness of the proposed new persistence analysis.
  • No Thumbnail Available
    Item
    Schedulability Analysis of MSC-based System Models
    (2007-10-23T01:40:39Z) JU, Lei; ROYCHOUDHURY, Abhik; CHAKRABORTY, Samarjit
    Message Sequence Charts (MSCs) are widely used for describing interaction scenarios between the components of a distributed system. Consequently, worst-case response time estimation and schedulability analysis of MSC-based speci.-cations form natural building blocks for designing distributed real-time systems. However, currently there exists a large gap between the timing and quantitative performance analysis techniques that exist in the real-time systems literature, and the modeling/speci.cation techniques that are advocated by the formal methods community. As a result, although a number of schedulability analysis techniques are known for a variety of task graph-based models, it is not clear if they can be used to effectively analyze standard speci.cation formalisms such as MSCs. In this work, we make an attempt to bridge this gap by proposing a schedulability analysis technique for MSC-based system speci.cations. We show that compared to existing timing analysis techniques for distributed real-time systems, our pro-posed analysis gives tighter results, which immediately translate to better system design and improved resource dimensioning. We illustrate the details of our analy-sis using a setup from the automotive electronics domain, which consist of two real-life application programs (that are naturally modeled using MSCs) running on a platform consisting of multiple electronic control units (ECUs) connected via a FlexRay bus.
  • No Thumbnail Available
    Item
    Security Analysis of Unmanned Aircraft Systems
    (2017-01-25T06:55:10Z) NGUYEN, Manh-Dung; DONG, Naipeng; ROYCHOUDHURY, Abhik
    Security is a big concern in widely adopting security critical systems, such as Unmanned Aerial Vehicles (UAV). To ensure security of a system, the rst step is to identify the required security properties as well as the potential attacks, i.e., security requirements. We identify a set of security requirements for UAV systems which is more complete and in more details than existing works. To facilitate formal analysis of a system against the set of requirements, we propose algorithms to automatically generate attack trees from the requirement set for the developers and designers to have a better understanding of the potential risks of a UAV system. Moreover, we propose an algorithm to automatically generate attack models from the attack tree and associate each attack model with the expected security properties. Given a UAV system model representing the honest behavior of participants, we are able to verify whether the system su ers from some potential attacks, by feeding the automatically generated attack models and the UAV system model to a model checker to verify the associated security properties.
  • No Thumbnail Available
    Item
    Software Change Contracts
    (2012-03-30T09:16:26Z) QI, Dawei; YI, Jooyong; ROYCHOUDHURY, Abhik
    Incorrect program changes including regression bugs, incorrect bugfixes, incorrect feature updates are pervasive in software. These incorrect program changes affect software quality and are difficult to detect/correct. In this paper, we propose the notion of “change contracts" to avoid incorrect program changes. Change contracts formally specify the intended effect of program changes. Incorrect program changes are detected when they are checked with respect to the change contracts. We design a change contract language for Java programs and a dynamic checking system for our change contract language. General guidelines as well as concrete examples are given to illustrate the usage of our change contracts. We conduct an user study to check the expressiveness of our change contract language and find that the language is expressive enough to capture a wide variety of real-life changes in three large software projects (Ant, JMeter, log4j). Finally, our contract checking system detects several real-life incorrect changes in these three software projects via runtime checking of the change contracts.
  • No Thumbnail Available
    Item
    Specification-driven Compact Test Suite Generation for Complex Processor Pipelines
    (2007-11-21) NGA, Dang T. Thanh; ROYCHOUDHURY, Abhik; MITRA, Tulika
    Testing of modern-day processors to achieve gate-level coverage is a complex activity. While VLSI testing methods are extremely useful, they are unaware of the micro-architectural features of the processor. Functional validation of a processor design through simulation of a suite of test programs is a common industrial practice. In this paper, we develop a high-level architectural specification driven methodology for systematic test suite generation. Our primary contributions are (1) a fully formal processor pipeline modeling framework based on Communicating Extended Finite State Machines and (2) on-the-fly exploration of the processor model to generate test program witnesses, with an aim to achieve complete state coverage. While we achieve 100% coverage, random test generation manages to cover as low as 10% of the state space with comparable sized test suite. Moreover, we achieve significant reduction in the test-suite size compared to previously studied formal approaches that rely on querying an external model checker for test generation.
  • No Thumbnail Available
    Item
    Tenant Onboarding in Evolving Multi-tenant SaaS
    (2011-10-06T02:00:53Z) JU, Lei; SENGUPTA, Bikram; ROYCHOUDHURY, Abhik
    A multi-tenant software as a service (SaaS) system has to meet the needs of several tenant organizations, which connect to the system to utilize its services. To leverage economies of scale through re-use, a SaaS vendor would, in general, like to drive commonality amongst the requirements across tenants. However, many tenants will also come with some custom requirements that may be a pre-requisite for them to adopt the SaaS system. These requirements then need to be addressed by evolving the SaaS system in a controlled manner, while still supporting the requirements of existing tenants. In this paper, we study the challenges associated with engineering multi-tenant SaaS systems and develop a framework to help evolve such systems in a systematic manner. We adopt an intuitive formal model of services that is easily amenable to tenant requirement analysis and provides a robust way to support multiple tenant onboarding. We perform a substantial case study of a multi-tenant blog server to demonstrate the benefits of our proposed approach.