CSB+15_NFM15.pdf - 223.06 KByte

Since about two decades, formal methods for continuous and hybrid systems enjoy increasing interest in the research community. A wide range of analysis techniques were proposed in the literature and implemented in powerful tools. However, the lack of appropriate benchmarks make the testing, evalu...

paper.pdf - 404.86 KByte

We improve thepolicy iteration-based algorithm for value set analysis by giving a new heuristic for policy selection based on a local static analysis. In particular, we detect loops in the program and perform an analysis to discover therelative changesof variables in the loop, that is, whether a ...

A Comparison of Dual-Core Approaches for Safety-Critical Automotive Applications.pdf - 162.38 KByte

Safety is a requirement concerning an increasing number of automotive applications. Recent safety standards set requirements for designing safety-critical systems. Among others, these specifications include a comprehensive detection and handling of hardware faults. Cu...

Arens - ASAIO 2010 - A Dynamic Study on the Hemolytic Effect of Negative Pressure on Blood.pdf - 175.48 KByte

It is often regarded as common knowledge that negative pressure applied on blood causes hemolysis, e. g. during ECMO or cardiac surgery. But in literature there are only few studies with different outcomes and often with static settings. Therefore, we designed a dynamic test set up to study the e...

A GPS-aided Inertial Navigation System.pdf - 1.34 MByte

The accuracy of a low-cost inertial navigation system is highly dependent on the overall accuracy provided by the respective sensors and the quality of the mathematical modeling of the error sources. Sensor fusion allows to alleviate and bound the occurring errors, resulting in increased precisio...

paper.pdf - 154.85 KByte

Static code analysis is a convenient technique to support the development of software. Without prior test setup, information about a later runtime behavior can be inferred and errors in the code can be found before using a regular compiler. Solutions to apply static code analysis to PLC software ...

BMT2011.pdf - 14.32 KByte

Today extracorporeal membrane oxygenation (ECMO) is an ultima-ratio treatment for severe lung injury. Not only the technical complexity of the system and the physiological relationship between the different related parameters, but also the safety issues related to an ECMO cause it to be a very ra...

WESE10.pdf - 2.15 MByte

In current curricula, more and more courses endeavor to give practical examples on the usage of embedded hardware. Either by demonstrations e. g. in lectures or as hands-on practice in lab courses. In order to motivate the students a reference to current technological developments is desired. All...

CASE2018_final.pdf - 190.44 KByte

Heavy-duty slow-rotating roller chains are expensive and time-consuming to replace. Inspections to assess the wear on a chain can only be carried out periodically and usually lead to a standstill of production, which comes with a loss of earnings. Therefore, the incentive to maintain them only wh...

Walter - A physiological model for extracorporeal - EMBC.pdf - 0.98 MByte

Long term extracorporeal membrane oxygenation can be used in cases of severe lung failure to maintain sufficient gas exchange without the need to apply higher ventilationpressures which damage the lung additionally. The use of cardiopulmonary bypass devices is well established inside the operati...

jtres12.pdf - 468.07 KByte

Android belongs to the leading operating systems for mobile devices, e.g. smartphones or tablets. The availability of Android's source code under general public license allows interesting developments and useful modifications of the platform for third parties, like the integration of real-time su...

WESE2019_finalSmall.pdf - 1.74 MByte

We report on a remote test environment for a mandatory undergraduate lab course on microcontroller programming at RWTH Aachen University. Since the course is being attended by up to 320 students each semester, it is not possible to provide comprehensive supervised on-site access to the laboratory...

gbk10.pdf - 228.55 KByte

Formal verification of embedded software is crucial in safety-critical applications, ideally requiring as little human intervention as possible. Binary code model checking based on hardware simulators already comes close to this goal, although with high initial effort for developing a simulator o...

Original_Publication_Springer_Copyright.pdf - 287.57 KByte

In this paper we present how formal methods can be applied to MATLAB programs. We apply a static analysis based on abstract interpretation to derive reachable values and identify potential programming faults fully automatically. Our verification is built on a formalization and abstraction of ...

EMBC19_final.pdf - 1.99 MByte

Thermal imaging is used in medical diagnosis and preventive screening, e.g. breast cancer, cardiovascular disease, and orthopedics. Segmentation algorithms fail to recognize body parts of interest when the temperature difference between the body parts and the background is insufficient. We propos...

CESCIT21_AlgorithmicdistinctionofARDSandHeartFailureinICUdatafrommedicalembeddedsystemsbyusingacomputermodel(1).pdf - 718.39 KByte

Acute Respiratory Distress Syndrome (ARDS) is a common cause for respiratory failure and has a high mortality rate of 30-40% in most studies. The current standard for the diagnosis of ARDS was proposed by the Berlin Definition from 2012. This article proposes an algorithmic classification to dist...

MobiCASE13_Final.pdf - 282.54 KByte

