International School HATS-FMCO


Beyond Inheritance

Dave Clarke
Katholieke Universiteit Leuven

Modern software engineering approaches, such as software product line engineering, have high demands on programming languages in terms of both modularity and reuse. To address these demands, a variety of different composition mechanisms for object-oriented programming languages have evolved over recent years, beyond traditional single and multiple inheritance. This tutorial will describe and compare a number of these mechanisms, including mixins (as seen in Scala), traits (as in the Smalltalk variant Squeak), and aspect-oriented programming, along with some more recent research approaches including subobject-oriented programming and delta-oriented programming.

Integrating Deployment Decisions in Application-level Models

Einar Broch Johnsen
University of Oslo

Traditionally in software engineering, the model of a system abstracts from the details of how the system should be deployed. This abstraction is based on an assumption that the provisioning of resources is handled sufficiently well at a lower layer. However, increasing emphasis on quality-of-service for high-level applications, support for e.g. network-awareness and cloud computing, force the developer to take the resource provisioning of the developed system into account. In this lecture, we discuss how some low-level deployment decisions may be lifted to the abstraction level of modeling languages for object-oriented design. By supporting application-specific deployment decisions at early stages in software engineering, developers may design applications with deployment-dependent behavior in order to optimize quality of service in given deployment scenarios, for example to minimize loss of QoS when unexpected peaks in client traffic or fluctuations in the underlying resource provisioning occur.

Formal Aspects of Free Software Components

Roberto Di Cosmo
University Paris Diderot

In recent years, the number of available free software components has grown at an astonishing rate, to the point that configuring a running system based on free software is mostly done by selecting and configuring together compatible modules, that can be packages, plugins, or other software components. In this short course we will give the theoretical underpinnings of the composition of software packages, establish its complexity, and present various efficient algorithms that can be used to analyse large repositories of components, identify their compatibility issues, and predict their future behaviour.

Abstract Behavioral Specification of Distributed Object-Oriented Systems

Reiner Hähnle
Technical University of Darmstadt

ABS (for abstract behavioral specification) is a novel language for modelling feature-rich, distributed, object-oriented systems at an abstract, yet precise level. ABS has a clear and simple concurrency model that permits sychronous as well as actor-style asynchronous communication. ABS abstracts away from specific datatype or I/O implementations, but is a fully executable language and has code generators for Java, Scala, and Maude. ABS goes beyond conventional programming languages in two important aspects: first, it embeds architectural concepts such as components or feature hierarchies and allows to connect features with their implementation in terms of product families. In contrast to standard OO languages, code reuse in ABS is feature-based instead of inheritance-based. Second, ABS has a formal semantics and has been designed with formal analysability in mind. This makes it possible, for example, perform automatic resource estimation of concurrent ABS models.

In the lecture we present the most important language features of ABS and illustrate them with examples. We will also demonstrate parts of the ABS tool chain, including code generation, code animation, deadlock analysis, functional verification, and resource analysis. Students will be able to download the ABS tools and try them out hands-on, if they wish.

Automatic Inference of Bounds on Resource Consumption

Elvira Albert
Universidad Complutense de Madrid

One of the main features of programs is the amount of resources which are needed in order to run them. Different resources can be taken into consideration, such as the number of execution steps, amount of memory allocated, number of calls to certain methods, etc. Unfortunately, manually determining the resource consumption of programs is difficult and error-prone. In this course we will study a state of the art framework for automatically obtaining both upper and lower bounds on the resource consumption of programs. The bounds obtained are functions on the size of the input arguments to the program and are obtained statically, i.e., without running the program. Due to the approximations introduced, the framework can fail to obtain (non-trivial) bounds even if they exist. On the other hand, modulo implementation bugs, the bounds thus obtained are valid for any execution of the program. The framework has been implemented in the COSTA system and can provide useful bounds for realistic object-oriented and actor-based concurrent programs.

Verification of Open Concurrent Object Systems

Arnd Poetzsch-Heffter
Technical University of Kaiserslautern

In the course, we present techniques for the specification and verification of open concurrent object systems. A concurrent object system consists of a dynamically changing set of objects that work concurrently and interact with the environment of the system. An object system is called open if the environment of the system is not known. To proof that an open system satisfies a desired property P, we have to show that P holds for all possible environments. We describe a simple calculus for concurrent object systems together with an operational and a trace-based semantics. Then, we present a specification technique that supports looseness and restriction. Looseness allows specification refinement. Restriction allows expressing assumptions of the environment. Finally, we introduce a verification technique to prove that an open system OS satisfies a specified property P. The technique supports hierarchical reasoning, i.e., the properties of OS's components can be used in the proof of P.

Managing Diversity in Knowledge

Fausto Giunchiglia
University of Trento

Diversity is pervasive and this is particularly so in Knowledge. This is because of many reasons: time, geographical and space distribution, school of thought, opinions, ..., and so on. This problem becomes particularly acute when one tries to build large scale knowledge bases which can be used, in practice, for solving semantics and knowledge aware tasks.

This talk will be composed in 3 parts. In the first we will discuss the pervasiveness of diversity in knowledge. In the second we will propose a general mechanism for dealing with this problem, as applied to the specific task of aligning two semantically heterogeneous lightweight ontologies. In the third we will describe EntityPedia, a moderately large scale, but very high quality, knowledge base with around 10 million instances, 100 million ground axioms, and more 100,000 universal axioms.

The Role of Models@run.time in Supporting On-the-fly Interoperability

Valérie Issarny
INRIA Paris - Rocquencourt
CONNECT project coordinator

Models at runtime can be defined as abstract representations of a system, including its structure and behaviour, which exist in tandem with the given system during the actual execution time of that system. Furthermore, these models should be causally connected to the system being modelled, offering a reflective capability. Signicant advances have been made in recent years in applying this concept, most notably in adaptive systems. Our hypothesis is that a similar approach can also be used to support the dynamic generation of software artefacts at execution time. An important area where this is relevant is the generation of software connectors to tackle the crucial problem of interoperability in distributed systems.

We refer to this approach as emergent middleware, representing a fundamentally new approach to resolving interoperability problems in the complex distributed systems of today. In this context, the runtime model is used to capture meta-information about the underlying networked systems which need to interoperate including their interfaces and additional knowledge about their associated behaviour. This is supplemented by ontological information to enable semantic interoperability in given application domains.

In this lecture, we first provide an overview of the state of the art in the areas of models@runtime and of middleware solutions to interoperability. We then focus on the novel use of models at runtime to enable Emergent middleware, examining in detail the nature of such runtime models coupled with consideration of the supportive algorithms that extract this knowledge and use it to synthesize the appropriate emergent middleware.

Load-time Security Verification for Real Smart-cards

Fabio Massacci
University of Trento

How to make sure that the applets downloaded on your smart cards don't talk to each other, unless you really want. You have seen many papers of this kind (when they use model checking, theorem proving and the like), but here we are talking on something that runs on a real card.