A benchmark suite for hybrid systems reachability analysis

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...

A Comparison of Dual-Core Approaches for Safety-Critical Automotive Applications

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...

A Dynamic Study on the Hemolytic Effect of Negative Pressure on Blood

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 model-based safety concept for a rotary blood pump

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...

A Modular, Robust and Open Source Microcontroller Platform for Broad Educational Usage

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...

A Physiological Model for Extracorporeal Oxygenation Controller Design

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...

A Real-time Extension to the Android Platform

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...

A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification

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...

Abstract Interpretation of MATLAB Code with Interval Sets

FMICS_2016.pdf - 379.21 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 ...

An Approach for Using Mobile Devices In Industrial Safety-Critical Embedded Systems

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...

An Architecture with Integrated Image Processing for Autonomous Micro Aerial Vehicles

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...

An Integrated and Vision Aided GPS/INS Navigation System for Ultra-low-cost MAVs

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...

An Undergraduate Embedded Software Laboratory for the Masses

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...

Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations

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...

Analyzing the Restart Behavior of Industrial Control Applications

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...

Application of Static Analyses for State Space Reduction to Microcontroller Binary Code

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...

Approximate Quantifier Elimination for Propositional Boolean Formulae

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,...

Arcade.PLC: A Verification Platform for Programmable Logic Controllers

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...

Automated Test-Trace Inspection for Microcontroller Binary Code

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...

Automatic Abstraction for Bit-Vectors using Decision Procedures

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...

Automatic Abstraction for Intervals using Boolean Formulae

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...

Automatic Control of veno-venous Extracorporeal Lung Assist

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...

Automatic Error Cause Localization of Faulty PLC Programs

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...

Automatic Invariant Checking for discrete Block Diagrams using Lyapunov Functions with Sat Modulo Theory Solvers

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...

Automatic Test Case Generation for PLC Programs using Coverage Metrics

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...

Automatically Deriving Symbolic Invariants for PLC Programs Written in IL

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...

Automation of long term extracorporeal oxygenation systems

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...

Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung

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...

Automatisierung der extrakorporalen Membranoxygenierung

wartzek_automed2009_Automatisierung der extrakorporalen Membranoxygenierung.pdf - 217.85 KByte

Automatisierung und Fehlerdiagnose bei der extrakorporalen Membranoxygenierung

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...

Closed loop physiological ECMO control

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...

Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams

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 ...

Comparison of Reachability Methods for Uncertain LinearTime-Invariant Systems

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...

Coping with Complexity of Testing Models for Real-Time Embedded Systems

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...

Counterexample-Guided Abstraction Refinement for PLCs

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...

Cyber-Physical Systems –- eine Herausforderung für die Automatisierungstechnik?

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...

Das Barrierenerkennungssystem von eNav

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 ...

Der Bodenbelag-Detektor des eNav-Systems

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...

Development and Execution of PLC Programs on Real-Time Capable Mobile Devices

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...

Direct Model Checking of PLC Programs in IL

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...

Duplikatserkennung und Refactoring in Matlab/Simulink-Modellen

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

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 ...

Ein modellbasiertes Sicherheitskonzept für die extrakorporale Lungenunterstützung

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...

eNav A Suitable Navigation System for the Disabled

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...

Entwicklung eines Mobilen Navigationssystems für Elektrofahrzeuge

Paper_Fossgis_2011_final.pdf - 0.95 MByte

Entwicklung und Evaluation eines Navigationssystems für Elektrorollstühle

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 ...

Existential Quantification as Incremental SAT

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...

Hardware Support for Efficient Testing of Embedded Software

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...

Inferring Definite Counterexamples Through Under-Approximation

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...

Integration und Analyse von Artefakten in der modellbasierten Entwicklung eingebetteter Software

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...

Integration von Bodenbelagsinformationen zum energieeffizienten Routen von Elektrorollstühlen

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. ...

Integration von Informationen über die Bodenbeschaffenheit in das eNav-System

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 ...

Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software

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...