With the booming mobile market and increasing capability of mobile devices, mobile platforms like Android emerge from end-user to industrial application areas. This paper sketches an approach to implement industrial safety-critical embedded systems with fail-safe state on the mobile platform Andr...

cameraready.pdf - 1.5 MByte

This paper presents an overall MAV design with an integrated camera system. It shows the integration of the camera into the hardware and software architecture and how camera information can be used within the logical design for improving flight control. The presented architecture will be tested a...

Full_dernehl_camera_ready.pdf - 345.3 KByte

Today's MAV navigation systems take advantage of GPS in combination with an IMU to derive velocity and position as well as attitude and heading. Ultra-low-cost systems (<500$) for unstable flight vehicles, with their restricted hardware abilities and low measurement quality, use GPS information t...

WESE09_klein.pdf - 463.89 KByte

In addition to lectures on basic theoretical topics nowadays curricula demand more and more practical experiences from the students. Due to the so-called bologna process in Europe the graduation scheme at the department of computer science at RWTH Aachen University was changed, towards Bachelor a...

BBSK_AMICS_final_Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations.pdf - 211.87 KByte

This paper presents a low-level memory and hardware model suitable for analyzing embedded systems software written in high-level languages such as C. The key feature of this approach is that it combines information that can be discovered from the C code itself with information from the executable...

paper.pdf - 338.67 KByte

Critical infrastructure such as chemical plants, manufacturing facilities or tidal barrages are usually operated using specialized control devices. These devices are programmed using domain-specific programming languages for which static code analysis techniques are not widely used yet. This pape...

goebeEtAl_ApplicabilityOfSupervision.pdf - 642.38 KByte

The safety of software-based control systems plays an essential role in a vast number of applications. SynTACS is a tool that generates a framework for controller supervision, which enforces safety during runtime by utilizing the supervisory control theory of Ramadge and Wonham. In this paper, th...

sbk10.pdf - 274.67 KByte

This article describes the application of two abstraction techniques, namely dead variable reduction and path reduction, to microcontroller binary code in order to tackle the state-explosion problem in model checking. These abstraction techniques are based on static analyses, which have to cope w...

bk11b.pdf - 340.89 KByte

This paper describes an approximate quantifier elimination procedure for propositional Boolean formulae. The method is based on computing prime implicants using SAT and successively refining overapproximations of a given formula. This construction naturally leads to an anytime algorithm, that is,...

bbk12b.pdf - 570.81 KByte

This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports static analysis as well as ACTL and past-time LTL model checking using counterexample-guided abstraction refinement for different programming languages used in industry. In the u...

2017-01-0004.pdf - 4.56 MByte

Modern vehicles become increasingly software intensive. Software development therefore is critical to the success of the manufacturer to develop state of the art technology. Standards like ISO 26262 recommend requirement-based verification and test cases that are derived from requirements analysi...

rbs11.pdf - 330.16 KByte

This paper presents a non-intrusive framework for runtime verification of executable microcontroller code. A dedicated hardware unit is attached to a microcontroller, which executes the program under scrutiny, to track atomic propositions stated as assertions over program variables. The truth ver...

aib-main.pdf - 3.28 MByte

This dissertation is concerned with abstract interpretation of programs whose semantics is defined over finite machine words. Most notably, the considered class of programs contains executable binary code, the analysis of which turns out demanding due to the complexity and the sheer number of inv...

bk10.pdf - 388.11 KByte

Traditionally, transfer functions have been manually designed for each operation in a program. Recently, however, there has been growing interest in computing transfer functions, motivated by the desire to reason about sequences of operations that constitute basic blocks. This paper focuses on de...

Kopp - Automatic Control of veno-venous Extracorporeal Lung Assist - Artif Organs.pdf - 262.82 KByte

Veno-venous extracorporeal lung assist (ECLA) is used to provide sufficient gas exchange even in most severe cases of acute respiratory distress syndrome. Commercially available systems are manually controlled, although an automatically controlled ECLA could enable individualized and continuous a...

main_4thVersion.pdf - 352.42 KByte

When a model checker detects a violation of an all-quantified specification, it generates a counterexample trace that explains how to reach a violating state. In the context of PLCs, the counterexample contains the required stimuli for the program to cause erroneous behavior. Although these count...

ECC16.pdf - 275.86 KByte

In this paper we propose a fully automatic technique to generate safety proofs for a given block diagram. Our method computes automatically Lyapunov functions for linear and polynomial systems within a block diagram. User defined safety constraints can be added to our verification algorithm, comb...

TestcaseGenerationForPlcUsingCoverageMetrics.pdf - 234.29 KByte

This paper presents a method for automatic test case generation for PLC software following the IEC61131-3 standard. The core component is a model checker that iteratively creates program traces, each of them covering a part of the program in terms of a coverage metric. These test cases are transl...

