Formal Research Demonstrations (FD)

These systems will also be demonstrated in the exhibits area.

Thursday, May 17, 2001

S25
Software Architecture

Session chair:
Rudolf K. Keller,
University of Montréal, Canada

Model Processing Tools in UML
Johannes Koskinen,
Jari Peltonen,
Petri Selonen,
Tarja Systä, and
Kai Koskimies,
Tampere University of Technology, Finland

Unified Modeling Language (UML) provides several diagram types viewing a system from different perspectives. In this research, we exploit logical relationships between different UML models. We propose operations to compare, merge, slice and synthesize UML diagrams based on these relationships. In the formal demonstration we show how statechart diagrams can be synthesized semi-automatically from a set of sequence diagrams using an interactive algorithm called MAS. We also demonstrate how a class diagram, annotated with pseudocode presentations of key operations, can be synthesized from sequence diagrams, and how class diagrams and sequence diagrams can be sliced against each other.

Hyper/J™: Multi-Dimensional Separation of Concerns for Java™
Harold Ossher and
Peri Tarr,
IBM T.J. Watson Research Center, USA

Hyper/J™ supports a new approach to constructing, integrating and evolving software, called Multi-Dimensional Separation of Concerns. Developers can decompose and organize code and other artifacts according to multiple, arbitrary criteria (concerns) simultaneously-even after the software has been implemented-and synthesize or integrate the pieces into larger-scale components and systems. Hyper/J™ facilitates several common development and evolution activities noninvasively, including: adaptation and customization, mix-and-match of features, reconciliation and integration of multiple domain models, reuse, product line management, extraction or replacement of existing parts of software, and on-demand remodularization. Hyper/J™ works with standard Java™ software, not requiring special compilers or environments.

Architecture-Oriented Programming Using FRED
Markku Hakala,
Juha Hautamäki,
Kai Koskimies,
Tampere University of Technology, Finland; and
Jukka Paakki,
Jukka Viljamaa,
Antti Viljamaa,
University of Helsinki, Finland

Software development is largely based on standards, conventions, underlying systems and architectures, most notably object-oriented frameworks. However, implementing application-specific code conforming to architectural rules and conventions can be tedious. We will demonstrate our research prototype FRED (Framework Editor), a generic architecture-oriented development environment for Java. FRED takes the definition of an architecture as a set of programming patterns and provides interactive task-based programming assistance. Incorporating adaptive code generation and documentation, the tool provides a convenient way to adopt as well as effectively reuse a framework or architectural standard such as Java Beans.

Thursday, May 17, 2001; 8:30 a.m.–10:00 a.m.

S33
Reuse and Integration

Session chair:
George T. Heineman,
Worcester Polytechnic Institute, USA

CodeWeb: Data Mining Library Reuse Patterns
Amir Michail,
University of New South Wales, Australia

Developers learn to use a software library not just from its documentation but also from toy examples and existing real-life application code (e.g., by using grep). The CodeWeb tool takes this simple idea further by a deeper analysis of a large collection of applications to see what characteristic usage of the library is like. We demonstrate the tool by showing how the KDE core libraries are used in real-life KDE applications. Moreover, we look at a recently developed feature that helps software developers port an application from an old version of a library to a new one.

Holmes: An Intelligent System to Support Software Product Line Development
Giancarlo Succi,
Jason Yip, and
Witold Pedrycz,
University of Alberta, Canada

A software product line is a set of software products that are developed in a synergistic fashion. Developing a software product line requires many interdependent activities. Tools to support product-line development should provide specific assistance for each activity. A limitation of existing tools is that they either focus mainly on architecture and component development aspects or vary in their support of queries, change consistency management, multiple users, and semantic support. Holmes is a product line support tool that supports the full product line life cycle as well as introduces novel features to address aspects missing from other tools.

Babel: Representing Business Rules in XML for Application Integration
Huaxin Zhang and
Eleni Stroulia,
University of Alberta, Canada

Information-system integration has become one of the major activities in modern IT industry. To address this problem, a generic method is needed for integrating heterogeneous data from the various individual systems according to relevant business rules, and disseminating the resulting information to other systems within the aggregate system. Babel is a prototype, designed to provide this mediation service. Babel's design-time environment uses XML to represent the services of the systems participating in the aggregation, and the integrating business rules. At run time, Babel acts as a blackboard, receiving records of actual services used, processing them according to the relevant business rules, and forwarding the results to their recipient systems.

Thursday, May 17, 2001; 2:00 p.m.–3:30 p.m.

S38
Verification and Maintenance

Session chair:
Eleni Stroulia,
University of Alberta, Canada

jMOCHA: A Model Checking Tool that Exploits Design Structure
R. Alur,
University of Pennsylvania, USA;
L. de Alfaro,
University of California, Berkeley, USA;
R. Grosu,
SUNY, Stony Brook, USA;
T. A. Henzinger,
University of California, Berkeley, USA;
M. Kang,
University of Pennsylvania, USA;
C.M. Kirsch,
University of California, Berkeley, USA;
R. Majumdar,
University of California, Berkeley, USA;
F. Mang,
University of California, Berkeley, USA; and
B. Y. Wang,
University of Pennsylvania, USA

Mocha is a model checker based on the theme of exploiting modularity. Instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of Reactive Modules. The hierarchy is exploited by the tool in three ways. First, verification tasks such as refinement checking can be decomposed into subgoals using assume-guarantee rules. Second, instead of traditional temporal logics such as CTL, it uses Alternating Temporal Logic (ATL), a game-based temporal logic that is designed to specify collaborative as well as adversarial interactions between different components. Third, the search algorithms incorporate optimizations based on the hierarchical reduction of sequences of internal transitions. This report describes a new release of Mocha that is implemented in Java and supports many new features including an extensive GUI and a scripting language for rapid prototyping of symbolic verification algorithms.

Maintenance Support Tools for Java Programs: CCFinder and JAAT
Toshihiro Kamiya,
Fumiaki Ohata,
Kazuhiro Kondou,
Shinji Kusumoto,
Katsuro Inoue,
Osaka University, Japan

This paper describes maintenance support tools, CCFinder and JAAT, for Java programs. CCFinder identifies code clones. A code clone is one of a code portions in source files that is identical or similar to each another and makes the source files very hard to consistently modify. JAAT executes alias analysis for Java program. When an expression refers to a memory location which is referred to by another expression, there is an alias relation between those expressions. The result of alias analysis is useful to locate the faults related to such aliases.

Using OCL-Queries for Debugging C++
Chanika Hobatr and
Brian A. Malloy,
Clemson University, USA

This demonstration will present a design and preliminary implementation of the OCL query-based debugger, OQBD, which is a tool to debug C++ programs using queries formulated in the object constraint language, OCL. We will illustrate how queries can be formulated to verify constraints such as class invariants and pre and post-conditions for member functions. These queries can be reused after code generation to verify the design contract, as part of the testing process, and to facilitate fault detection.

Thursday, May 17, 2001; 4:00 p.m.–5:30 p.m.