Filters

Settings

Now showing1 - 7 of 7
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: without files ,
    Time-Constrained Model Checking and Verification-Aware System Design for Medical Cyber-Physical Systems
    Medical cyber-physical systems (MCPS) face two challenges: the complexity of the patient and a potentially high risk. Particularly, more autonomous systems often have to adapt to the patient's internal state. While there is growing interest in studying possible benefits of smarter and more autonomous MCPS for patients and physicians, safe operation is one key concern. Having rigorous and comprehensible guarantees for safe system behavior could therefore raise the acceptance of such systems in clinical practice.Formal methods and particularly the technique of model checking can in principle provide such guarantees. But classical model checking runs offline and requires complete models up-front; yet, models of physiological processes are complex and incomplete. If one shifts verification from offline to online, complete models are no longer required because one can use sensor data available at run time to fill in missing values so, that it becomes possible to give formal guarantees at least for relevant time windows in the near future. An MCPS aware of the verification thus has the chance to adapt, at run time, not only to the patient, but also to the verification itself. The online model checker, however, now becomes constrained by the time window available for verification.In this proposal we assume that model checker and MCPS form a control loop that executes repeatedly under (soft or hard) time constraints and investigate how their mutual dependency can be exploited to enable model checking where otherwise model complexity or time constraints would prevent formal verification. Embedded in a feedback loop, the model checker may need to prioritize critical properties over weaker guarantees where, e.g., lower confidence is acceptable. Considering the model checker's output, the MCPS may adapt to allow for "sufficient" model checking, e.g., by changing its speed.We develop a verification-time analysis that can weigh between precision and overhead. Further, we introduce a domain-specific language supporting the prioritization and abstraction of logical properties, to configure model checking accordingly. Verification-aware design of MCPS implies a tight integration and interaction with model checking in a real-time and synchronized fashion. We study system adaptation as a multi-criteria optimizing problem of maximizing system efficiency while maintaining patient safety. The methods are developed and evaluated in the context of two actual application scenarios: motion compensated radiation therapy and robotic needle placement.
      73
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: without files ,
      155
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: without files ,
    Data Quality Explored (HOOU-Projekt)
    Das englischsprachige Lernangebot “QuaXP - Data Quality Explored” hat sich zum Ziel gesetzt, für die Bedeutung hoher Datenqualität beim maschinellen Lernen zu sensibilisieren. An ausgewählten Themen können Lernende praktisch erfahren, wie Daten gesammelt, aufbereitet und eingesetzt werden sollten, um bestmögliche Ergebnisse zu erzielen.
      83
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: without files ,
      747
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: with files ,
    Entwicklung einer Softwarearchitektur zur Steuerung Roboter-gesteuerten Probenahme und Entfernung potentieller Tumoren per theragnostischem Picosekunden-Infrarot-Laser
    Mithilfe der Kombination eines Roboter geführten PIRL-Skalpells, einer Optischen Kohärenztomografie (OCT) zur Erkennung von Unterschieden im Gewebe und Zielloordinaten-Bestimmung für die Roboter gesteuerte Laser-Ablation sowie einer Vorrichtung zum Einfangen des Gewebedampfs für massenspektrometrische Diagnostik sollen z.B. Tumore zielgerichtet erkannt werden und durch präzise Roboter-gesteuerte Ablation mit PIRL durch Verdampfung entfernt werden. Aus dem dem kondensierten Gewebedampf sollen über Massenspektrometrie detaillierte diagnostische Informationen über die Art des Tumors gewonnen werden, um sicherzustellen, dass der Tumor vollständig entfernt ist. Dafür ist eine leistungsfähige Software-Architektur notwendig, die Schnittstellen definiert und implementiert, um die unterschiedlichsten technischen Module (OCT/Roboter/PIRL/Massenspektrometer) zu verbinden. Das Ziel ist daher, eine Software-Architektur zu entwickeln, die eine zuverlässige Kommunikation zwischen den einzelnen Systemkomponenten erlaubt und die Echtzeit-Steuerung von Roboterbewegungen und PIRL-Parametern sowie die räumlich und zeitlich konsistente Speicherung von OCT-Bilddaten und Massenspektromiedaten ermöglicht.
      1195  6
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: without files ,
    MaLiTuP - Machine Learning in Theory and its Application
    The project aims at developping and permanently establishing a qualification program called "Machine Learning in Theory und Practice" in order to teach the fundamentals of the field of machine learning to Master's students in logistics at TUHH.
      170
  • Some of the metrics are blocked by your 
    consent settings
    Item type:Project, Access status: without files ,
      56