[Jot-newsletter] JOT Subscriber Newsletter Volume 10, July 2011

Oscar Nierstrasz oscar at iam.unibe.ch
Mon Jul 4 16:40:39 CEST 2011


For Volume 10, (July 2011)

I. Letter from the JOT Editor

Dear Readers,

The current volume contains two special sections, one on Formal Techniques for Java-like Programs, and another with selected, extended papers from International Conference on Model Transformations (ICMT) 2010. There are also two regular articles, one on Ontological Behavior Modeling, and another on Using Design Pattern Clues to Improve the Precision of Design Pattern Detection Tools.

JOT has gone through a number of changes in the past year. The most significant is the change in format from multiple issues per year to a single volume with articles appearing as soon as they are camera-ready.  This new format has the advantage that authors do not have to wait for their articles to appear just to satisfy an artificial pipeline of virtual issues.  On the other hand, it also means that the flow of articles published will be much more irregular than in the past. As a consequence, this newsletter will appear less regularly than in the past, whenever there is a significant batch of papers to announce.

Readers who wish to be informed of each new article are encouraged to follow the JOT Twitter feed (http://twitter.com/jotfm) or the RSS feed (http://blog.jot.fm/feed/).

JOT also welcomes Antonio Vallecillo as Special Section Editor, and Richard Paige as JOT Blog Editor. We encourage you to contact us at jot-editor at jot.fm concerning regular technical submissions, proposals for special sections, and all forms of articles related object technology.

For details see: http://www.jot.fm/authors.html

Oscar Nierstrasz
Editor-in-Chief, Journal of Object Technology
editor at jot.fm -- http://www.jot.fm

II. Content


JOT needs you!
By Oscar Nierstrasz

JOT has moved to a new publication model in which there is no pipeline of accepted papers to be published.  Instead, accepted papers will appear as soon as possible after the final camera-ready copy is provided, whereas in the past, accepted papers sometimes had to wait up to a year to appear on-line.  The old pipeline of accepted papers and regularly scheduled issues of JOT expired with the November 2010 issue. Although the new system promises faster turnaround, the downside is that issues will no longer appear regularly as clockwork.
The current volume of JOT is now open. Articles will appear as they become available.
Although the new JOT promises faster publication for accepted papers, the evaluation process is tougher, while being more transparent (see the information for authors page).


Special Section on Formal Techniques for Java-like Programs.
By Frank Piessens, Bart Jacobs, Gary T. Leavens

Formal Techniques for Java-like Programs (FTfJP), with 12 completed successful  events, and a 13th event on the horizon, is one of the most prestigious and long-standing ECOOP workshop series.
The 12th edition of the workshop was organized on June 22, 2010 in Maribor, Slovenia. Twelve papers were submitted in response to the Call For Papers, and nine of them were accepted for presentation at the workshop. With an average attendance of about 30 participants — and a peak attendance of over 50 during the invited talk (thanks to Shriram Krishnamurthi) — FTfJP was one of the most popular workshops at ECOOP 2010.



Strong exception-safety for checked and unchecked exceptions.
By Giovanni Lagorio, Marco Servetto

“Exception-safety strong guarantee:
The operation has either completed successfully or thrown an exception,
leaving the program state exactly as it was before the operation started.”
— David Abrahams.
The above definition of strong exception-safety comes from the world of C++, but
it can be applied to any language.
Because the exception-safety strong guarantee plays a central role in
easing the development of robust software, we have designed a type-system able to capture its
essence. The idea is that the state of the reachable objects at the beginning of a
catch block is the same as the beginning of the corresponding try block.
We present a lightweight type system for Java-like languages that, by introducing
a simple modifier to types, enforces that programs satisfy the strong guarantee in the presence
of checked and unchecked exceptions.


Modular Verification of Linked Lists with Views via Separation Logic.
By Jonas Braband Jensen, Lars Birkedal, Peter Sestoft

We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for .NET. A view is a generalization of the well-known concept of an iterator. Linked lists with views form an interesting case study for verification since they allow mutation through multiple, possibly overlapping, views of the same underlying list. For modularity, we build on a fragment of higher-order separation logic and use abstract predicates to give a specification with respect to which clients can be proved correct. We introduce a novel mathematical model of lists with views, and formulate succinct modular abstract specifications of the operations on the data structure. To show that the concrete implementation realizes the specification, we use fractional permissions in a novel way to capture the sharing of data between views and their underlying list.
We conclude by suggesting directions for future research that arose from conducting this case study.


Ontological Behavior Modeling.
By Conrad Bock, James Odell

This article gives an example of improving the effectiveness of behavior modeling languages using ontological techniques. The techniques are applied to behaviors in the Unified Modeling Language (UML), using the logical meanings for classification introduced in UML 2. The article suggests unifying UML's three kinds of behavior languages around the abstract syntax and semantics of composite structure, UML's model for capturing interconnection of parts of classes. This significantly simplifies the UML metamodel, provides a formal semantics to clarify ambiguities in the current informal semantics, and increases the expressiveness of UML behaviors.


Using Design Pattern Clues to Improve the Precision of Design Pattern Detection Tools.
By Francesca Arcelli Fontana, Marco Zanoni, Stefano Maggioni

Design pattern detection, or rather the detection of structures that match design patterns, is useful for reverse engineering, program comprehension and for design recovery as well as for re-documenting object-oriented systems. Finding design patterns inside the code gives hints to software engineers about the methodologies adopted and the problems found during its design phases, and helps the engineers to evolve and maintain the system. In this paper, we present the results provided by four different design pattern detection tools on the analysis of JHotDraw 6.0b1, a well-known Java GUI framework. We show that the tools generally provide different results, even while evaluating the same system. From this observation, we introduce an approach based on micro structures detection that aims to discard the false positives from the detected results, hence improving the precision of the analyzed tools results. For this purpose we exploit a set of micro structures called design pattern clues, which give useful hints for the detection of design patterns.



ICMT 2010 Special Section.
By Laurence Tratt, Martin Gogolla

This JOT special section presents 4 carefully selected and extended papers from the third edition of the International Conference on Model Transformations (ICMT), held in Málaga in June / July 2010.



A Rewriting Logic Semantics for ATL.
By Javier Troya, Antonio Vallecillo

As the complexity of model transformation (MT) grows, the need to rely on
formal semantics of MT languages becomes a critical issue. Formal semantics
provide precise specifications of the expected behavior of transformations,
allowing users to understand them and to use them properly, and MT tool
builders to develop correct MT engines, compilers, etc. In addition, formal
semantics allow modelers to reason about the MTs and to prove their
correctness, something specially important in case of large and complex MTs
(with, e.g., hundreds or thousands of rules) for which manual debugging is no
longer possible. In this paper we give a formal semantics of the ATL 3.0 model
transformation language using rewriting logic and Maude, which allows
addressing these issues. Such formalization provides additional benefits, such
as enabling the simulation of the specifications or giving access to the Maude
toolkit to reason about them.


From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case.
By Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki

Existing bidirectional model transformation (BX) languages are mainly
state-based: model alignment is hidden inside update propagating
procedures, and model deltas are implicit. Weaving alignment with
update propagation complicates the latter and makes it less predictable
and less manageable.  We propose to separate concerns and consider
two distinct operations: delta discovery (alignment) and delta
propagation. This architecture has several technological advantages, but
requires a corresponding theoretical support.
The goal of the paper is to develop a delta-based algebraic
framework for the case of <i>asymmetric</i> BX, where one model is
a view of the other. In this framework, model spaces are categories
(nodes are models and arrows are composable deltas), and delta
propagation procedures are mappings between them.  We call the
corresponding algebras <i>delta lenses</i>, prove their several basic
properties,  and explore their relationships with ordinary lenses --
well-known algebraic models for state-based asymmetric BX.


Safe Composition of Transformations.
By Florian Heidenreich, Jan Kopcsek, Uwe A\ssmann

Model transformations are at the heart of Model-Driven Software Development (MDSD) and, once composed in 
transformation chains to MDSD processes, allow for the development of 
complex systems and their automated derivation. While there already exist 
various approaches to specify and execute such MDSD processes, only 
few of them draw focus on ensuring the validity of the transformation chains, 
and thus, safe composition of transformations. In this paper, we present the 
TraCo composition system, which overcomes these limitations and evaluate and 
discuss the approach based on two case studies.


From UML 2 Sequence Diagrams to State Machines by Graph Transformation.
By Roy Gr\/{o}nmo, Birger M\/{o}ller-Pedersen

Algebraic graph transformation has been promoted by several authors as a means to specify model transformations. This paper explores how we can specify graph transformation-based rules for a classical problem of transforming from sequence diagrams to state machines. The specification of the transformation rules is based on the concrete syntax of sequence diagrams and state machines. We introduce tailored transformation support for sequence diagrams and a novel graphical operator to match and transform combined fragments.


III. About JOT

The Journal of Object Technology (JOT) is a peer-reviewed, open-access journal dedicated to the timely publication of previously unpublished research articles, surveys, tutorials, and technical notes on all aspects of object technology.

JOT is available online at http://www.jot.fm and is free to both readers and authors, with no registration required.

The JOT newsletter is sent with the publication of selected JOT issues and is available by subscription to the JOT reader and author community. The subscription form may be found on the JOT Web site. Subscribing requires no personal information or fee, only your email address. We use such addresses for the sole purpose of distributing the JOT newsletter and do not communicate them to third parties.
You are receiving this newsletter because you have subscribed to
	jot-newsletter at jot.fm
To unsubscribe, please use the mailman interface:

More information about the jot-newsletter mailing list