Keynote Lectures

Model-centric Assumption Promise Specification
Manfred Broy, Technische Universität München, Germany, Germany

The Role of Models in the Automated Integration of Service-oriented Software Systems
Paola Inverardi, Università dell'Aquila, Italy, Italy

Making Model-Driven Verification Practical and Scalable - Experiences and Lessons Learned
Lionel Briand, Université du Luxembourg, Luxembourg, Luxembourg

Abstract
The talk addresses foundations, basic concepts, and paradigms for the specification of and reasoning about interactive real-time systems, their interfaces, and architectures as well as their properties in terms of contracts. Contracts are structured into assumptions about the behavior of the operational context of systems and promises about the system behavior (in the literature also called assumption/guarantee or assumption/commitment specification patterns). A logical analysis of assumption/promise specifications is carried out based on a mathematical system model:
+ From assumption/promise contracts interface specifications are derived and analysed.
+ Safety and liveness properties for assumption/promise contracts are analysed.
+ Healthiness conditions are worked out for assumption/promise contracts.
+ From interaction specifications describing the interaction between two + systems assumption/promise contracts for the involved systems are derived.
+ Contracts for components in architectures are studied in terms of
+ assumptions and promises and healthiness conditions are worked out that guarantee that assumptions for the composite systems guarantee the validity of the assumptions for components.
Based on the theoretical analysis more practical issues are dealt with for a systematic use of assumption/promise patterns in system specification and architecture design.

Abstract
In the near future we will be surrounded by a virtually infinite number of software applications that provide services in the digital space. This situation radically changes the way software will be produced and used: (i) software is increasingly produced according to specific goals and by integrating existing software; (ii) the focus of software production will be shifted towards reuse of third-parties software, typically black-box, that is often provided without a machine readable documentation. The evidence underlying this scenario is that the price to pay for this software availability is a lack of knowledge on the software itself, notably on its interaction behaviour. A producer will operate with software artefacts that are not completely known in terms of their functional and non-functional characteristics. The general problem is therefore directed to the ability of interacting with the artefacts to the extent the goal is reached. This is not a trivial problem given the virtually infinite interaction protocols that can be defined at application level. Different software artefacts with heterogeneous interaction protocols may need to interoperate in order to reach the goal. In this talk focuses on models, techniques and tools for integration code synthesis, which are able to deal with partial knowledge and automatically produce correct-by-construction service-oriented systems with respect to functional goals. The research approach we propose builds around two phases: elicit and integrate. The first concerns observation theories and techniques to elicit functional behavioural models of the interaction protocol of black-box services. The second deals with compositional theories and techniques to automatically synthesize appropriate integration means to compose the services together in order to realize a service choreography that satisfies the goal.

Abstract
Verification challenges in the software industry, including testing, come in many different forms, due to significant differences across domains and contexts. But one common challenge is scalability, the capacity to test and verify increasingly large, complex systems. Another concern relates to practicality. Can the inputs required by a given technique be realistically provided by engineers? Though, to a large extent, Model-Driven Engineering (MDE) is a significant component of many verification techniques, a complete solution is necessarily multidisciplinary and involves, for example, machine learning or evolutionary computing components.

This talk reports on 10 years of research tackling verification and testing problems, in most cases in actual industrial contexts, relying on MDE but also metaheuristic search, optimisation, and machine learning. The focus of the talk will be on how to scale to large system input spaces and achieve practicality by decreasing the level of detail and precision required in models and abstractions. I will draw from past and recent experiences to provide practical guidelines and outline possible avenues of research.

Concrete examples of problems we have addressed, and that I will cover in my talk, include schedulability analysis, stress/load testing, CPU usage analysis, robustness testing, testing closed-loop dynamic controllers, and SQL Injection testing. Most of these projects have been performed in industrial contexts and solutions were validated on industrial software.