Introduction to the Coq Proof
Coq is an interactive environment allowing to specify and prove properties.
It has been used in a wide range of applications, in particular for defining
semantics and semantic transformations or analyses. The tutorial will focuse
on this area. The first part of the tutorial will give a basic overview of
the specification language and the proof tactics, illustrating the way to
define and manipulate semantics. The second part will be devoted to the
development of a simple formally verified compiler.
Catherine Dubois is a Professor at ENSIIE (École Nationale Supérieure
d'Informatique pour l'Industrie et l'Entreprise - Evry - France) since
2000. She received her PhD from CNAM in 1989 under the supervision of
Véronique Donzeau-Gouge and her Habilitation from the University of Evry
in 2000. Her main research interests concern typed programming languages,
formal semantics and formal proof, more generally the use of formal
methods to develop safe applications. She is a Coq user, in particular
as an environment for programming language semantics. Furthermore, for
several years, she has been involved in the development of the Focalize
environment, in particular regarding the definition of the formal
semantics. She is currently leading a research group CPR (CEDRIC - CNAM
- ENSIIE) which is mainly working on the developement of Focalize and
the certification of tools (e.g. termination tools, watermarking
Session 1, Tuesday 28, 11:00-13:00
Test Suite Quality for Model Transformation Chains
Eduard Bauer, Jochen Kuester and Gregor Engels
Abstract: For testing model transformations or model transformation chains, a software engineer usually designs a test suite consisting of test cases where each test case consists of one or several models. In order to ensure a high quality of such a test suite, coverage achieved by the test cases with regards to the system under test must be systematically measured. Using coverage analysis and the resulting coverage information, missing test cases and redundant test cases can be identified and thereby the quality of the test suite can be improved. As test cases consist of models, a coverage analysis approach must measure how complete models cover the domains of the transformations in the chain and to which degree of completeness transformations are covered when executing the test suite. In this paper, we present a coverage analysis approach for measuring test suite quality for model transformation chains. Our approach combines different coverage criteria and yields detailed coverage information that can be used to identify missing and redundant test cases.
Automated Translation of Java Source Code to Eiffel
Marco Trudel, Manuel Oriol, Carlo Alberto Furia and Martin Nordio
Abstract: Reusability is an important software engineering concept actively advocated for the last forty years. While reusability has been addressed for systems implemented using the same programming language, it does not usually handle interoperability with different programming languages. This paper presents a solution for the reuse of Java code within Eiffel programs based on a source-to-source translation from Java to Eiffel. The paper focuses on the critical aspects of the translation and illustrates them by formal means. The translation is implemented in the freely available tool J2Eif; it provides Eiffel replacements for the components of the Java runtime environment, including Java Native Interface services and reflection mechanisms. Our experiments demonstrate the practical usability of the translation scheme and its implementation, and record the performance slow-down compared to custom-made Eiffel applications: automatic translations of java.util data structures, java.io services, and SWT applications can be re-used as Eiffel programs, with the same functionalities as their original Java implementations.
Session 2, Tuesday 28, 14:30-15:30
KlaperSuite: an Integrated Model-Driven Environment for Non-Functional Requirements Analysis of Component-Based Systems
Andrea Ciancone, Mauro Luigi Drago, Antonio Filieri, Vincenzo Grassi and Raffaela Mirandola
Abstract: Automatic prediction tools play a key role in enabling the application of non-functional requirements analysis to selection and assembly of components for Component-Based Systems, reducing the need for strong mathematical skills to software designers. Exploiting the paradigm of Model Driven Engineering (MDE), it is possible to automate transformations from design models to analytical models, enabling for formal property verification. MDE is the core paradigm of KlaperSuite presented in this paper, which exploits the KLAPER pivot language to fill the gap between Design and Analysis of Component-Based Systems for reliability and performance properties. KlaperSuite is a family of tools empowering designers with the ability to capture and analyze QoS views of their systems by building a one-click bridge towards a number of established verification instruments.
Daniel Langone, Jorge Ressia and Oscar Nierstrasz
Abstract: Subjective behavior is essential for applications that must adapt their behavior to changing circumstances. Many different solutions have been proposed in the past, based, for example, on perspectives, roles, contextual layers, and force trees. Although these approaches are somehow equally expressive, each imposes a particular world view which may not be appropriate for all applications. We propose a unification of these approaches, called Subjectopia, which makes explicit the underlying abstractions needed to support subjective behavior, namely subjects, contextual elements and decision strategies. We demonstrate how Subjectopia subsumes existing approaches, provides a more general foundation for modeling subjective behavior, and offers a means to alter subjective behavior in a running system.
Session 3, Tuesday 28, 16:00-17:30
Lifted Java: A Minimal Calculus for Translation
Matthias Diehn Ingesman and Erik Ernst
Abstract: This paper contributes to the formal foundations of
translation polymorphism by proving type soundness and offering a range of
solutions to an ambiguity problem. In order to support roles and similar notions
involving multiple views on an object, languages like Object Teams and CaesarJ
include mechanisms known as lifting and lowering. These mechanisms connect pairs
of objects of otherwise unrelated types to each other, and enables programmers
to consider such a pair almost as a single object which has both of those types.
In the terminology of Object Teams this is called translation polymorphism. In
both Object Teams and CaesarJ the type system of the Java programming language
has been extended to support this through the use of advanced language features.
However, so far the soundness of translation polymorphism has not been proved.
This paper presents a simple model that extends Featherweight Java with the core
operations of translation polymorphism, proves that its type system is sound,
and shows that the ambiguity problem associated with the so-called smart lifting
mechanism can be eliminated by a very simple semantics for lifting. The
soundness proof of the model has been mechanically verified in the Coq proof
Location Types for Safe Distributed Object-Oriented
Yannick Welsch and Jan Schäfer
Abstract: In distributed object-oriented systems, objects belong to
different locations. For example, in Java RMI, objects can be distributed over
different JVM instances. Accessing a reference in RMI has crucial different
semantics depending on whether the referred object is local or remote.
Nevertheless, such references are not statically distinguished by the type
system. This paper presents location types, which statically distinguish far
from near references. We present a formal type system for a minimal core
language. In addition, we present a type inference system that gives optimal
solutions. We implemented location types as a pluggable type system for the ABS
language, an object-oriented language with a concurrency model based on
concurrent object groups. An important contribution of this paper is the
combination of the type system with the flexible inference system and a novel
integration into an Eclipse-based IDE by presenting the inference results as
overlays. This drastically reduces the annotation overhead while providing full
static type information to the user. The IDE integration is a general approach
of its own and can be applied to many other type system extensions.
Static Dominance Inference
Ana Milanova and Jan Vitek
Abstract: Dominance, the property that all paths to a given object must
go through another object, is at the heart of ownership type disciplines. While
ownership types have received abundant attention, ownership inference remains an
open problem, and crucial questions about the practical impact of ownership
remain unanswered. We argue that a static program analysis that infers dominance
is a crucial first step to ownership types inference. This paper describes an
algorithm for statically computing dominance relations and shows that it can be
used as part of an ownership inference algorithm.
Session 5, Wednesday 29, 14:30-15:30
An Overview of ALIA4J: An Execution Model for Advanced-Dispatching Languages
Christoph Bockisch, Andreas Sewe, Mira Mezini and Mehmet Aksit
Abstract: New programming languages that allow to reduce the complexity of software solutions are frequently developed, often as extensions of existing languages. Many implementations thus resort to transforming the extension's source code to the imperative intermediate representation of the parent language. But approaches like compiler frameworks only allow re-use of code transformations for syntactically-related languages; they do not allow for re-use across language families. In this paper, we present the ALIA4J approach to enable such for language families with advanced dispatching mechanisms like pointcut-advice or predicate dispatching. ALIA4J introduces a meta-model of dispatching as a rich intermediate representation. By implementing language constructs of four languages as refinements of this meta-model, we show that a significant amount of these constructs can be re-used across language families. Another building block of ALIA4J is a framework for execution environments that automatically derives an execution model of the program's dispatching from our intermediate representation. This model enables different execution strategies for dispatching; we have validated this by implementing four execution environments based on strategies ranging from interpretation to different kinds of code generation
Systems evolution and software reuse in OOP and AOP
Abstract: New programming techniques make claims that software engineers often want to hear. Such is the case with aspect-oriented programming (AOP). This paper describes a quasi-controlled experiment which compares the evolution of two functionally equivalent programs, developed in two different paradigms. The aim of the study is to explore the claims that software developed with aspect-oriented languages is easier to maintain and reuse than this developed with object-oriented languages. We have found no evidence to support these claims.
Session 6, Wednesday 29, 16:00-17:30
A Generic Solution for Syntax-driven Model Co-evolution
Zvezdan Protic, Mark Van Den Brand and Tom Verhoeff
Abstract: In this paper we discuss, and provide a generic solution to, the problem referred to as model co-evolution: How to evolve models in case their metamodels evolve? We solve this problem by extending a traditional three-step approach. In the first step, differences between an initial and an evolved metamodel are determined. Unlike in traditional approaches, we treat metamodels as models conforming to a special metamodel, thus the same difference representation and calculation mechanisms for metamodels as for models are used in our approach. In the second step, metamodel differences are classified into four groups based on their possible influence on co-evolving models, and the possibilities of handling them automatically. We adopt two of these groups (non-breaking and breaking and resolvable differences) from the existing co-evolution approaches, and we introduce two new groups (breaking and semi-resolvable and breaking and human-resolvable differences). In the third step, based on the determined metamodel differences, a generic co-evolution transformation is invoked. This transformation takes the metamodel differences, and a model as arguments, and returns an adapted model. We validated our approach by incorporating our method into a prototype tool for generic model co-evolution, and by testing this tool on a large set of metamodels and models.
From UML Profiles to EMF Profiles and Beyond
Philip Langer, Konrad Wieland, Manuel Wimmer and Jordi Cabot
Abstract: Domain-Specific Modeling Languages (DSMLs) are getting more and more attention as a key element of Model Driven Engineering. As any other software artefact, DSMLs should continuously evolve to adapt to the changing needs of the domain they represent. Unfortunately, right now evolution of DSMLs is a costly process that requires changing its metamodel and re-creating the complete modeling environment. In this paper we advocate for the use of EMF Profiles, an adaptation of the UML profile concept to DSMLs. Profiles have been a key enabler for the success of UML by providing a lightweight language-inherent extension mechanism which is expressive enough to cover an important subset of adaptation scenarios. We believe a similar concept for DSMLs would provide an easier extension mechanism which has been so far neglected by current metamodeling tools. Apart from direct metamodel profiles, we also propose reusable profile definition mechanisms whereby profiles are defined independently of any DSML and, later on, coupled with all DSMLs that can benefit from these profiles. Our approach has been implemented in a prototype integrated in the EMF environment.
Alexandre Bergel, Oscar Nierstrasz, Lukas Renggli and Jorge Ressia
Abstract: Domain-specific languages and models are increasingly used within general-purpose host languages. While traditional profiling tools perform well on host language code itself, they often fail to provide meaningful results if the developers start to build and use abstractions on top of the host language. In this paper we motivate the need for dedicated profiling tools with three different case studies. Furthermore, we present an infrastructure that enables developers to quickly prototype new profilers for their domain-specific languages and models.
Metamodel Dependencies for Executable Models
Carlos Rodríguez, Mario Sanchez and Jorge Villalobos
Abstract: Cumbia is our platform to develop applications based on multiple, coordinated executable models which can be described using different languages. The coordination of models is achieved by describing how their elements should interact, and mapping those descriptions into low level coordination primitives. Moreover, the description of the coordination is described externally: it does not have an impact either on the metamodels or on the models, and this results in lower coupling and increased flexibility. This approach, which is appropriate when the metamodels are highly independent, has limitations when it comes to describing dependencies that are inherent to the concerns. In those cases, it makes sense to incorporate those dependencies into the metamodels descriptions. The goal of this paper is thus to discuss two alternative ways to establish those dependencies, and illustrate their usage, benefits, and drawbacks in a concrete example.
Session 7, Thursday 30, 11:00-13:00
Seuss: Cleaning up Class Responsibilities with Language-based Dependency Injection
Niko Schwarz, Mircea Lungu and Oscar Nierstrasz
Abstract: Unit testing is often made more difficult by the heavy use of classes as namespaces and the proliferation of class methods to encapsulate configuration code. We have analyzed the use of 120 class methods from 96 projects by categorizing them according to their responsibilities. We find that most class methods support a hodgepodge of mixed responsibilities, held together only by their common need to be globally visible. Tight coupling between instances and their classes breaks encapsulation, and, together with the global visibility of class methods, complicates testing. By making dependency injection a feature of the programming language, we can get rid of class methods altogether. We employ the following semantic changes: (1) Replace every occurrence of a global with an access to an instance variable; (2) Let that instance variable be automatically injected into the object when it is instantiated. We present Seuss, a prototype that implements this change of semantics in Smalltalk. We show how Seuss eliminates the need to use class methods for non-reflective purposes, reduces the need for many design patterns, such as Abstract Factory, and simplifies configuration code, particularly for unit tests.
Extensive Validation of OCL Models by Integrating SAT Solving into USE
Mirco Kuhlmann, Lars Hamann and Martin Gogolla
Abstract: The Object Constraint Language (OCL) substantially enriches modeling languages like UML, MOF or EMF with respect to formulating meaningful model properties. In model-centric approaches, an accurately defined model is a requisite for further use. During development of a model, continuous validation of properties and feedback to developers is required, since many design flaws can then be directly discovered and corrected. For this purpose, lightweight validation approaches which allow developers to perform automatic model analysis are particularly helpful. We provide a new method for efficiently searching for model instances. The existence or non-existence of model instances with certain properties allows significant conclusions about model properties. Our approach is based on the translation of UML and OCL concepts into relational logic and its realization with SAT solvers. We explain various use cases of our proposal, for example, completion of partly defined model instances so that particular properties hold in the completed model instances. Our proposal is realized by integrating a model validator as a plugin into the UML and OCL tool USE.
Session 8, Thursday 30, 14:30-15:30
Efficient Retrieval and Ranking of Undesired Package Cycles in Large Software Systems
Jean-Rémy Falleri, Simon Denier, Jannik Laval, Philippe Vismara and Stéphane Ducasse
Abstract: Many design guidelines state that a software system architecture should avoid cycles between its packages. Yet such cycles appear again and again in many programs. We believe that the existing approaches for cycle detection are too coarse to assist the developers to remove cycles from their programs. In this paper, we describe an efficient algorithm that performs a fine-grained analysis of the cycles among the packages of an application. In addition, we define a metric to rank cycles by their level of undesirability, prioritizing the cycles that seems the more undesired by the developers. Our approach is validated on two large and mature software systems in Java and Smalltalk.
Session 9, Thursday 30, 16:00-17:30
Computational REST Meets Erlang
Alessandro Sivieri, Gianpaolo Cugola and Carlo Ghezzi
Abstract: Today's applications are developed in a world where the execution context changes continuously. They have to adapt to these changes at run-time if they want to offer their services without interruption. This is particularly critical for distributed Web applications, whose components run on different machines, often managed by different organizations. Designing these programs in an easy and effective way requires choosing the right architectural style and the right run-time platform. The former has to guarantee isolation among components, supporting scalability, reliability, and dynamic changes. The latter has to offer mechanisms to update the applications' code at run-time. This work builds upon previous research about architectures and run-time platforms. Its contribution is to put together a very promising architectural style -- Computational REST -- with a language (and run-time environment) designed with dynamic, distributed applications in mind -- Erlang. We show how they fit together by developing a new framework, which eases development of highly distributed Web applications capable of operating in dynamic environments. We also provide an initial experimental assessment of the proposed approach.
A Heuristic Approach for Computing Effects
Phillip Heidegger and Peter Thiemann
A Case of Visitor versus Interpreter Pattern
Mark Hills, Paul Klint, Tijs Van Der Storm and Jurgen Vinju
Abstract: We compare the Visitor pattern with the Interpreter pattern, investigating a single case in point for the Java language. We have produced and compared two versions of an interpreter for a programming language. The first version makes use of the Visitor pattern. The second version was obtained by using an automated refactoring to transform uses of the Visitor pattern to uses of the Interpreter pattern. We compare these two nearly equivalent versions on their maintenance characteristics and execution efficiency. Using a tailored experimental research method we can highlight differences and the causes thereof. The contributions of this paper are that it isolates the choice between Visitor and Interpreter in a realistic software project and makes the difference experimentally observable.