bbks10.pdf - 249.14 KByte

In this paper, we propose a new approach to automatically derive invariants from Programmable Logic Controller programs by symbolically rewriting Instruction List code. These invariants describe the relations between all variables and capture the behavior of the program. Usually, invariants are c...

walter-control of extracorporeal oxygenation.pdf - 2.02 MByte

In case of severe lung malfunction (ARDS), conventional artificial ventilation strategies may not be able to maintain physiological gas exchange. In these life threatening situations, extracorporeal gas exchange is one of the last available options to keep the patient alive. Until now, most cente...

Langfassung_Testfallgenerierung.pdf - 366.08 KByte

Langfassung.pdf - 367.83 KByte

In this work we will present a method for automatic test case generation for PLC-software. We support the coverage criteria line coverage and branch coverage. The test cases are generated using a model-checker, which iteratively creates program traces, each of them covering a part of the coverage...

wartzek_automed2009_Automatisierung der extrakorporalen Membranoxygenierung.pdf - 217.85 KByte

Walter - Automatisierung und Fehlerdiagnose bei der ECMO - at 1_2010.pdf - 2.43 MByte

Die Extrakorporale Membranoxygenierung ist eine der letzten Therapieoptionen für schwere Fälle eines akuten Lungenversagens. Hierzu wird Blut in einem externen Kreislauf ähnlich einer Herz-Lungen-Maschine durch einen Oxygenator gepumpt. In diesem findet ein zusätzlicher Gasaustausch statt. Im...

BMT16_JK.pdf - 1 MByte

This paper presents a decentralized safety concept for networked intensive care setups, for which a decentralized network of sensors and actuators is realized by embedded microcontroller nodes. It is evaluated for up to eleven medical devices in5 a setup for automated acute respiratory distress s...

Walter et al - EMBEC 2011 - physiological ecmo control.pdf - 571.12 KByte

Patients suffering acute lung failure depend on artificial ventilation in order to survive. In severe cases even this is not sufficient any more and long term extracorporeal membrane oxygenation is applied as a last chance rescue ther-apy. Adapted from short term cardiopulmonary bypass these mach...

SEFM_2016.pdf - 437.34 KByte

This paper presents a fully automatic verification technique for Simulink block diagrams, by combining a static value range analysis with symbolic execution. Our concept avoids a translation to other languages and, instead, extracts all necessary attributes from Simulink and interprets the model ...

ECC13_1025_FI.pdf - 1.84 MByte

In this paper, we evaluate a number of methods for computing reachable sets using on one hand approximations and on the other hand invariants. We address systems of the form x'(t)=Ax(t)+Bu(t) with uncertain but bounded input function u(t). We introduce our implementation based on zonotopes and us...

06004514.pdf - 324.42 KByte

Model based testing techniques are a breakthrough in the modern software development. The integration of state-of the-art tools to automatically generate and evaluate tests from a model of the software product allows reducing the effort of testing activities while maintaining quality. A major pro...

bbk10.pdf - 237.32 KByte

This paper presents a method for model checking programs for programmable logic controllers (PLCs) using the counterexample-guided abstraction refinement (CEGAR) approach. The technique is tailored to this specific hardware platform by accounting for the cyclic scanning mode that is symptomatic t...

Automation_2012_final.pdf - 474.35 KByte

Der Beitrag befasst sich mit den methodischen Herausforderungen, die durch die Verbreitung der Cyber-Physical Systems (CPS) in der Automatisierungstechnik entstehen, und stellt Lösungsansätze vor. Nach einer Behandlung des Begriffs CPS werden zunächst die allgemeinen, IT-bezogenen Fragestellun...

Barrierenmelder_enav.pdf - 607.3 KByte

Considering mobility of wheelchair users, barriers are of utmost importance. Steps are already an unpassable obstacle and can lead to long detours. To reduce the number of detours occur-ring, barriers should be known to navigation systems, like eNav. In this paper a concept is intro-duced, which ...

eNav Bodenbelag Erkennung.pdf - 366.43 KByte

Surfaces influence comfort as well as energy consumption or necessary strength during wheelchair driving. However, information about surfaces is only scarcely available in OpenStreetMap. To increase the density of this information, smartphone sensors combined with crowdsourcing is used. In this w...

ETFA2014 - Twistturn.pdf - 1.16 MByte

This paper introduces the application of off-theshelf Android tablet computers as real-time capable control devices. We present an IDE to create and execute PLC programs written in Structured Text on a tablet running RTAndroid. This derivative of Android with support for real-time applications en...

sbwk09.pdf - 182.72 KByte

While there are several approaches applying model checking to PLC programs, it is still not used in industry. This is due to the limited applicability of the existing approaches, which all translate PLC programs into the input languages of existing model checkers and thus suffer from certain prob...

final_version.pdf - 214.52 KByte

