Dependable Things/Events/3rd Symposium on Dependable Internet of Things in Adverse Environments/Detailed Program
Detailed Program
Date: September 22, 2022
Location: Graz University of Technology, Lecture Hall G, 3rd floor, Kopernikusgasse 24, 8010 Graz, Austria
| Time-slot | Program |
| 09:00-09:15 | Opening words by Prof. Horst Bischof, TU Graz |
| 09:15-10:15 | Explainable and Verifiable Machine Learning - A Grand Challenge for Computer Science |
| Keynote by Prof. Kim Larsen, Aalborg University | |
| Abstract: Learning-based components in general and Neural Networks in particular are increasingly used in general and Neural Networks in particular are increasingly used in safety-critical systems, e.g., autonomous vehicles, smart energy grids, traffic control systems and several other complex and critical infrastructure systems. In such cyber-physical systems (CPS), which connect the physical and the digital world, ... (more) | |
| 10:15-10:45 | The future of automation will accelerate with IT-Capabilities Abstract: Today´s automation is what we know as Operational Technology (OT).
The dependencies are obvious, environments as of today are adverse. Let´s make the |
| 10:45-11:10 | Coffee break |
| 11:10-11:40 | Dependable Internet of Things - Challenges, Results, and Impact |
| Prof. Kay Römer, TU Graz | |
| Abstract: In the first ever TU Graz LEAD project which was devoted to making the Internet of Things dependable also in harsh environments, about 40 key researchers, associated researches, postdocs and phd students carried out research during the past 6 years in three main areas: wireless communication and position estimation, security and correctness, as well as multi-agent systems involving networked control and artifical intelligence. This opening presentation of the symposium gives an overview of the main research challenges, key results and impact of this research program. | |
| 11:40-12:00 | Dependable Wireless Communication and Localization |
| Prof. Klaus Witrisal, TU Graz | |
| Abstract: Harsh environments -- characterized e.g. by severe multipath propagation and/or radio interference -- cause severe impairments on wireless communication and positioning systems. A joint approach is being taken in the project to overcome these impairments, addressing the problem from the directions of antenna design, wireless networking, and physical layer signal processing. It is proposed to map performance metrics of the wireless systems geographically in order to scale the system in an efficient manner towards large-scale deployments, many agent nodes, and highly dynamic agents considering ultra-wideband and mm-wave radio nodes. This talk will illustrate the challenges posed on wireless systems in harsh environments, the concept of location awareness to map channel properties spatially, and modeling aspects that are the basis of robust, location-aware transceiver algorithms for harsh environments. | |
| 12:00-12:10 | mmWave Frontends for Dependable Wireless Communication and Localization Systems |
| Gerzon Gomes Bravo, TU Graz | |
| Abstract: Location-based service is a primary service of the IOT, while localization accuracy is a key issue. mm-Wave wireless systems have the potential to improve the accuracy of said systems while supporting single-anchor operation. Together with the use of adaptive beam switching are the key to overcome the limitation of current localization systems. | |
| 12:10-12:20 | Robust radio-based Localization and Tracking for Obstructed-Line-of-Sight Situations |
| Alexander Venus, TU Graz | |
| Abstract: We present an algorithm for localization and tracking in multipath-prone environments that is able to operate reliably, even if a temporary obstruction of one or all anchors occurs. The proposed graph-based algorithm employs adaptive probabilistic data association to infer the position of a mobile agent, using delay and amplitude of multipath components (MPCs) as well as their respective uncertainties. By employing a non-uniform clutter model, the algorithm exploits position information contained in the MPCs as to strengthen the line-of-sight hypothesis. Using real radio measurements, we show that the algorithm performs robustly, even if a temporary obstruction of all anchors occurs simultaneously. | |
| 12:20-12:30 | UWB in Large-Scale Real-World Deployments |
| Maximilian Schuh, TU Graz | |
| Abstract: Due to its excellent localization performance UWB has rapidly gained popularity in IoT applications. In fact the number of UWB devices is expected to grow significantly, as UWB radios are currently deployed in more and more end-user products such as car-access systems or smartphones. Therefore, testing facilities are necessary, that are capable to test large-scale UWB systems in real-world environments. | |
| 12:30-12:40 | The emergence of Ultra-wideband as the fastest growing wireless technology |
| Dr. Bernhard Großwindhager, NxP Semiconductors | |
| Abstract: The history of Ultra-wideband (UWB) dates back to the 90’s and even earlier. However, just in recent years UWB made its breakthrough as a common wireless technology for Automotive, Mobile, and IoT. Starting as a pure ranging and localization technology, UWB is now entering new markets and applications such as Radar-based presence detection. This presentation gives an overview over future UWB applications and the role of NXP in the build-up of a worldwide UWB ecosystem. | |
| 12:40-13:40 | Lunch Break |
| 13:40-14:00 | Verified Dependability |
| Prof. Bernhard Aichernig, TU Graz | |
| Abstract: In this talk we give an overview of our research on verifying IoT components, with a special focus on security and real-time properties. We approached the verification problem from different angles: (i) formal verification with model checking and theorem proving provide the highest levels of assurance at design-time. We developed methods to prove the correct design and implementation of central parts of real-time operating systems, including the port to different hardware platforms. Furthermore, we investigated novel verification techniques to protect against side-channel attacks.(ii) Learning-based testing and model inference is applied where formal verification is not possible, e.g. for third-party components. Here, we identified several issues in implementations of the IoT protocols MQTT and Bluetooth Low Energy. (iii) Since testing will always be incomplete, we also researched run-time enforcement techniques for controllers to protect against unsafe behaviour with verified fallback mechanisms. The decision logic when to switch into a save mode is automatically synthesised out of a formal specification. | |
| 14:00-14:10 | Secure and Efficient Masking using Formal Verification |
| Barbara Gigerl, TU Graz | |
| Abstract: Cryptographic devices are susceptible to physical side-channel attacks, which are usually defeated using the masking countermeasure on algorithmic level. In a first step, we focus on the security of masked software implementations and their execution on microprocessors using formal approaches. We particularly focus on physical side-effects such as glitches within the microprocessor's hardware, which might be a servere thread to the security of masked implementations. In a second step, we extend this formal approach to the arithmetic domain, which is especially relevant for side-channel protection of post-quantum cryptography. | |
| 14:10-14:20 | Runtime Enforcement for CPS with Proofs on Demand |
| Benedikt Maderbacher, TU Graz | |
| Abstract: The ubiquitous application of CPS in safety critical settings demands for a conclusive formal verification of such systems, which is most often infeasible to achieve. We address the problem of guaranteed correctness for CPS by presenting a methodology to compute a correct-by-construction Simplex architecture. The simplex architecture consists of an advanced controller, a verified base controller and a switching logic to switch from the advanced controller to the base controller whenever needed to enforce safety. Our novel algorithm uses proofs-on-demand techniques to automatically construct a switching module that minimizes interference, thereby maximizing performance, while guaranteeing safety. | |
| 14:20-14:30 | Learning-Based Fuzzing of IoT Protocols |
| Andrea Pferscher, TU Graz | |
| Abstract: Security testing in the IoT is a challenging task since many heterogenous black-box components interact with each other. During the first phase of the LEAD project, learning-based testing successfully revealed issues in IoT protocols. To investigate security-critical aspects of IoT protocols, we extended learning-based testing by fuzzing techniques. In my talk, I will introduce the application of learning-based fuzzing on two different IoT protocols, namely MQTT and Bluetooth Low Energy, and present revealed security vulnerabilities and reliability issues. | |
| 14:30-14:40 | Formal Verification of RTOS |
| Anton Saikia, TU Graz | |
| Abstract: To meet the need for developers to provide guarantees that the Real-Time Operating Systems (RTOS) that run IoT systems are reliable, formal verification is an comprehensive and effective method. The model-checking tool UPPAAL has been used for this purpose to verify non-functional properties such as schedulability and power consumption. As proof of concept we perform this research for MCSmart OS and AUTOSAR. | |
| 14:40-14:50 | Model Learning for Dependable Machine Learning |
| Dr. Martin Tappler, TU Graz | |
| Abstract: During Phase 1 of the Dependable Things project in subproject Dependable Composition, we combined model learning, search techniques, model-based testing, and formal verification to check dependability of reactive software systems, such as, IoT protocols. An inter-subproject case study in platooning, where we combined these techniques with machine learning, paved the way towards my current research. In ongoing collaborations, we view machine-learned systems as reactive systems that we analyze through techniques, such as model learning, search-based testing, and formal verification. In my talk, I will showcase results from two recent works on reinforcement learning (RL): (1) runtime enforcement of RL agents guided by learned Markov decision processes and (2) search-based testing of deep reinforcement learning. | |
| 14:50-15:20 | Coffee break |
| 15:20-15:40 | Towards Dependable Networked Systems |
| Prof. Gerald Steinbauer-Wagner, TU Graz | |
| Abstract: Complex industrial applications such as modern production lines or complex robotic systems are highly networked dynamic systems embodying hierarchical control structures consisting of fast and reactive as well as slower and deliberative control. Fault diagnosis and fault tolerant control are key techniques for dependable networked systems. By employing observer techniques discrepancies between nominal and real system behavior are detected. These discrepancies are interpreted by exploiting either deterministic or probabilistic inference techniques. Based on the successful cooperation between control and communication theory in the first phase of the Lead Project, additional expertise from artificial intelligence, i.e., from probabilistic inference as well as from planning and execution monitoring made important scientific contributions towards the systematic design of dependable networked systems. | |
| 15:40-15:50 | Message Passing in Probabilistic Models |
| Dr. Christian Knoll, TU Graz | |
| Abstract: Probabilistic graphical models are flexible models for representing complex high-dimensional distributions and for incorporating domain knowledge in an intuitive and expressive way. For making probabilistic inference, one often relies on recursive message passing methods. While these methods are efficient for restricted model classes (e.g., for trees), they only serve as approximation methods for more complex models. In this talk, I will show how we can enhance the performance of message passing methods from two opposing angles: either by simplifying the model itself with the utilized inference method in mind or by modifying the inference method with the underlying model in mind. | |
| 15:50-16:00 | State Estimation and Fault Detection for Complex Dynamical Systems |
| Dr. Markus Tranninger, TU Graz | |
| Abstract: Reliable diagnosis of dynamical systems is crucial in order to adequately react to problems and hence to guarantee dependability. In our work, we developed model-based estimation techniques which allow to detect discrepancies between the expected and the real behaviour of a system. Together with the structural properties of the underlying model, our methods allow to reliably detect faults and to determine their root cause in real-time. | |
| 16:00-16:10 | Packet Communication Outcome as a Stochastic Process |
| Hadi Gharibdoust, TU Graz | |
| Abstract: In a control system, the feedback mechanism is used for stablization or improving the performance. Network Controlled Systems (NCS) are control systems with the feedback loop that is closed over a Network. For many reasons such as inapproachability, it might be impossible to stablize the system locally. Then NCSs are used to maintain stability over the packet network. Network impairments such as packet loss and delay can force the system to instability. Consquently, an accurate model of such impairments is paramount for preventing system failure. In this work, a systematic approach is developed for identifying the stationarity and dependence in non-numeric random processes using the approaches developed for numeric processes such as autocorrelation. Subsequently, many models including homogeneous and inhomogeneous Bernoulli, Markov and polyphaser Markov, and hidden Markov models are studied. They are evaluated based on their log-spectral distance from the measurements. The results suggest that due to strong unstationarity and time-varying conditional probabilities,inhomogeneous Bernoulli model best characterizes the process for it does not make invalid assumptions though it only models the slowly varying feature of the process. | |
| 16:10-16:20 | Supporting Long-term Robot Autonomy using Model-based Engineering |
| Stalin Munoz Gutierez, TU Graz | |
| Abstract: Long-term robot autonomy (LTRA) requires a high degree of dependability from robotic solutions. Model-based engineering (MBE) methods and technologies are ideal for implementing dependable systems. Here we present the application of MBE to develop a dependable architecture for LTRA in the RoboCup Logistics League domain. | |
| 16:20-16:30 | Autonomous Mobile Robots - The Moving Networked Control Systems |
| Dr. Jakob Ludwiger, Knapp Logistik | |
| Abstract: During my employment as a PhD student at the Institute of Automation and Control I developed discrete-time mathematical models and sliding mode control algorithms for networked control systems. My thesis mainly focused on analyzing such systems and their properties from a theoretical point of view. In my talk, I will connect these scientific concepts with the challenges we are currently facing while develping autonomous mobile robots for logistics applications at KNAPP Industry Solutions. | |
| from 16:30 | Poster & Demo Session (fingerfood and coffee served) |