Home      Log In      Contacts      FAQs      INSTICC Portal

Keynote Lectures

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

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

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


Model-centric Assumption Promise Specification

Manfred Broy
Fakultät Für Informatik , Technische Universität München

Brief Bio
Manfred Broy is a full professor at the Department of Informatics at the TUM in Munich. In 1994, he received the Leibniz Prize from the German National Science Foundation (DFG) for his academic achievements. In 2003, he obtained a Doctor Honoris Causa from the University of Passau. Prof. Broy is a member of the Deutsche Akademie der Naturforscher “Leopoldina” and a member of acatech, which is the Deutsche Akademie der Technikwissenschaften.

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.



The Role of Models in the Automated Integration of Service-oriented Software Systems

Paola Inverardi
Università dell'Aquila

Brief Bio
Paola is professor at the Department of Information Engineering Computer Science and Mathematics at University of L'Aquila. Her research interests are in the field of the application of formal techniques to the development of software systems. These include software specification and verification of concurrent and distributed systems, deduction systems, and Software Architectures. Current research interests mainly concentrate in the field of software architectures specifically addressing the verification and analysis of software architecture properties, both behavioral and quantitative. On this topics she collaborates with several national and international companies. Recently she is working on the design and development of mobile resource aware applications. Paola is member of ACM Europe Council, of Academia Europaea, and received a Honorary Doctorate at Malardalen University.

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.



Making Model-Driven Verification Practical and Scalable - Experiences and Lessons Learned

Lionel Briand
Université du Luxembourg

Brief Bio
Lionel Briand is professor  and FNR PEARL chair in software engineering and Vice-Director at the Centre for ICT Security, Reliability, and Trust (SnT), University of Luxembourg. He is a highly regarded expert in the areas of software verification and model-driven engineering, performing research with strong and sustained industrial collaborations. He is an IEEE Fellow, and is the recipient of the IEEE CS Harlan Mills award, and the IEEE Reliability Society’s engineer-of-the-year award.

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.