Courses and Material ↑
You will find the list of invited speakers below, along with a short abstract, summarising the contents of the course:
Temporal Coordination of Actors: Specification, Inference and Enforcement of Mechanisms (ACT)
Speaker: Gul Agha (U. of Illinois at Urbana-Champain)
Pre-requisites: Basic familiarity with concurrent and object-oriented programming.
Abstract: In sequential systems, programmers are responsible for totally ordering events occurring in a system. This results in overly constraining when events may occur. In concurrent systems, actions at autonomous actors are nondeterministically interleaved. Without additional constraints on the order of events at participating actors, an interleaving may lead to incorrect operation or deadlocks. The presentation will describe several mechanisms for temporal coordination of actors: synchronization constraints, session types, specification diagrams and protocol description languages. I will survey methods for specification, inference and enforcement of these mechanisms, their applicability and limitations. The talk will conclude with a perspective on open problems and research directions.
| Lecture 1 | Lecture 2 |
|---|---|
|
Introduction to Session Types (IST)
Speaker: Ornela Dardha (U. of Glasgow)
Pre-requisites: No pre-requisites required.
Abstract: In complex distributed systems, communicating participants agree on a protocol to follow, by specifying the type and direction of data exchanged. Session types are an elegant type formalism used to model structured communication-based programming. They guarantee privacy, communication safety and session fidelity. A binary session type describes communication among two participants, as opposed to multiparty session type, which describes communication among two or more participants.
In these lectures we will focus mainly on binary session types and the pi-calculus, a core communication and concurrency calculus, which is the original and most successful framework for session types. We will give the statics and dynamics of the language and illustrate these with several examples and exercises. We will present some advanced topics on session types as well as their logical foundations. Finally, we will present how session types are integrated in mainstream programming languages, with main focus on Java, and a summary of session-based software tools for specifying and verifying communicating protocols in distributed scenarios.
| Lecture 1 & 2 | Lecture 3 | Lecture 4 |
|---|---|---|
Using behavioral abstractions for testing and validating classes. (BAT)
Speaker: Diego Garbervetsky (U. of Buenos Aires)
Pre-requisites: No pre-requisites required.
Abstract: Many software engineering artefacts, such as source code or specifications, define a set of operations and impose restrictions to the ordering on which they have to be invoked. Enabledness Preserving Abstractions (EPAs) are concise representations of the behaviour space for such artefacts. In this tutorial, we exemplify how EPAs might be used for validation of software engineering artefacts by showing the use of EPAs to support some programming tasks on a simple Java/C# classes. We will also show how EPAs can be used for better test case generation for classes with interesting protocols.
| Lecture 1 | Lecture 2 | Lecture 3 |
|---|---|---|
|
Choreographic Programming of Adaptive Applications (CPA)
Speaker: Ivan Lanese (U. of Bologna)
Pre-requisites: some previous knowledge about choreographies or multiparty session is encouraged, but not necessary
Abstract: Choreographic Programming exploits choreographies as a programming language. We will introduce choreographic programming, and showcase its use for programming distributed applications which are:
- dynamically updatable by including new code fragments at runtime
- free by construction from errors such as communication deadlocks
races
We will be using the following software: AIOCJ and Jolie
| Lectures 1, 2, 3 |
|---|
Foundations of runtime verification (RTV)
Speaker: Karoliina Lehtinen (U. of Liverpool)
Pre-requisites: No pre-requisites required.
Abstract: This course is an introduction to the theoretical foundations of runtime verification.
The idea of runtime verification is to observe the executions of a system in order to derive information on its behaviour. By analysing executions rather than the system itself, it avoids the state-explosion problem associated with exhaustive verification techniques such as model-checking.
The cost of lower complexity is limited expressivity: while model-checking will always provide a definite answer to the question “does the system satisfy the specification”, runtime verification provides no such firm guarantees. However, depending on the specification, runtime verification can provide a range of weaker guarantees. Understanding the trade-offs between the complexity of specifications and the power of runtime verification is at the heart of this course.
The first part of this course will be an introduction to runtime monitors and how to formalise their behaviour. The course will then cover different notions of correctness for runtime monitors, and discuss the trade-off implied by these different definitions. We will discuss the automatic synthesis of monitors directly from specifications. The final part of the course will cover how moving from linear-time specifications to branching-time specifications affects monitorability.
The aim of the course is to familiarise the participants with recent efforts to give rigorous foundations to runtime verification. At the end of the course the participants will be able identify and state precisely how useful runtime verification might be for a given specification or class of specifications, and generate monitors with the appropriate correctness guarantees
| Lecture 1 | Lecture 2 & 3 |
|---|---|
Session Types meet Type Providers: Compile-time Generation of Protocol APIs (STG)
Speaker: Rumyana Neykova (Brunel University London)
Pre-requisites: No prerequisites. We will provide VMs with the environment setup. If attendees want to install the tools in their own environment, then they will need: .Net 4.5 (at least) with F#, Visual Studio and Java8.
Abstract: Session types is a typing discipline for concurrent and distributed processes that allows errors such as communication mismatches and deadlocks to be detected statically. Refinement types are types elaborated by logical constraints that allow richer and finer-grained specification of application properties, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. Type providers, developed in F#, are compile-time components for on-demand code generation. Their architecture relies on an open-compiler, where provider-authors implement a small interface that allows them to inject new names/types into the programming context as the program is written.
In these lecture series, I will present a library that integrates aspects from the above fields to realise practical applications of multiparty refinement session types (MPST) for any .Net language. Our library supports the specification and validation of distributed message passing protocols enriched with message-type refinements (value constraints) and value dependent control flow. The protocols are written in Scribble (a toolchain for MPST).
The combination of these aspects—session types for structured interactions, constraint solving from refinement types, and protocol-specific code generation enables the specification and implementation of enriched protocols in native F# (and any .Net-compiled language) without requiring language extensions or external pre-processing of user programs. The API generation happens on demand (while the developer is writing the program) and at compile-time (the generated API calls are directly integrated into the compiled binaries of the program).
We will discuss the formal foundations of the library, validation of Scribble protocols, the technical challenges of compile-time generation, and finally, we will practice type-driven development of several small- and large-scale protocols. We will conclude with a brief overview of other tools and techniques for API generation of Scribble protocols.
| Lectures 1, 2, 3 |
|---|
The impact of asynchronous communication on the theory of contracts and session types (CST)
Speaker: Gianluigi Zavattaro (U. of Bologna)
Pre-requisites: No pre-requisites required.
Abstract: We discuss some of the proposals in the literature about contract theories and session types dealing with asynchronous communication. Assuming that communication is mediated by buffers, notions of compatibility, contract refinement and session subtyping can be defined that are less restrictive w.r.t. their synchronous counterparts. Unfortunately, most of such notions in the literature turn out to be undecidable. We discuss the source of this negative result, and present some proposals to overcome this limitation, with the aim of obtaining algorithmic versions of such notions.
| Lectures 1, 2, 3 |
|---|
Bootcamp ↑
The school will host a one day bootcamp, where companies will showcase their approaches to API development with hands-on sessions.
STIX 2.0 model and Patterns: Applying API economy to cybersecurity (STIX)
Speakers: Leonardo Frittelli, Facundo Maldonado(McAfee)
Pre-requisites: Laptop with internet connectivity; basic introduction to STIX would help, but it is not necessary.
Abstract: Effectively exchanging and acting upon threat intelligence in a diverse, heterogeneous landscape such as cyber security has proven an elusive goal. With the continuous evolution of both the security tools and the attack techniques, combined with a market where new cloud based players surface on a rapid scale, having a common language to both define and apply the knowledge obtained from actual attacks is key to the success of the whole industry.
This bootcamp will present a STIX 2.0.
STIX 2.0 is a proposal the standardisation of data modelling for security products as well as application of the model through the definition of suitable patterns. After overviewing the history STIX 2.0, its applications in industry, and its model, we will focus on the libraries and the Patterning methods. Students will use real world examples of threat intelligence reports to practice first hand both the model and patterning API with bespoke exercises.
Industry use-case: uncompromisingly available agents (ACTYX)
Speakers: Jan Pustelnik (Actyx)
Pre-requisites: No pre-requisites.
Abstract: In the manufacturing industry downtime is very expensive, therefore most small and midsize factories are still managed using paper-based processes. The problem space is perfectly suited for a microservices approach: well-defined and locally encapsulated responsibilities, collaboration and loose coupling, rapid evolution of individual pieces. But how can we operate microservices such that they can deliver the resilience of paper? How can we leverage the locality of process data and benefit from high bandwidth and low latency communication in the Internet of Things?
This workshop explores the radical approach of deploying autonomous actor-like agents in a peer-to-peer network on the factory shop-floor, using event sourcing as the only means of communication and observation. We discuss the approach of a coordination-free totally ordered eventually consistent event log and its consequences on the programming model inspired by the time warp algorithm (Jefferson 1987). In particular we dive into the question of a formal description of legal event sequences to simplify the programmer’s life: it is not yet clear what is attainable in this regard
| Two-hour Workshop |
|---|
Business Process Regulatory Compliance (DCR)
Speakers: Hugo Andrés Lopez (DCR Solutions)
Pre-requisites: Internet connection and a browser. Link and instructions to DCR graphs below.
Abstract: Regulatory compliance describes the level of alignment between business processes and legislations, and it represents a complex process where regulations have to be instantiated in terms of a business process, and later check for correctness: the business process should provide evidence that actors fulfilling necessary conditions will eventually be granted with the rights they are entitled to. This is important for governmental case work, that are tightly governed by law. Legislations are far from being digitalised, and to provide a better support for ensuring regulatory compliance of case management processes we need formalisations of the law that can be mechanised and used for determining the legal and the required activities to be carried out at a particular point in a given process. This calls for a logic that can distinguish between what is possible, i.e. legal and may happen, and what is required, i.e. legal and must happen. Which legal constraints are relevant at a particular time for a particular process often varies a lot depending on the case. This calls for a logic in which rules can be dynamically included and excluded, and where adaptation of regulations can be made in an effortless way.
Moreover, case management processes often contain activities and rules that are not described in detail by the law, but still relevant for the effective support of the process. Consequently, we need tools and methods for the formalisation of regulations and processes by different kinds of users and from two different kind of sources: Legal texts formalised by legal experts, and descriptions of practice formalised by process experts.
In this tutorial we will present how the declarative Dynamic Condition Response (DCR) graphs process notation and associated tools have been developed for the formalisation and mechanisation of adaptive case management processes and meets exactly these requirements. Essentially, DCR graphs is a. A (declarative) process language that defines the causal relations between activities, with emphasis in what may happen (conditions) vs. what must be done (responses). It is dynamic, as these relations might change depending on the execution of certain events. b. It is a graphical language that users with no background in formal methods can use, and c. It is a business process execution engine. We will present how DCR graphs have been used in the formalisation of legally-compliant business processes in Danish Municipalities. In particular, we will demonstrate how the recently developed highlighter tool can be used to faciliate model creation and provide traceability between process models and textual descriptions of law and regulations. Rather than describing the process and later inspecting its alignment with law, our approach forms part of the family of Compliance-by-Design (CbD) process development methodologies. The methodology involves the generation of formal models from the legal text, and the refinement of such models into the activities that conform a business process. The advantage of such approach is that there is no further need for testing whether one execution of the process will violate a legal requirement
| Two-hour Workshop |
|---|
Tools: Validation: Some initial readings on the formal foundations of DCR graphs |
Security Connected Solutions using Open APIs (OpenDXL)
Speakers: Andres More, Damian Quiroga (McAfee)
Pre-requisites: No pre-requisites.
Abstract: OpenDXL is an open API to enable devices to share intelligence and orchestrate security operations in real-time. This security connected platform from McAfee provides a unified framework for hundreds of products, services, and partners already adopted in the field. Any organization can improve its security posture and minimize operational costs through the platform’s capabilities. The platform leverages a real-time data exchange framework to build collective threat intelligence to make endpoint, network, and cloud countermeasures protect and detect as one.
The tutorial includes a review of the problem-space and use cases to be supported, then matching against the proposed platform capabilities including open APIs. After reviewing concrete examples of real-world integrations by partners and customers, we will discuss how to develop by leveraging current APIs and creating new ones. To complete the tutorial student will be challenged with hands-on exercises reusing both Python and NodeRed samples from OpenDXL to add security-related behaviors to the platform.
Programme ↑
| Time/Day | Monday | Tuesday | Wednesday | Thursday | Friday |
|---|---|---|---|---|---|
| 9:00 | IST | IST | DCR | IST | CST |
| 10:00 | IST | RTV | DCR | STG | CST |
| 11:00 | Coffee break | Coffee break | Coffee break | Coffee break | Coffee break |
| 11:30 | RTV | RTV | OpenDXL | CST | STG |
| 12:30 | BAT | BAT | OpenDXL | CPA | CPA |
| 13:30 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 14:30 | ACT | ACT | STIX | STG | |
| 16:00 | Coffee break | Coffee break | Coffee break | Coffee break | |
| 16:30 | BAT | CPA | Actyx |