3,458 papers · page 149 of 173
Decompositional Verification of Component-based Systems-A Hybrid Approach
Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests
Understanding Aspects via Implicit Invocation
Refactoring Use Case Models on Episodes
Automated Support for Framework Selection and Customization
On the automatic evolution of an OS kernel using temporal logic and AOP
Automating software evolution requires both identifying precisely the affected program points and selecting the appropriate modification at each point. This task is particularly complicated when considering a large program, even when the modifications appear to be systematic. We …
Graph Rewriting And Transformation (GReAT): A Solution For The Model Integrated Computing (MIC) Bottleneck
Graph grammars and transformations (GGT) have been a field of theoretical study for over two decades. However, it has produced only a handful of practical implementations. GGT needs a widely used practical application to exploit its potential. On the other hand model integrated c…
A Type System for Statically Detecting Spreadsheet Errors
We describe a methodology for detecting user errors in spreadsheets, using the notion of units as our basic elements of checking. We define the concept of a header and discuss two types of relationships between headers, namely is-a and has-a relationships. With these, we develop …
XRay Views: Understanding the Internals of Classes
Understanding the internal workings of classes is a key prerequisite to maintaining an object-oriented software system. Unfortunately, classical editing and browsing tools offer mainly linear and textual views of classes and their implementation. These views fail to expose the se…
Parallel Breadth-First Search LTL Model-Checking
We propose a practical parallel on-the-fly algorithm for enumerative LTL (linear temporal logic) model checking. The algorithm is designed for a cluster of workstations communicating via MPI (message passing interface). The detection of cycles (faulty runs) effectively employs th…
Semi-Automatic Fault Localization and Behavior Verification for Physical System Simulation Models
Mathematical modeling and simulation of complex physical systems are emerging as key technologies in engineering. Modern approaches to physical system simulation allow users to specify simulation models with the help of equation-based languages. Due to the high-level declarative …
Model Checking Software Requirement Specifications using Domain Reduction Abstraction
As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its…
An Infrastructure to Support Meta-Differencing and Refactoring of Source Code
The proposed research aims to construct an underlying infrastructure to support (semi) automated construction of refactorings and system wide transformation via a fine grained syntax level differencing approach. We term this differencing approach meta-differencing as it has addit…
A Programmable Client-Server Model: Robust Extensibility via DSLs
The client-server model has been successfully used to support a wide variety of families of services in the context of distributed systems. However, its server-centric nature makes it insensitive to fast changing client characteristics like terminal capabilities, network features…
Testing Database Transaction Concurrency
Database application programs are often designed to be executed concurrently by many users. By grouping related database queries into transactions, DBMS (database management system) can guarantee that each transaction satisfies the well-known ACID properties: atomicity, consisten…
Automated Software Testing Using a Metaheuristic Technique Based on Tabu Search
The use of techniques for automating the generation of software test cases is very important as it can reduce the time and cost of this process. The latest methods for automatic generation of tests use metaheuristic search techniques, i.e. genetic algorithms and simulated anneali…
Automation for Exception Freedom Proofs
Run-time errors are typically seen as unacceptable within safety and security critical software. The SPARK approach to the development of high integrity software addresses the problem of run-time errors through the use of formal verification. Proofs are constructed to show that e…
Specification and Synthesis of Hybrid Automata for Physics-Based Animation
Physics-based animation programs can often be modeled in terms of hybrid automata. A hybrid automaton includes both discrete and continuous dynamical variables. The discrete variables define the automaton's modes of behavior. The continuous variables are governed by mode-dependen…
Applying AutoBayes to the Analysis of Planetary Nebulae Images
We take a typical scientific data analysis task, the analysis of planetary nebulae images taken by the Hubble Space Telescope, and describe how program synthesis can be used to generate the necessary analysis programs from high-level models. We describe the AutoBayes synthesis sy…