In dieser Arbeit wird ein Rahmenwerk zur Erkennung und Refactoring von duplizierten Modellfragmenten innerhalb von Matlab/Simulink-Modellen vorgestellt. Dazu wird auf ein Duplikatserkennungsverfahren auf Basis von Layoutinformationen aus Matlab/Simulink-Modellen und auf aus der Literatur bekannte...

Ein Ansatz zum merkmalsbasierten Konsistenzmanagement in der Produktlinienentwicklung.pdf - 3.4 MByte

In dieser Arbeit werden Konzepte pr \250 asentiert, mit denen Verkn \250 upfungen zwischen Elementen, welche w \250 ahrend der Produktlinienentwicklung entstehen, analysiert und im Fall von identifizierten Inkonsistenzen die semiautomatische Ausf \250 uhrung von korrektiven Ma\337nahmen erm \250 ...

Diss - Andre Stollenwerk - modellbasiertes Sicherheitskonzept für die extrakorporale Lungenunterstützung.pdf - 8.87 MByte

Die extrakorporale Lungenunterstützung (ECLA) als intensivmedizinische Behandlung des akuten progressiven Lungenversagens (ARDS) wird heutzutage nur als Ultima-Ratio-Therapie eingesetzt. Dies ist nicht zuletzt der Komplexität der Anwendung und den mit ihr verbundenen Risiken geschuldet. Zur Üb...

WESH_Abstract.pdf - 97.37 KByte

eNav_aal 2016.pdf - 348.31 KByte

Navigation for disabled people in wheelchairs is a huge challenge: stairs and curbstones can already hinder a wheelchair to pass the route. The avail-ability of affordable increasingly powerful smartphones and Internet allows for smart applications, which can help wheelchairs users to find a vali...

Paper_ACMOTE_2012_final.pdf - 289.02 KByte

Paper_Fossgis_2011_final.pdf - 0.95 MByte

Paper_GI_2013_final.pdf - 444.71 KByte

Für Fahrer von elektrisch betriebenen Fahrzeugen ist eine energieeffiziente Nutzung der Akkukapazität von großer Bedeutung. Ein Navigationssystem, das Routen in Abhängigkeit der Steigung, welche einen bedeutenden Einfluss auf den Verbrauch nimmt, berechnet, bietet einen sinnvollen Beitrag zu ...

FS-MCPS2016_final.pdf - 0.96 MByte

Thorough hand disinfection in hospitals is essential to prevent nosocomial infections. Health care workers are trained and instructed on when and how to use hand sanitizers during apprenticeship training and continuing education, but up to now there is no automatic system to give immediate feedba...

bkk11a.pdf - 470.01 KByte

This paper presents an elegant algorithm for existential quantifier elimination using incremental SAT solving. This approach contrasts with existing techniques in that it is based solely on manipulating the SAT instance rather than requiring any reengineering of the SAT solver or needing an auxil...

iupesm18.pdf - 324.91 KByte

This paper compares two fault identification implementations based on a neural network and a model based approach. Our worked example is the detection of gas bubbles in the pump head of a centrifugal blood pump. We focus on algorithms applicable on minimal sensor data with a reasonable implementa...

Ground Surface Pattern Recognition.pdf - 279.58 KByte

We evaluate the feasibility of a low-cost solution to enhance the absolute positioning estimation of a vehicle using the example of a Pedelec (Pedal Electric Cycle). For this purpose, the acceleration sensor and the magnetometer of a smartphone's inertial measurement unit (IMU) are used to record...

rsm11.pdf - 263.49 KByte

Verification of software for embedded systems is crucial for ensuring a product's integrity. Formal approaches like static analysis and model checking are gaining momentum in this context. To make an exhaustive examination of the system's state space tractable in practice, these methods perform a...

AUTOMED_Implementation of ResNet-50 for the Detection of ARDS in Chest X-Rays using transfer-learning.pdf - 284.76 KByte

Acute Respiratory Distress Syndrome is a severe condition with high morbidity and mortality. The current standard for the diagnosis of ARDS was proposed by the Berlin-Definition in 2012. However, studies have shown, that ARDS is often recognized too late or not at all. Smart methods, like machine...

bs12.pdf - 511.13 KByte

Abstract interpretation for proving safety properties summarizes concrete traces into abstract states, thereby trading the ability to distinguish traces for tractability. Given a violation of a safety property, it is thus unclear which trace led to the violation. Moreover, since part of the abstr...

diss_merschen.pdf - 1.94 MByte

Nowadays, functional and safety requirements of vehicles can hardly be met without embedded software since a pure hardware-oriented realisation would be too complex and would result a huge number of electronic control units. Hence, the vehicle's weight would increase leading to a higher fuel cons...

Paper_AGIT_2014_final.pdf - 237.27 KByte

