My research primarily focuses on modeling and reasoning approaches all the way from low-level sensor networks to high-level qualitative situation awareness. I work on modeling and verification of hybrid systems with an application to robotics, intermodal traffic situation awareness and situation awareness in road traffic management. Mostly, I use data from existing information systems. To complement those with on-demand deployed sensor networks, I created a toolbox to easily model sensor network applications.
Besides my research on hybrid systems, I also applied qualitative situation awareness techniques to purely virtual data in social network analysis.
Cyber-physical systems (CPS) are operated in many safety-critical areas where lives are at stake, such as in road traffic and robotics. CPS are almost impossible to get right without proper analysis of their behavior, which emerges from combined discrete dynamics (the cyber part, e.g., setting the acceleration of a car) and the entailed continuous dynamics (the physical part, e.g., motion of a car). Thus, formal verification techniques to analyze CPS are of paramount importance to provide correctness guarantees for all of the infinitely many possible states of a CPS - not just for some, as in testing or simulation.
Formal verification rests on models of a CPS, which capture these infinitely many possible states. Current methods make a trade-off between full automation and modeling expressiveness: Reachability analysis methods focus on full automation and are therefore restricted to less expressive classes of CPS. Theorem proving methods, in contrast, rely on human guidance to make progress despite undecidability so that more realistic models can be verified. To make human guidance possible, however, the inherent complexities of CPS practically mandate incremental development, which requires full re-verification after every change with current theorem proving methods. At the same time, we want the correctness properties that are verified formally for a model also to hold for an actual implementation. For this, we have to resolve a gap between modeling concepts that are beneficial for verification (e.g., non-deterministic control) and those that are appropriate for implementation (e.g., deterministic control) in a way that preserves correctness.
The vision of this project is to reduce verification effort despite incremental CPS engineering, and at the same time ensure implementation correctness despite conceptual gaps to modeling.
To work towards achieving this vision, we will base on our prior experience with CPS to make the concepts, methods, techniques, and tools for incremental engineering of CPS proof-aware.
Funding: FWF P28187-N31
Computers that control physical processes, thus forming so-called cyber-physical systems (CPS), are today pervasively embedded into our lives. For example, cars equipped with adaptive cruise control form a typical CPS, responsible for controlling acceleration on the basis of distance sensors. Further prominent examples can be found in many safety-critical areas, such as in factory automation, medical equipment, automotive, aviation, and railway industries. From an engineering viewpoint, CPSs can be described in a hybrid manner in terms of discrete control decisions (the cyber-part, e.g., setting the acceleration of a car to keep safety distance) and in terms of differential equations modeling the entailed continuous dynamics of the physical world under control (the physical part, e.g., motion).
The key challenge in engineering CPSs is the question of how to ensure their correct functioning in order to avoid incorrect control decisions w.r.t. safety requirements (e.g., a car with adaptive cruise control will never collide with a car driving ahead). This overall challenge is even reinforced by the fact that evolution is inherent to engineering CPSs due to incremental development being frequently applied to cope with their complexity. For example, common practice is to start with a simple CPS model (e.g., apply only maximum braking power), prove its correctness in a typically laborious process, and incrementally extend the model (e. g., choose between maximum and moderate braking power) to better reflect the real-world CPS (i. e., refactor the model while ensuring preservation of safety constraints).
The vision of Sphinx is to address this question with a modeling environment for verification-driven engineering. The modeling environment should support model refactoring and corresponding proof adaptation for CPSs. In particular, I will deal with the following research questions:
Funding: ERC Marie Curie PIOF-GA-2012-328378-Sphinx
Traffic management, emergency rescue, and military operations are domains that naturally exhibit several control systems. These are operated by different authorities in a distributed manner, share an environment, are information-intensive and constantly evolving. In such distributed control systems, authorities pursue individual goals and independently collect a vast amount of specific information. As a consequence, each authority has only a restrained view on the shared environment. This hampers effective collaboration, which requires awareness about simultaneously occurring and mutually affecting situations and possible control measures. Todays system support is insufficient for collaborative situation awareness, since it induces huge communication efforts, potential misunderstandings, information overload, and timely pressure on the human system operators. This ultimately endangers the operators’ ability to respond to critical situations.
The main goal of the CSI project is to propose novel semantic methods and technologies for collaborative situation awareness. Motivated by this overall research focus, CSI provides answers for three unique but highly interwoven research questions:
Large-scale control systems, as encountered in the domain of road traffic management, typically deal with highly-dynamic environments. Those provide a vast amount of information about a large number of real-world objects. The information items, which originate in multiple heterogeneous sources, are anchored in time and space. In such systems, human operators are at permanent risk to get lost in the induced information overload. As a result, they fail to be aware of the overall meaning of the available information and its implications.
The main goal of this project was to create an ontology-driven framework for supporting situation awareness in large-scale control systems. We developed a situation awareness ontology to facilitate the specification of domain-independent rules for detecting relevant situation. These rules use qualitative spatio-temporal reasoning techniques. We extended the concept of conceptual neighborhood between spatio-temporal relations to assess possible future situations.
Wireless Sensor Networks in general and Body Sensor Networks in particular enable sophisticated applications in pervasive healthcare, sports training and similar domains. Their main goal is to derive context from raw sensor data with feature extraction and classification algorithms. Typical body sensor networks not only comprise a single sensor type or family, but often combine different hardware platforms (e.g., sensors to measure acceleration or blood-pressure). As a result, the questions arises of how to efficiently deal with these heterogeneous platforms and programming languages. In this project, we developed a distributed signal processing framework based on TinyOS and nesC. The framework forms the basis for a Model-Driven Software Development approach. Models raise the level of abstraction and hide implementation specifics of the framework in a Platform Specific Model. A Platform Independent Model further lifts modeling to functional and non-functional requirements independently from platforms. We used sensor networks for activity recognition (e.g., walking vs. sitting) as well as for indoor localization.
Online social networks have seen enormous growth over the past few years and now reached truly widespread adoption. However, social networkers are present in several different networks, since every social network focuses on serving quite specific human needs. This leads to scattered social content with the potential pitfall of untargeted services like indiscriminated product offers. This situation is further aggravated by the fact that social networkers are particularly reluctant to share social content with service providers, especially when they are not in control of how their social content is being exploited.
In the course this project, we developed a system whose main goal is to exploit the encouraging win-win situation between social networkers and service providers with respect to personalization. For this, we leverage semantic-based techniques for integrating, profiling and privatising social content. TheHiddenU provides a single point of access to social networks in terms of an integrated semantic representation of scattered social content. It uses semantic-based profiling mechanisms in order to discover hidden facts. Finally, TheHiddenU focuses on privacy concerns by providing social networkers with awareness and ample control regarding disclosure and usage of their social content.