The IPA Fall Days are an annual multi-day event, dedicated to a specific theme of current interest to the research community of IPA. This year’s Fall Days are dedicated to Communication, Safety and Privacy in the Internet of Things, fitting in the Cyber-Security, Cyber Physical Systems and Real World Algorithmics and Models focus areas of the research school for the period 2013-2018.
Registration closed on 24 October. As always, IPA PhD students can attend for free. For others, details on pricing will be made available upon request.
To make maximal use of the available capacity, we process applications on the following basis: Registrations are treated “first come, first served”. In principle, all PhD students (IPA and non-IPA) will share a room. Others may also be asked to share if we run out of rooms. Until the registration deadline, we will accept participants until we run out of space at the hotel!
A number of speakers have made their slides available; these can be downloaded
from this location. If you cannot find the slides online, you may try contacting the speaker directly.
Monday 7 November is reserved for the IPA PhD workshop; the remainder of the days are devoted to topics in communication, safety and privacy in the Internet of Things. Our keynote speaker for the PhD Workshop is Jurriaan Rot, winner of the IPA Dissertation Award of 2015. The workshop aims to promote the interaction and cohesion with PhD students from other universities on both a social and technical level, provide a hospitable setting in which presentation skills can be demonstrated and improved through constructive feedback by peers, and be fun.
MONDAY 7 NOVEMBER: PHD WORKSHOP
Send an email to firstname.lastname@example.org if you wish to present at the IPA PhD Workshop; we still have at least one slot available!
|14:00-14:30||Nico Naus, UU
Building a generic end-user feedback system for iTasks
iTasks is a rule based workflow management framework, implemented in a functional programming language. It allows programmers to define chunks of work, called tasks, and to combine them into bigger tasks, using combinators. This structure forms the complete program specification. From this specification, the entire application is generated.
In many domains where iTasks is being used to write applications, it is beneficial to provide the end-user with feedback while he/she executes the program. This feedback can consist of hints on what to do next, explaining why something has to be done, etc. To save the programmers from writing ad-hoc user feedback systems, we are constructing a generic end-user feedback framework for iTasks.
|14:30-15:00||Joshua Moerman, RU
Learning to verify
Learning techniques are becoming a more and more popular topic in many sciences. Even in software it has its applications. I will talk about using model learning as a promising tool in software verification. Model learning can be applied in situations where developers want to prove properties about their software, but have no models of the software amenable to model checking techniques. I will talk about the advances we booked in our research as well as some open problems we are tackling now.
|15:15-15:45||Thomas Neele, TU/e
Scalable model checking of timed systems
The mCRL2 tool set is a versatile tool for modelling and analysing concurrent systems. However, practical support for systems with time is limited. In this talk, I will explain why verification of timed systems is relevant for real-world applications and how we aim to improve the scalability of mCRL2 for timed systems.
Additionally, I will give a short overview of my past work in other areas of model checking.
|15:45-16:15||Henning Basold, RU
The classical notion of algorithm assumes that inputs are finite and that computations eventually terminate with an output. For example, sorting algorithms take (finite) lists as input and output a sorted list after a finite number of computation steps. Due to their finite structure, lists are considered as inductive data. Moreover, sorting algorithms usually operate by sorting parts of the list and combine these parts, so they are defined inductively in the input.On the other hand, many systems are assumed to run indefinitely, while reacting to their environment. Examples here are control systems and deterministic finite automata that recognise regular languages. Such systems can be described and reasoned about using coinduction.Finally, in many cases we need to combine both types of computation, which leads to inductive-coinductive structures and reasoning principles. For instance, so-called liveness properties of reactive systems, that is, properties that something needs to happen eventually, can be described by mixing induction and coinduction.
In the talk, we will study inductive-coinductive properties in the case of reactive systems, and discuss the arising issues and approaches to overcome these issues.
|16:35-17:30||Jurriaan Rot, RU
Enhanced coinductive proof techniques
Coinduction, the dual of induction, is a fundamental principle for defining infinite objects and proving properties about them. It is becoming increasingly clear that coinduction provides a foundation for many structures arising in computer science, and in recent years it has been the subject of intense research activity.
In this talk, I will give an introduction to coinductive reasoning, as well as enhanced proof principles, and discuss applications to languages and automata.
TUESDAY 8 NOVEMBER
|09:00-10:00||Gerd Kortüm, TUD
Why the Internet of Things Needs Design, Not Just Technology
The Internet of Things is not just about connecting sensors and actuators, ultimately it is an attempt to activate and automate the world – with outcomes which will deeply affect and effect people. In this talk I will talk about the Internet of Things as a design challenge and discuss how an integration of design and technology might help fulfil the promises of the Internet of Things.
|10:30-11:15||Mariëlle Stoelinga, UT
Reliability, safety and maintenance in the internet of things: risk happens, and formal methods can help
How do we ensure that applications like robots, drones, and IoT applications are safe and reliable? That is the topic of risk analysis, and fault tree analysis is a very popular technique here, deployed by many institutions like NASA, ESA, Honeywell, Toyota, etc.In this presentation, I will elaborate how the deployment of stochastic model checking can improve the capabilities of fault tree analysis, making them more powerful, flexible and efficient: I will present a compositional framework, where we can analyze a richer variety of questions via stochastic model; I will show how we obtain more compact models via bisimulation and graph rewriting techniques, and get more flexibility in the modeling power.Finally, I will show how one can incorporate smart maintenance strategies, a crucial aspect in reliability engineering, reporting on our experience with the application and validation of these techniques in industrial practice.
|11:15-12:00||Kasim Sinan Yildirim, TUD
Safety and Security Challenges in RF-based Wireless Power Transfer Networks
RF-based wireless power transfer networks (WPTNs) are deployed to transfer power to embedded devices over the air via radio frequency waves. Up until now, a considerable amount of effort has been devoted by researchers to design WPTNs that maximize several objectives such as harvested power, energy outage and charging delay. However, inherent security and safety issues in these networks are generally overlooked. In this talk, I will focus on the safety and security problems in WPTNs and provide an overview of new research opportunities in this emerging domain.
|14:00-15:00||Rolf Ernst, Technische Universität Braunschweig (DE)
Automotive Ethernet - Good models and formalisms for safety and higher efficiency
The lecture will start with a motivation for using Ethernet in cars as a next generation communication backbone. Then, a number of limitations will be highlighted that threaten functional safety and time predictability. In the third part, selected properties are investigated showing that a formal analysis of Ethernet standard extensions is very helpful in identifying protocols with efficient worst-case guarantees.
|15:30-16:15||Jingyue Cao, TU/e
Independent yet Tight WCRT Analysis for Individual Priority Classes in Ethernet AVB
In the high-tech and automotive industry, bandwidth considerations and widely accepted standardization are two important reasons why Ethernet is currently being considered as an alternative solution for real-time communication (compared to the traditional fieldbusses). Although Ethernet was originally not intended for this purpose, the development of the Ethernet AVB standard enables its use for transporting high-volume data (e.g. from cameras and entertainment applications) with latency guarantees.Worst-case response time (WCRT) analysis is essential to ensure these latency guarantees. The traditional busy-period analysis relies on knowledge of all data streams, including interference. However, for complex industrial systems, the assumption that characteristics of all interfering data streams are known, is not realistic. As the amount of components connected to an Ethernet network grows, it becomes less likely that one can know or enforce the traffic patterns generated by all these components.In this presentation, we will introduce an independent real-time analysis based on so-called eligible intervals, which does not rely on any assumptions on interfering priority classes other than those enforced in the Ethernet AVB standard. We will show our analysis is tight when no additional information on interference is known. Furthermore, we will compare the results of our approach to the two most recent busy-period analyses, point out sources of pessimism in these earlier works, and discuss the advantages of using eligible-intervals over busy-period analysis when studying idling servers.
|16:15-17:00||Mahmoud Talebi, TU/e
Design and Verification of a Cluster-Tree Formation Algorithm in IEEE 802.15.4e TSCH mode
In wireless lighting applications, the predominant scheme used for dissemination of data is flooding. However, in dense networks, flooding leads to a high number of retransmissions and contention. With the advent of the IEEE 802.15.4e standard and the time-slotted channel hopping (TSCH) mode, there have been efforts to replace the flooding schemes with more structured protocols in which the dissemination of data occurs over a cluster-tree topology in the network. However, the problem of designing and verifying the correctness of a protocol for the formation of a cluster-tree is non-trivial.In this presentation, I present a methodology for the design and verification of a cluster-tree formation protocol using the mCRL2 toolset. We first see how the mCRL2 toolset can be used to specify the peculiar phenomena which occur in wireless communication. We then see the requirements that should be satisfied by the given protocol, as well as the limitations that we face in implementation. Through verifying the protocol, we analyze the impact of the decisions that were made in the design of the protocol, and in the end we arrive at an improved cluster-tree formation protocol.
WEDNESDAY 9 NOVEMBER
|09:00-10:00||Nirvana Meratnia, UT
Who knows what you did this summer?
With the increase of personal wireless devices such as smart phones, smart watches, fit bits, etc, city-wide sensing has been gaining both popularity and feasibility. While several systems and applications leverage data of users’ mobile devices to provide services, privacy of users is under pressure. The privacy concerns include what personal and private information/context can be inferred from this data and what is the value and impact of this information/context.
|10:30-11:15||Tanir Özçelebi, TU/e
Smart Space Fundamentals, Architectures and Performance
The Internet of Things is becoming a reality. Although most of the billions of IoT devices will belong to machine-to-machine IoT networks, IoT networks that aim to serve human users in a way that is perceived as “smart” in some sense are becoming increasingly popular. The smart space concept offers exciting possibilities for the realization of ubiquitous systems as was envisioned by Mark Weiser in 1991 in the article titled “The Computer for the 21st Century”. This presentation gives an overview of smart space fundamentals, architectural choices in smart space design and resulting performance issues.
|11:15-12:00||Mike Holenderski, TU/e
Data-driven failure prediction for manufacturing and maintenance
The vast amount of sensor data collected in modern manufacturing processes facilitates the development of data driven approaches for predicting machine and product failures. They rely on machine learning techniques for identifying common patterns in the sensor data preceding the failures, and offer an alternative to the traditional methods which rely on the expertise of engineers familiar with the mechanical and physical models of the analysed system. This talk presents the challenges of applying such methods for predicting failures in two industrial use cases.
|14:00-14:45||Jacques Verriet, TNO/ESI
Model-based analysis of large-scale distributed systems: dealing with scalability and hiding complexity
This presentation addresses model-based analysis of distributed control systems using large-scale indoor lighting systems as a carrying example. We will show how we can use the nature of distributed systems to deal with the limited scalability of analysis techniques, such as simulation, model checking, and model-based testing. We also present a domain-specific modelling approach that allows the complexity of analysis tools to be hidden from non-specialist users.
|14:45-15:30||Michel Reniers, TU/e
Compositional Specification of Functionality and Timing of Manufacturing Systems
This talk introduces a formal modeling approach for compositional specification of both functionality and timing of manufacturing systems. Functionality aspects can be considered orthogonally to timing aspects. The functional aspects are specified using two abstraction levels; high-level activities and lower level actions. Design of a functionally correct controller is possible by looking only at the activity level, abstracting from the different execution orders of actions and their timing. As a result, controller design can be performed on a much smaller state space compared to an explicit model where timing and actions are present. The performance of the controller can be analyzed and optimized by taking into account the timing characteristics. Since formal semantics are given in terms of a (max; +) state space, various existing performance analysis techniques can be used. We illustrate the approach, including performance analysis, on an example manufacturing system.
THURSDAY 10 NOVEMBER
|09:00-10:00||Günter Karjoth, Lucerne University (Ch)
Taking Privacy by Design to the World of IoT
The Mauritius Declaration on the Internet of Things states that data obtained from connected devices is “high in quantity, quality and sensitivity” and, as such, “should be regarded and treated as personal data.” Thus, those offering connected devices “should be clear about what data they collect, for what purposes and how long this data is retained.” In information ethics, the notion of transparency refers to the visibility of information, intentions or behaviours, and therefore solutions should implement the privacy by design principle in order to be transparent about data collection, processing and use, and whether data will be distributed to third parties.
|10:30-11:15||Zeki Erkin, TUD
Privacy-preserving Data Aggregation in Smart Cities
Millions of IoT devices are distributed across big cities, collecting variety of sensory data. It is highly beneficial to utilise them e.g. for better city planning, optimisation of public transportation and generating new and custom services for the citizens. Unfortunately, the data collected are mostly very privacy sensitive; they can be misused, re-purposed or stolen. In this talk, we are going to address privacy enhancing technologies, particularly for aggregating sensitive data without leaking personal information.
|11:15-12:00||Sandro Etalle, TU/e
Rethinking Security for IoT
It is evident that the IoT is going to be much more difficult to defend than standard computer systems, which are already no match for professional attackers. To cope with the security and privacy challenges of the IoT we need to completely rethink our way to address security issues. In this presentation I will illustrate my personal view on the road ahead.
|14:00-15:00||Paul Koster, Philips Research Lab
IoT Security in the Real World
Despite IoT security getting a lot of attention both in academia and industry, IoT security practices in the real world are below par and only slowly improves. This presentation explores this gap along cases of IoT security in healthcare and smart living. It shows that some key distinguishing properties of IoT, e.g. semi-unmanaged intelligent devices operating in hostile environments, are not well addressed by IoT security concepts and technology. It also highlights the importance of context and the particular challenge of usable security, designing-in end-users as part of IoT security and the implied compromises.
|15:30-16:15||Marco Caselli, UT
Specification Mining for Intrusion Detection in Networked Control Systems
In this talk I will discuss a novel approach to specification-based intrusion detection in the field of networked control systems. The approach reduces the substantial human effort required to deploy a specification-based intrusion detection system by automating the development of its specification rules.
|16:15-17:00||Gergely Alpár, OU and RU
Cookie in the fridge -- privacy problems with the Internet of Things and some ideas how to fix them
Cookies are one of the main elements of web technologies today. They make the link between web-site visitors and organisations. There are multiple things that can go wrong; and do go wrong here. The Internet of Things is a new communication platform between humans and machines. Since it has been created by the same technological trends as web cookies, they inherit some of the same problems. These problems, most related to privacy, have broad consequences. In this thought-provoking talk, I will discuss phenomena that seem to be unavoidable, yet they can (and probably should) be changed. The group that can primarily influence the current trends is exactly the group of computer scientists, that is, YOU!
FRIDAY 11 NOVEMBER
|09:30-10:30||Rob van Glabbeek, Data 61, CSIRO (Aus)
Process Algebra for Network Protocols
Wireless Mesh Networks (WMNs) are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transport, mining, video surveillance, etc. Unfortunately, they still do not live up to expectations. One of the main factors is the sad state of affairs of the underlying communication protocols that aim to find the best paths through a network. Routing protocols for WMNs are traditionally specified in English prose, and consequently are riddled with ambiguities, contradictions and underspecification. Implementations accordingly show undesirable behaviour, such as routing loops.
This talk advocates formal methods in general, and process algebra in particular, as an alternative methodology for specifying, analysing and verifying (communication) protocols. I give a brief overview of our work in this area, which includes the development of a process algebra for WMNs, and its application to prove loop freedom of the Ad hoc On-Demand Distance Vector routing protocol, one of the main standards for routing through WMNs. The latter required some adaptations to the specification, as the original protocol is not loop free. I will illustrate that our modular proof strategy makes it easy to check that crucial correctness properties, like loop freedom, are preserved under changes in the specification. Through automatic translation from process algebraic-specifications to the input language of model checkers, like UPPAAL, proposed protocol specifications can be tested on the fly using model checking techniques.
|11:00-11:45||Jorge A. Pérez, RUG
Logical Foundations for Concurrency and Distribution: Overview and Recent Developments
Developing correct communication-centric programs is hard. Two major challenges that developers face are ensuring that protocol messages are sent/received in the intended order, and that concurrent protocols interact safely. The interplay of concurrency and distribution add further challenges. To tame this complexity, developers need structures that make interaction protocols explicit throughout the development process.Behavioral type systems are an approach to protocol conformance that codifies communication structures as types for concurrent programs. In this talk I will introduce a logically motivated theory of behavioral types, which results from a tight correspondence with Girard’s linear logic: a Curry-Howard isomorphism for concurrency. I will present the key elements of this correspondence, but also recent developments on its application for the analysis of multiparty protocols (choreographies).
|11:45-12:30||Mauricio Cano, RUG
A Reactive Interpretation of Session-Based Concurrency
I will present ongoing work on the principled development of communication-centric software systems, in which distributed entities (say, Web services) interact by following precise protocols. Our approach is based on behavioral types for concurrency, a class of type systems that classify the interactive behavior of channels in programs. In particular, we investigate implementations of session-based concurrency, the interaction model induced by session types (a widely studied class of behavioral types). Our goal is to consistently integrate the disciplined concurrency (as induced by session types) and reactive behavior, an increasingly relevant feature in many real-world interaction scenarios. I will discuss the challenges involved in this integration, and also preliminary results for ReactiveML, a functional programming language.