Fahrbahnen, deren Oberfläche aus Kopfsteinpflaster besteht, stellen nicht nur für Fahrer eines Elektrorollstuhls einen unbequemen Verkehrsträger dar. Diese Beobachtung legt nahe, den Einfluss des Straßenbelags auf die Güte einer durch ein Navigationssystem be-rechneten Route zu begutachten. ...

Paper_GI_2014_final.pdf - 521.46 KByte

Eine effiziente Nutzung der Akkukapazität ist für Fahrer von Elektrofahrzeugen erstrebenswert. Die Kalkulation des Energieverbrauchs führt besonders für Nutzer von Elektrorollstühlen zur Steigerung der Mobilität, da der Fahrer einen potentiellen Ausfall des Akkus aufgrund fehlender Energie ...

bns10.pdf - 493.16 KByte

Static analysis is often performed on source code where intervals { possibly the most widely used numeric abstract domain { have successfully been used as a program abstraction for decades. Binary code on microcontroller platforms, however, is different from high-level code in that data is freque...

1-invariants-rp2012.pdf - 317.82 KByte

We propose a new method to derive invariants for LTI systems with uncertain inputs, i.e. systems of the form _x(t) =Ax(t)+Bu(t) with state vectorx(t)2Rnand uncertain inputu(t)2Rmbounded by u(t)2U\022Rmfor allt\0250. Our approach is based on the real canonical form and the resulting invariants are...

MobilTUM_final.pdf - 240.11 KByte

The demographic trends in Germany have led to a continuously growing proportion of elderly people in the population. Population aging is progressing rapidly due to declining fertility, low birth rates and higher life expectancy. As consequence, the number of people with special needs, illness, or...

Paper_AGIT_2011_final.pdf - 352.31 KByte

In den vergangenen Jahren ist die Informationsmenge von frei verfügbaren Weltkarten wie OpenStreetMap enorm gewachsen. Davon profitieren wiederum andere freie Dienste und Applikationen, wie der Open Source Routenplaner OpenRouteService und das mobile Smartphone-Navigationssystem AndNav. Neben ei...

LoadQualityFinalWithoutCopyright.pdf - 136.93 KByte

Nowadays the design goal of embedded systems is shifted from statically defined to a dynamic quality of service at application level. Where embedded systems getting distributed or co-located on platforms, the complexity increases along with their adaptivity and dynamic. And while real-time requir...

bkkn10.pdf - 397.37 KByte

This paper presents a technique for refining the control structure of loops in programs operating over finite bitvectors. This technique is based on abstract interpretation using octagons and affine equalities in order to identify infeasible sequences of loop iterations. Our approach naturally in...

modeTestingFinal.pdf - 287.79 KByte

During the development of PLC software, standards usually require testing to consider certain coverage criteria. Since a manual generation of coverage tests is tedious and error-prone, automatic approaches as concolic testing are highly desirable. Approaches targeting non-reactive software usuall...

ESAO2010Abstract.pdf - 493.4 KByte

mdr_12.pdf - 215.11 KByte

In automotive software development, dependencies among process artefacts, i. e. requirements, implementation and test cases, are often not obvious. This causes time-intensive manual analysis efforts to incorporate changes during software evolution. Therefore, automated tool support is essential t...

root.pdf - 430.38 KByte

In this paper, we present a novel method to supervise several discrete events and continuous processes causing failures in a blood pump. These are potential hazards which regularly cause problems in intensive care routine. We propose an indicator that considers the nonlinear shear thinning flow p...

Arttest_LanguageFormalization.pdf - 580.79 KByte

In this paper, we present Arttest, a tool for functional testing of block diagrams developed with MATLAB/Simulink. We introduce testing concepts for closed-loop tests of automotive software on model and software level, the integration of the concepts into a signal specification language and corre...

Stollenwerk-Modelbasierte Fehlerdiagnose eines Membranoxygenator.pdf - 451 KByte

Modelbasierte Fehlerdiagnose eines Membranoxygenators

Barakat - Modeling and Verification of Network Protocol.pdf - 530.89 KByte

We present a toolkit based on our timed extension of pi-calculus. The calculus is employed as a domain specific language for modeling telecommunication protocols with real-time properties. This model can be simulated, visualized, debugged and transformed for model-checking using UPPAAL. This pape...

Paper_AGIT_2013_final.pdf - 724.55 KByte

Um eine Route zu berechnen, greifen die meisten Navigationssysteme auf zweidimensiona-les Kartenmaterial zurück. In der Regel hat der Benutzer vor der Berechnung die Wahl, ob er die kürzeste oder schnellste Route berechnen lassen möchte. Navigationssysteme ver-wenden für die Routenberechnung ...

mobilTUM2017_final.pdf - 1.1 MByte

There is a wide variety of navigation systems available on the market. Most of these systems offer the possibility to choose between different transport vehicles and routing options. However, these systems hardly offer the possibility for accessible routing, which is optimized especially for user...

Agit 2017Final.pdf - 557.52 KByte

The type of navigation-systems available nowadays varies a lot. Although a lot of these systems provide the user with a choice between several means of transportations and calculation types, the transportation type, for example bus or train, remains static during route guidance. This induces the ...

benchmarks_platoon.pdf - 417.01 KByte

practical benchmark for testing analysis and veri?cation methods for con-tinuous as well as for hybrid systems is suggested. It consists of a platoon ofcontrolled vehicles. The vehicles exchange information via a communication net-work that is subject to failure of single nodes or a complete loss...

submission.pdf - 632.37 KByte

The Android platform is an open source operating system for mobile devices developed by the Open Handset Alliance. Due to its usability and rich set of functionalities, Android is an attractive platform for both, developers and end-users. RTAndroid is a modified version of the Android 2.2 platfor...

bbgk10.pdf - 298.59 KByte

Path reduction is a well-known technique to alleviate the state-explosion problem incurred by explicit-state model checking, its key idea being to store states only at predetermined breaking points. This paper presents an adaptation of this technique which detects breaking points on-the-fly durin...

imav2013-easychair.pdf - 377.71 KByte

Onboard image processing for unmanned aerial vehicles (UAVs) has become a popular method in the recent decades and the number of available hardware solutions has increased. Growing processing power and reduced weight and size of the embedded systems facilitate more computational power onboard the...

rbh11.pdf - 420.92 KByte

This paper presents a method for runtime verification of microcontroller binary code based on past time linear temporal logic ( ptLTL ). We show how to implement a framework that, owing to a dedicated hardware unit, does not require code instrumentation, thus, allowing the program under scrutiny ...

Walter - Patient oriented closed loop control of extracorporeal lung assist.pdf - 104.92 KByte

In cases of severe lung failure, long term extracorporeal membrane oxygenation has become a relevant treatment option in the ICU. With the availability of small and long term stable oxygenation circuits and dedicated drive units, it is now possible to apply ECLA in the intensive care unit on a ro...

1569434415.pdf - 351.74 KByte

Ein Hauptproblem der Extrakorporalen Membranoxygenierung (ECMO) ist, dass durch die intermittierende Überwachung des Patienten keine kontinuierliche Anwendungskontrolle, wie bei der Herz-Lungen-Maschine im Operationssaal, gegeben ist. Damit steigt die Gefahr von Komplikationen und eine optimale ...

rb11.pdf - 467.84 KByte

This paper presents a SAT-based method for control flow graph reconstruction from executable code. The key idea of the technique is to express the semantics of each basic block in a program using Boolean logic, followed by inferring preand postconditions for each block through interleaved forward...

main.pdf - 699.59 KByte

In this paper, we present a predicate abstraction for programs for programmable logic controllers (PLCs) so as to allow for model checking safety related properties. Our contribution is twofold: First, we give a formalization of PLC programs in first order logic, which is then used to automatical...

jtres2014.pdf - 0.86 MByte

Several approaches to extend the original Android implementation with real-time capabilities were presented in the last few years. Most of the research was limited to fundamental issues like real-time scheduling and non-blocking memory management. This paper demonstrates the weak predictability o...

jtres2015-binder.pdf - 1.58 MByte

Different approaches for improving process scheduling, memory management and generic message passing have been introduced to Android in the past, in order to extend it with support for real-time applications. One of Android's most important security features is sandboxing and strict isolation of ...

Biallas - PtrTracker Pragmatic pointer analysis.pdf - 186.5 KByte

Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, bot...

atp_2015JK.pdf - 488.72 KByte

This work presents a pulsatile control of a commercial rotary blood pump with a prototypic control box. It is part of the project ECLA-Vent, which focuses on the optimization and safety of ARDS treatment. The task of the rotary blood pump is the generation of a bloodflow for extracorporeal lung a...

Automation2015_JK.pdf - 429.71 KByte

Diese Arbeit stellt die pulsatile Ansteuerung einer handelsüblichen Blutpumpe über eine prototypische Steuerung vor. Die Arbeit ist Teil des Projektes ECLA-VENT, in dem die Verbesserung der Effizienz und Sicherheit der ARDS-Behandlung untersucht wird. Aufgabe der betrachteten Diagonalblutpumpe ...

bkk10.pdf - 422.85 KByte

Bitwise instructions, loops and indirect data access pose difficult challenges to the verification of microcontroller programs. In particular, it is necessary to show that an indirect write does not mutate registers, which are indirectly addressable. To prove this property, among others, this pap...

bks12b.pdf - 278.63 KByte

This paper presents an analysis to infer range and value-set information for programs operating on programmable logic controllers. Given a program, the algorithm gathers all possible values of all variables for all possible program executions using abstract simulation. The set of these values con...

MED13_0307_FI-1.pdf - 345.89 KByte

In this work we address the management of a pla-toon of vehicles passing an intersection. In such a sit-uation we have to decide under which conditions theplatoon can pass the intersection in its entirety whileavoiding collisions. If this cannot be assured, the pla-toon should be stopped at the i...

submittedPrerelease.pdf - 477.96 KByte

Reachability analysis is one major approach for safety verification of continuous and hybrid dynamical systems. In this paper we present a new approach to calculate the reachable states of linear systems with uncertain inputs under the assumption that the inputs are stepwise constant. The origina...

snbb09.pdf - 502.8 KByte

Interrupts play an important role in embedded software. Unfortunately, they aggravate the state-explosion problem that model checking is suffering from. Therefore, we propose a new abstraction technique based on partial order reduction that minimizes the number of locations where interrupt handle...

LWW+09.pdf - 256.26 KByte

In schweren Fällen des akuten Lungenversagens kann der lebensnotwendige Gasaustausch mitunter nur noch mithilfe der Extrakorporalen Oxygenierung gewährleistet werden. Einer breiten Anwendung dieser Therapieform steht jedoch derzeit der enorme personal- und gerätetechnische Aufwand entgegen, da...

BMT.2009.pdf - 262.1 KByte

Die Anwendung extrakorporaler Lungenunterstützungsverfahren auf der Intensivstation ist bei schwerstem akutem Lungenversagen (ARDS) mit fortbestehender Hypoxie eine etablierte Therapie, obwohl der Einsatz von Regelungs- und Sicherheitskonzepten bisher höchstens ansatzweise realisiert ist. Ziel ...

GNK - Reusability and Modularity of Safety Specifications for Supervisory Control.pdf - 715.28 KByte

Supervisory control theory, introduced by Ramadge and Wonham, provides a method to synthesize a supervisor that keeps a discrete-event system model inside a previously specified safe state space. In order to apply this technique on physical plants, the user has to provide a model representation o...

AGIT2015final.pdf - 638.99 KByte

Navigation systems are able to determine the shortest, fastest and most energy efficient route. Whenever an area is encountered on a route it will be driven around. A realistic scenario would be a pedestrian going from point A to B crossing a market place or a parking lot. A common navigation sys...

AGIT2015.pdf - 712.63 KByte

Navigationssysteme und Routenplaner können problemlos über Graphen mit Knoten und Kanten die kürzeste, schnellste oder energieeffizienteste Route finden. In dem Fall, dass sich auf der Route zum Ziel ein Polygon befindet, wird dieses umfahren. In einem realen Beispiel sieht dies wie folgt aus:...

ESAO2011Abstract.pdf - 108.87 KByte

During ECMO, about 12 % of all complications are caused by the blood pump or by air in the circuit. In addition, hemolysis, which bases on activation within the blood pump, causes complications during 7 % of all ECMO treatments. Since ECMO is still an ultima-ratio therapy we want to improve this ...

MCPS15_JK.pdf - 445.98 KByte

This paper presents a method to include safety system conflicts into a fault tree analysis (FTA) with semantic extensions of fault events. The verification of the incoherent fault tree is done with an SMT-Solver. As an example a networked setup of medical devices for extracorporeal lung assist wa...

4-ifac2165_reviewed.pdf - 463.95 KByte

bbk11.pdf - 182.97 KByte

This paper studies the application of counterexample-guided abstraction refinement to programs written in Instruction List. More importantly, it presents an approach for automatic abstraction refinement based on SAT solving. This technique is based on an encoding of the semantics of Instruction L...

ScenarioBasedEvaluationofAbstractStateMachines.pdf - 84 KByte

In this paper we suggest a scenario-based approach to analyzing non-functional properties of ASM ground models. It is based on well-founded evaluation methods from the software architecture field and enables a designer to reason about the quality features of his model, like e. g. maintainability ...

Alrifaee2017b.pdf - 525.17 KByte

This paper presents a dynamic collision avoidance controller of a connected vehicle group using Model Predictive Control (MPC). The vehicles should follow a predefined reference trajectory while simultaneously avoiding collisions on this trajectory. MPC pursues the tracking of the reference traje...

EKA2010.pdf - 64.25 KByte

Durch stetig verbesserte Sensorik und wachsende Rechenkapazität moderner Prozessoren ist es möglich geworden, auch komplexe intensivmedizinische Szenarien zu automatisieren. Die vielschichtigen und oftmals hochgradig nichtlinearen Problemstellungen in der Medizintechnik sorgten in Verbindung mi...

Stollenwerk - Smart Data Provisioning for Model-Based Generated Code - HCMDSS.pdf - 398.04 KByte

Software modeling tools likeMATLAB/Simulink found their way into contemporary embedded software engineering. These tools relieve the software engineer from implementing constructs like a controller or complex models of physical behavior manually in e.g. C code. Thus, one major field of applicatio...

SKW+14.pdf - 451.88 KByte

This paper presents a novel method to predict the occlusion of a withdrawing cannula during extracorporeal circulation due to a networked intensive care setup. During in-vivo experiments we were able to detect the cannula suction up to 90 seconds prior to the collapse of extracorporeal blood flow...

PID4333625_final.pdf - 163.69 KByte

ASE_2015.pdf - 348.75 KByte

In this paper we present a static value range analysis of signals within function block diagrams developed with Matlab/Simulink. We analyse signals with respect to their data type and compute an approximation of the possible value range of each signal represented by a set of intervals. In additio...

StructuralConcolicTesting_final.x5rPA.pdf - 393.32 KByte

Graphical programming languages allow for well structured software and support comprehensibility and maintainability of the code. As for industrial applications,

StructuralConcolicTesting_final.pdf - 403.93 KByte

Graphical programming languages allow for well structured software and support comprehensibility and maintainability of the code. As for industrial applications,

ACPS2011Abstract.pdf - 93.75 KByte

A major challenge in the design and operation of cyber-physical systems is the ability to cope with changes. Usually, this is understood as the need for systems to adapt to changing conditions and constellations in the (physical and infrastructural) environment of a system. However, the challenge...

Dissertation_Final_Druck.pdf - 5.37 MByte

Creating software for embedded systems requires rigid quality measures. The reason for this is that errors in the software may have very expensive or even disastrous consequences. This gives rise to the use of formal methods for software verification, such as model checking, theorem proving, and ...

Goebe Timmermanns Ney Kowalewski - Synthesis Tool for Automation Controller Supervision.pdf - 805.6 KByte

The supervisory control theory is a conceptual framework to keep a discrete-event system in a desired state space by disabling controllable events. This paper introduces a new software tool to create supervisors for actual, physical plants in terms of a PLC code implementation. It points out the ...

Abstract GTÜM 2017.pdf - 80.39 KByte

Die meisten modernen Tauchcomputer berücksichtigen nur den Zusammenhang zwischen Tauchzeit und -tiefe für die Dekompressionsberechnung. In der Literatur sind jedoch weitere Einflussfaktoren wie z.B. Temperatur oder Anstrengung des Tauchers hinreichend beschrieben. Dies wirft unweigerlich die Fr...

rbh_10.pdf - 286.6 KByte

This paper describes a framework for test-case generation for microcontroller binary programs using abstract interpretation techniques. The key idea of our approach is to derive program invariants a priori, and then use backward analysis to obtain test vectors that are executed on the target micr...

RWTH-Fak1.sty - 3.92 KByte

Erstellt Titelblätter für die Prüfungsversion und die Abgebeversion der Dissertation gemäß Vorgabe der Fakultät für Mathematik, Informatik und Naturwissenschaften der RWTH Aachen. Nutzung: \usepackage[option]{RWTH-Fak1} Aktuelle Optionen sind: pruefung: Für die Abzugebende Prüdung...

Paper_IPIN_2014_final.pdf - 245.96 KByte

As indoor navigation matures, advanced navigation services for users with special needs become possible. We argue for the development of Indoor Traffic Report systems. While a typical user might only be slightly inconvenienced, when an elevator is out of order or parts of a building are being ren...

bk11.pdf - 399.83 KByte

Recently it has been shown how transfer functions for linear template constraints can be derived for bit-vector programs by operating over propositional Boolean formulae. The drawback of this method is that it relies on existential quantifier elimination, which induces a computational bottleneck....

BVM2017_final.pdf - 1.08 MByte

Bei der Verbreitung und Übertragung von Infektionen im Krankenhaus sind die Hände ein zentraler Infektionsweg. Die korrekt ausgeführte hygienische Händedesinfektion ist deshalb entscheidend, um nosokomiale Infektionen zu verhindern. Unser Prototyp, aus voran gegangenen Arbeiten, bewertet die ...

SKW09.pdf - 462.94 KByte

Speicherprogrammierbare Steuerungen werden häufig in sicherheitskritischen Systemen verwendet. Einfaches Testen dieser Systeme reicht häufig nicht aus, da bestimmte Fehler durch Testen alleine schwer zu finden sind. Model-Checking ist eine formale Methode, die zeigen kann, dass ein System seine...

pmt_10.pdf - 571.69 KByte

When applying model-based techniques to the engineering of embedded application software, a typical challenge is the complexity of dependencies between application elements. In many situations, e.g., during rollout of products or in the evolution of product lines, the understanding of these depen...

HCI_2017.pdf - 2.5 MByte

Mobility is a fast developing, technological and simultaneously human field of research. V2X-technology is one major contributor that will influence the behavior, efficiency and safety of traffic participants. To include all participating members of traffic, we developed a V2X-smartphone applicat...