[Jot-newsletter] [JOT] JOT Subscriber Newsletter Volume 14, no. 3 (August 2015)

JOT EIC editor at jot.fm
Fri Aug 14 18:55:00 CEST 2015


For Volume 14, no. 3 (August 2015)

I. Content


VOLT 2012/2013 Special Section
By Eugene Syriani, Manuel Wimmer

  This JOT special section contains three extended and peer reviewed papers
  from the first and second editions of the International Workshop on
  Verification Of modeL Transformation (VOLT). The first edition of VOLT was
  held on April 21st, 2012 in Montreal, Canada as satellite event of the 5th
  International Conference on Software Testing, Verification and Validation
  (ICST 2012). The second edition was held on June 17th, 2013 in Budapest,
  Hungary as a satellite event of Federated Conferences on Software
  Technologies: Applications and Foundations (STAF 2013).



Formal Verification Techniques for Model Transformations: A Tridimensional
By Moussa Amrani, Benoît Combemale, Levi Lúcio, Gehan M. K. Selim, Jürgen
Dingel, Yves Le Traon, Hans Vangheluwe, James R. Cordy

  In Model Driven Engineering (MDE), models are first-class citizens, and
  model transformation is MDE's "heart and soul". Since model
  transformations are executed for a family of (conforming) models, their
  validity becomes a crucial issue. This paper proposes to explore the
  question of the formal verification of model transformation properties
  through a tridimensional approach: the transformation involved, the
  properties of interest addressed, and the formal verification techniques
  used to establish the properties. This work is intended for a double
  audience. For newcomers, it provides a tutorial introduction to the field
  of formal verification of model transformations. For readers more familiar
  with formal methods and model transformations, it proposes a literature
  review (although not systematic) of the contributions of the field.
  Overall, this work allows to better understand the evolution, trends and
  current practice in the domain of model transformation verification. This
  work opens an interesting research line for building an engineering of
  model transformation verification guided by the notion of model
  transformation intent.


Validating Transformations for Semantic Anchoring
By David  Lindecker, Gabor Simko, Tihamer Levendovszky, Istvan Madari,
Janos Sztipanovits
  Making Domain-Specific Modeling Languages a part of a tool chain, a part
  of a proven development process, or the subject of verification cannot be
  achieved without the precise specification of the language and the models
  expressed in it. Defining formal semantics for modeling languages is a
  widely accepted solution to this problem. We have developed methods,
  techniques and processes to provide a systematic mapping -- which we call
  semantic anchoring -- that support the scaling of these formal definitions
  to large modeling languages. Although a semantic mapping is a definition
  and behaves as a set of axioms for formal verification, we argue that a
  semantic mapping can conflict with the informal intentions of the language
  designer, resulting in a counterintuitive DSML, and should therefore be
  validated.  This paper proposes a solution that involves formalizing the
  language designer's intentions about the semantic mapping and validating
  the consistency between the two by applying model finding techniques.


A Methodology for Verifying Refinements of Partial Models.
By Rick Salay, Marsha Chechik, Michalis Famelis, Jan Gorzny

  Models are typically used for expressing information that is known at a
  particular stage in the software development process.  Yet, it is also
  important to express what information a modeler is still uncertain about
  and to ensure that model refinements actually reduce this uncertainty.
  Furthermore, when a refining transformation is applied to a model
  containing uncertainty, it is natural to consider the effect that the
  transformation has on the level of uncertainty, e.g., whether it always
  reduces it. In our previous work, we have presented a general approach for
  precisely expressing uncertainty within models.  In this paper, we  use
  these foundations and define formal conditions for uncertainty reducing
  refinement between individual models and within model transformations. We
  describe tooling for automating the verification of these conditions
  within transformations and describe its application to example


II. 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