Lectures¶

Language-Driven Engineering¶

Lecturers: Bernhard Steffen (Technical University of Dortmund), Tiziana Margaria (University of Limerick and LERO)

Language-Driven Engineering (LDE) is a new paradigm that aims at involving stakeholders, including the application experts, to participate in the system development and evolution process using dedicated Domains-Specific Languages (DSLs) tailored to match the stakeholders’ mindsets. Technically, the interplay between the involved DSLs is realized in a service-oriented fashion. This eases product line and system evolution by allowing to introduce and exchange entire DSLs within corresponding Mindset-Supporting Integrated Development Environments (mIDEs). Participants of STRESS will be provided with a tangible LDE experience along the development and evolution of an email distribution system. The practical part will focus on the problem of profile-based email selection, where participants are invited to play with and adapt a variety of decision languages, e.g., to switch from a binary mindset to a “fuzzy” mindset. The practicality of the participants’ solutions will be evaluated in a corresponding simulation environment.

Meta-Modelling from a Practical Perspective¶

Lecturers: Bernhard Steffen (Technical University of Dortmund), Tiziana Margaria (University of Limerick and LERO)

The practicality of LDE requires powerful means for the construction of Mindset-Supporting Integrated Development Environments (mIDEs). CINCO, the Meta Tooling Suite developed in Dortmund is designed exactly for this purpose. STRESS participants will be provided with hands-on experience with CINCO-based meta-model-driven engineering from three perspectives: (1) the perspective of a user of a CINCO product (an mIDE) by enhancing a basic “Web Story” application with additional features, (2) the perspective of an mIDE developer by enhancing the Web Story DSL, and (3) the perspective of a CINCO core developer by enhancing CINCO itself using CINCO.

In particular the third perspective is exciting because of its bootstrapping effect. As CINCO is available open source, participants are invited to continue their experimentation, and to cooperate as CINCO product users, CINCO product developers, or even as CINCO core developers.

Model-based Development for High-Assurance Embedded Systems¶

Lecturers: John Hatcliff (Kansas State University) and Robby (Kansas State University)

Low cost embedded cyber-physical systems and ubiquitous net-working has opened up a new world of connected devices in our homes and workplaces, and in safety critical contexts such as automobiles, medical care, and drone-based air vehicles. There are many different approaches to developing and assuring these systems, but not all take a rigorous approach and even fewer offer integrated frameworks for assurance.

In this lecture, we will introduce students to an integrated modeling and verification environment for high-assurance embedded systems. The modeling framework is based on the SAE standard Architecture and Analysis Definition Language (AADL). Students will enhance models from a building control systems and a simple medical device, generate component interfaces, develop component implementations and use an associated simulation environment to debug and assess the appropriateness of the design and implementation. Next, will use a code-level verification environment based on symbolic execution to illustrate how systems can be simulated and component implementations can be verified to conform to component contracts derived from system requirements.

An Overview of Malware Detection and Evasion Techniques¶

Lecturer: Axel Legay, INRIA

This tutorial presents and motivates various malware detection tools and illustrates their usage on a clear example. We demonstrate how statically-extracted syntactic signatures can be used for quickly detecting simple variants of malware. Since such signatures can easily be obfuscated, we also present dynamically-extracted behavioral signatures which are obtained by running the malware in an isolated environment known as a sandbox. However, some malware can use sandbox detection to detect that they run in such an environment and so avoid exhibiting their malicious behavior. To counteract sandbox detection, we present concolic execution that can explore several paths of a binary. We conclude by showing how opaque predicates and JIT can be used to hinder concolic execution.