Invariants for LTI Systems with Uncertain Input

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...

Investigation of barrier-free environment based on smart band technology

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...

Konzept eines mobilen OSM-Navigationssystems für Elektrofahrzeuge

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...

Load and Quality Cooperation for Distributed Embedded Systems Using Different Modes of Operation

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...

Loop Refinement Using Octagons and Satisfiability

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...

Model-Based Analysis of Design Artefacts Applying an Annotation Concept

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...

Model-based supervision of a blood pump

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...

Modelbasierte Fehlerdiagnose eines Membranoxygenators

Stollenwerk-Modelbasierte Fehlerdiagnose eines Membranoxygenator.pdf - 451 KByte

Modelbasierte Fehlerdiagnose eines Membranoxygenators

Modeling and Verification of Network Protocol Specs using Timed Pi-Calculus

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...

Modifikation des A*-Algorithmus für energieeffizientes 3D-Routing

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 ...

Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools

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...

Non-Blocking Garbage Collection for Real-Time Android

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...

On-The-Fly Path Reduction

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...

Optimizing Image Processing on OMAP3 with driver-level frame buffering and color space conversion

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...

Past Time LTL Runtime Verification for Microcontroller Binary Code

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 ...

Patient oriented closed loop control of extracorporeal lung assist

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...

Patientenorientierte Automatisierung der Therapie mit der Extrakorporalen Membranoxygenierung (ECMO)

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 ...

Precise Control Flow Reconstruction Using Boolean Logic

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...

Predicate Abstraction for Programmable Logic Controllers

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...

Predictable Broadcasting of Parallel Intents in Real-Time Android

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...

Priority Inheritance during Remote Procedure Calls in Real-Time Android using Extended Binder Framework

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 ...

PtrTracker: Pragmatic Pointer Analysis

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...

Pulsatile Ansteuerung einer Diagonalblutpumpe

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...

Pulsatile Ansteuerung einer Diagonalblutpumpe

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 ...

Range Analysis of Microcontroller Code using Bit-Level Congruences

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...

Range and Value-Set Analysis for Programmable Logic Controllers

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...

Reachability Analysis for Managing Platoons at Intersections

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...

Reachability Analysis of Linear Systems with Stepwise Constant Inputs

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...

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

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...

Regelung des Gasaustauschs für die extrakorporale Oxygenierung

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...

Regelungs- und Sicherheitskonzepte für extrakorporale Systeme zur Lungenunterstützung

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 ...

Reusability and Modularity of Safety Specifications for Supervisory Control

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...

Routing über Flächen mit SpiderWebGraph

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...

Routing über Flächen mit SpiderWebGraph

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:...

Safety Aware Pump-Control for a Rotary ECMO Blood Pump

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 ...

Safety Conflict Analysis in Medical Cyber-Physical Systems using an SMT-Solver

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...

SAT-Based Abstraction Refinement for Programmable Logic Controllers

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...

Scenario-Based Evaluation of Abstract State Machines

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 ...

Sicherheitskonzept für eine intensivmedizinische Anwendung am Beispiel der ECMO

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...

Smart Data Provisioning for Model-Based Generated Code in an Intensive Care Application

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...

Software-based Prediction of Cannula Occlusion during Extracorporeal Blood Circulation through Networked Medical Data

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...

Static Value Range Analysis for Matlab/Simulink-Models

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...

Supporting evolving requirements in CPS by abstraction layers in the architecture

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...

Synthesis of State Space Generators for Model Checking Microcontroller Code

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 ...

Synthesis Tool for Automation Controller Supervision

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 ...

Test-Case Generation for Embedded Binary Code Using Abstract Interpretation

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...

Titelblatt für Promotionen gemäß Promotionsordnung

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...

Towards an Indoor Traffic Report

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...

Transfer Function Synthesis without Quantifier Elimination

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....

Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking

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...

View-Supported Rollout and Evolution of Model-Based ECU Applications

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...