Peter MarwedelPeter Marwedel
Title: Cyber-physical systems: opportunities, challenges and (some) solutions
Abstract: The term “cyber-physical systems” characterizes the integration of information and communication technologies (ICT) with their physical environment. This integration results in a huge potential for the development of intelligent systems in a large set of industrial sectors. The potential will be covered in the first part of the talk. Sectors comprise industrial automation (“industry 4.0”), traffic, consumer devices, the smart grid, the health sector, urban living and computer-based analysis in science and engineering. A multitude of goals can be supported in this way, e.g., the availability of higher standards of living, higher efficiency of many processes, the generation of knowledge and safety for the society.
However, the realization of this integration implies manifold challenges. Challenges covered in the second part of this talk include security, timing, safety, reliability, energy efficiency, interfacing, and the discovery of information in huge amounts of data. Also, the inherent multidisciplinarity poses challenges for knowledge acquisition and application.
In the third and final part of the talk, we will present some of our contributions addressing these issues. These contributions include real-time virus detection using an advanced sensor, resource-aware mapping of machine-learning applications to multi-cores, an integration of a timing model into the code generation process, techniques for improving the energy efficiency of CPS applications, tradeoffs between timeliness and reliability and approaches for education crossing boundaries of involved disciplines.
Title: Real Time Model Checking, Performance Evaluation, Synthesis and Optimization
Abstract: Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has been developed allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL CORA providing efficient support for optimization, UPPAAL TIGA allowing for automatic synthesis of strategies for given safety and liveness objectives, and UPPAAL SMC offering a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata. Most recently the branch UPPAAL STRATEGO has been released supporting synthesis (using machine learning) and evaluation of near-optimal strategies for stochastic priced timed games. The lecture will review and provide on-line demonstrations of the various branches of UPPAAL as well as their concerted applications to a range of real-time and cyber-physical examples.
Jan Madsen
Title: The Future of Advanced Cyber-Physical Microsystems
Abstract: With embedded systems, we have focused on making things in our environment smart, by integrating computing power into them. With the introduction of Cyber-Physical Systems (CPS), we have emphasised the interaction of the computing system with its physical environment. However, as other technologies get digitised and miniaturised, we are able to integrate part of the physical environment into our computing devices. This talk will outline the trends and challenges of integrating microfluidic biochips with our computing devices. The talk is split in two parts:
Part 1: Microfluidic biochips are replacing the conventional biochemical analysers, and are able to integrate on-chip all the necessary functions for biochemical analysis at the micro scale. There are several types of microfluidic biochips, each having advantages and limitations. In flow-based biochips the microfluidic channel circuitry on the chip is equipped with chip-integrated micro-valves that are used to manipulate the on-chip fluid flow. By combining several micro-valves, more complex units like mixers, micro-pumps, multiplexers etc. can be built up, with hundreds of units being accommodated on one single chip. In droplet-based biochips, the liquid is manipulated as discrete droplets on an electrode array. For both types of biochip, the synthesis process, starting from a biochemical application and a given biochip architecture, determines the resource allocation, binding, scheduling and placement of the application operations, resembling the mapping process for multi-core microelectronics. The first part of the talk will illustrate how techniques and methods from multi-core microelectronics can be used to solve synthesis and optimization problems of microfluidic biochips.
Part 2: Microfluidic biochips allows for manipulation of very small volumes of liquid, from micro- and nano-litre, down to pico-litre volumes. These are volumes at the size of living cells and bacteria. An interesting application of microfluidic biochips is the study and manipulation of living cells, with the aim to obtain deeper insights into the inner workings of living cells and to use this knowledge to re-program the behaviour of living cells by systematically changing parts of their DNA. The second part of the talk will outline the basic functions and processes taking place within a living cell and illustrate how microfluidic biochips can be applied to provide a fully integrated platform for cell re-programming.
Title: Hybrid Systems: An Introduction
Abstract
Aim: The technological developments of the past two decades have nurtured a fascinating convergence of computer science and electrical, mechanical and biological engineering. Nowadays, computer scientists work hand in hand with engineers to model, analyze and control complex systems, that exhibit discrete as well as continuous behavior. Examples of such systems include automated highway systems, air traffic management, automotive controllers, robotics and real-time circuits. They also include biological systems, such as immune response, bio-molecular networks, gene- regulatory networks, protein-signaling pathways and metabolic processes. The more pervasive and more complex these systems become, the more is the infrastructure of our modern society relying on their dependability. Traditionally however, the modeling, analysis and control theory of discrete systems is quite different from the one of continuous systems. The first is based on automata theory, a branch of discrete mathematics, where time is typically abstracted away. The second is based on linear systems theory, of differential (or difference) equations, a branch of continuous mathematics where time is of essence. This course is focused on the principles underlying their combination. By the end of this course the students will be provided with detailed knowledge and substantial experience in the mathematical modeling, analysis and control of hybrid systems.
Subject: Hybrid automata as discrete-continuous models of hybrid systems. Executions and traces of hybrid automata. Infinite transition systems as a time-abstract semantics of hybrid automata. Finite abstractions of infinite transition systems. Language inclusion and language equivalence. Simulation and bisimulation. Quotient structures. Approximate notions of inclusion and simulation. State logics, and model checking. Partition-refinement and model checking within mu-calculus. Classes of hybrid automata for which the model-checking problem is decidable. Modern overapproximation techniques for reachability analysis.
Title: Dynamic Resource Management for Multicore Linux Platforms
Abstract: Feedback techniques have been used in computer systems for quite some time. However, around 15 years ago the area started to ahieve increased attention and since then applications have been derived in everything from embeddded systems with real-time constraints, over desktops, to distributed systems, and cloud infrastructures. This presentation will describe the basis of this together with different examples. The focus here will be CPU resource management for Linux-based multi-core platforms. A resource manager developed within the European ACTORS project is presented and demonstrated using a multimedia demo. The approach combines integer programming with feedback in order to decide the application service levels and the amount of resources allocated to each application. In the second part an approach is presented that is only based on feedback and for which formal convergence analysis results can be derived. This resource manager is inspired by ideas from game theory. At the end it will be shown how these techniques directly carries over to management of web services executing in cloud datacenters.
Title: Cyber-Physical Systems Challenges in Social Spaces
Abstract: According to the United Nations, today, 54% of the world population lives in cities. This percentage will increase to 66% by 2050. Modern communities can be made more efficient by utilizing computational and networking assets for managing the exploitation of physical resources, leading to cyber-physical systems in social spaces. Examples include disaster response, intelligent transportation, and sustainability management to name a few. According to the US National Institute of Standards and Technology, cyber-physical systems currently account for more than $32 trillion in global economic activity, a number that is projected to grow. The talk will focus on cyber-physical applications in social spaces. These applications break the traditional "closed system" paradigm. They may feature tens of thousands if not millions of inputs that do not come from well-designed specialty sensors, but rather from households, people, cars, and other open sources whose reliability is unknown. Indeed, humans are the drivers in transportation applications, the survivors in disaster response scenarios, and the consumers in energy distribution systems. Humans are also in possession of increasingly many sensing platforms, such as cameras, GPS devices, Internet-connected cars, smartphones, smart watches, wireless energy metering systems, and activity monitoring wearables. To reduce the cost of infrastructure investment and facilitate retrofitting, new smart city applications will exploit these existing sensors in creative ways to make inferences about physical states of interest, such as traffic flow, energy consumption, or post-disaster damage. This talk presents recent analytical and experimental results on interfacing the world of cyber-physical applications and social systems. Examples are presented of reliably observing real-world events (such as hurricanes, earthquakes, and civil unrest) using unreliable human sources. The talk concludes with open challenges in this emerging area of embedded systems research, where humans are active contributors to observation and actuation tasks.
Insup Lee
Title: Toward Plug & Play Medical Cyber-Physical Systems
Abstract: There is a growing interest in plug & play systems in domains such as healthcare, where multiple medical devices are assembled at the bedside to coordinate with each other. Such plug & play medical device cyber-physical systems (MCPS) would help to provide better medical treatment to patients. For example, they can provide better physiologic alarms (by combining data streams from multiple medical devices) and closed loop control (by using physiologic sensors to drive actuators). MCPS are safety-critical systems, and thus they need to be evaluated for safety by regulators before they can be used. The state of the art in safety assessment is to consider the complete system. However, unlike other safety-critical systems such as aircrafts and nuclear plants, plug & play MCPS are constructed at bedside, based on the needs of an individual patient and from available devices. The challenge is how to assess the safety of plug & play MCPS a priori if we don’t know precisely what medical devices (i.e., make, model, brand, etc.) will be used in the instantiation?
There are several on-going efforts to support interoperability between medical devices using open standards. Based on standards, it is envisioned that MCPS would be assembled on-demand since they should be put together for a particular clinical scenario using available medical devices as needed, instead of having dedicated a set of medical devices developed and pre-configured for each clinical scenario. Such an on-demand assembly of MCPS requires a new paradigm to guarantee the safety of clinical applications using the MCPS. In contrast, currently practiced technologies for safety-critical systems assume that the system will be fully designed, manufactured, and tested prior to the customer. The main reason is that safety and effectiveness are emergent system-level properties and whether the properties are satisfied depends on the interactions among the system’s components.
This lecture will discuss several topics related to on-demand MCPS, including the current state of the art, challenges and needs, medical application platforms, formal modeling and analysis of medical devices and medical scenarios, ecosystem to support plug & play MCPS, assume-guarantee compositional proof rules for plug & play MCPS, and assurance case patterns for medical apps.
Title: A quick tour on Statistical Model Checking
Abstract: The two lectures are focused on Statistical Model Checking, that is a simulation-based approach for stochastic validation of potentially complex properties.