3,458 papers · page 130 of 173
Our objective is to provide automated support for assisting designers in fixing inconsistencies in UML models. We have previously developed techniques for efficiently detecting inconsistencies in such models and identifying where changes need to occur in order to fix problems det…
This contribution outlines a cognitive-oriented approach to construct test systems that can "partially " imitate several cognitive paradigms of skilled human testers. For example, learning, reasoning, optimization, etc. Hence, a reasonable portion of the workload done by a human …
Designing and maintaining a huge class model is a very complex task. When an object oriented software or model grows, duplicated elements start to appear, decreasing the readability and the maintainability. In this paper, we present an approach, implemented in a tool and validate…
We describe BPELCheck, a tool for statically analyzing interactions of composite Web services implemented in BPEL. Our algorithm is compositional, and checks each process interacting with an abstraction of its peers, without constructing the product state space. Interactions betw…
The reasons why software is changed are manyfold; new features are added, bugs have to be fixed, or the consistency of coding rules has to be re-established. Since there are many types of of source code changes we want to explore whether they appear frequently together in time an…
The Rosetta system specification language will require a variety of analysis capabilities to assist system designers. The language's generality prohibits the development of a single analysis tool. It is proposed, instead, to leverage the existing analysis tools and create an anal…
Rich Internet Application (RIA) has been proposed in order to solve the problems of current web applications. The user experience of current web applications is not comparable to desktop applications. RIA provides sophisticated interfaces for representing complex processes and da…
In this demonstration session, we present a toolkit we have designed around a model-driven language fLEJ. This relies on formal methods to ease the development of applications in an efficient and reusable way. Formal methods have been advocated as a means of increasing the reliab…
Rhizome is an end-to-end feature modeling and code generation platform that includes a feature modeling language (FeatureML), a template language (MarkerML) and a template-based code generator. A software designer creates feature models using FeatureML by selecting and defining d…
Multi-core programming presents developers with a dramatic paradigm shift. Whereas sequential programming largely allowed the decoupling of source from underlying architecture, it is now impossible to develop new patterns and abstractions in isolation from issues of modern hardwa…
Tool developers are facing high expectations regarding the capabilities and usability of software engineering tools. Users expect tools which are tailored to their specific needs and integrated in their environment. This increases the complexity of tools and makes their customiza…
Interrupt-driven real time control software is difficult to design and validate. It does not line up well with traditional state-based, timed-transition specification formalisms, due to the complexity of timers and the pending interrupt queue. The present work takes a new approac…
Provides notice of upcoming conference events of interest to practitioners and researchers.
Existing software model checkers based on predicate abstraction and refinement typically perform poorly at verifying the absence of buffer overflows, with analyses depending on the sizes of the arrays checked. We observe that many of these analyses can be made efficient by provid…
We describe PTYASM, an enhanced version of the YASM software model checker which uses proof templates. These templates associate correctness arguments with common programming idioms, thus enabling efficient verification. We have used PTYASM to verify the safety of array accesses …
Physical proximity supports various forms of ad-hoc collaboration among developers such as opportunistic task adaptation and helping co-developers when they are stuck. Connecting the input/output flows of stand-alone programming environments of distributed developers offers the p…
Developers undertaking a pragmatic reuse task must collect and reason about information that is spread throughout the source code of a system before they can understand the scope of their task. Once they have this understanding, they can undertake the manual process of actually r…
Reportedly, supercomputer designer Seymour Cray once said that he would sooner use two strong oxen to plow afield than a thousand chickens. Although this is undoubtedly wise when it comes to plowing afield, it is not so clear for other types of tasks. Model checking problems are …
Most existing fault-localization techniques focus on identifying and reporting single statements that may contain a fault. Even in cases where a fault involves a single statement, it is generally hard to understand the fault by looking at that statement in isolation. Faults typic…
Achieving high structural coverage such as branch coverage in object-oriented programs is an important and yet challenging goal due to two main challenges. First, some branches involve complex program logics and generating tests to cover them requires deep knowledge of the progra…