Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Departmental Papers (CIS)

Discipline
Keyword
Publication Year

Articles 1 - 30 of 112

Full-Text Articles in Computer Engineering

Holistic Resource Allocation For Multicore Real-Time Systems, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, Insup Lee Apr 2019

Holistic Resource Allocation For Multicore Real-Time Systems, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, Insup Lee

Departmental Papers (CIS)

This paper presents CaM, a holistic cache and memory bandwidth resource allocation strategy for multicore real-time systems. CaM is designed for partitioned scheduling, where tasks are mapped onto cores, and the shared cache and memory bandwidth resources are partitioned among cores to reduce resource interferences due to concurrent accesses. Based on our extension of LITMUSRT with Intel’s Cache Allocation Technology and MemGuard, we present an experimental evaluation of the relationship between the allocation of cache and memory bandwidth resources and a task’s WCET. Our resource allocation strategy exploits this relationship to map tasks onto cores, and to ...


Reducing Pulse Oximetry False Alarms Without Missing Life-Threatening Events, Hung Nguyen, Sooyong Jang, Radoslav Ivanov, Christopher P. Bonafide, James Weimer, Insup Lee Sep 2018

Reducing Pulse Oximetry False Alarms Without Missing Life-Threatening Events, Hung Nguyen, Sooyong Jang, Radoslav Ivanov, Christopher P. Bonafide, James Weimer, Insup Lee

Departmental Papers (CIS)

Alarm fatigue has been increasingly recognized as one of the most significant problems in the hospital environment. One of the major causes is the excessive number of false physiologic monitor alarms. An underlying problem is the inefficient traditional threshold alarm system for physiologic parameters such as low blood oxygen saturation (SpO2). In this paper, we propose a robust classification procedure based on the AdaBoost algorithm with reject option that can identify and silence false SpO2 alarms, while ensuring zero misclassified clinically significant alarms. Alarms and vital signs related to SpO2 such as heart rate and pulse rate ...


Bandwidth Optimal Data/Service Delivery For Connected Vehicles Via Edges, Deepak Gangadharan, Oleg Sokolsky, Insup Lee, Baekgyu Kim, Chung-Wei Lin, Shinichi Shiraishi Jul 2018

Bandwidth Optimal Data/Service Delivery For Connected Vehicles Via Edges, Deepak Gangadharan, Oleg Sokolsky, Insup Lee, Baekgyu Kim, Chung-Wei Lin, Shinichi Shiraishi

Departmental Papers (CIS)

The paradigm of connected vehicles is fast gaining lot of attraction in the automotive industry. Recently, a lot of technological innovation has been pushed through to realize this paradigm using vehicle to cloud (V2C), infrastructure (V2I) and vehicle (V2V) communications. This has also opened the doors for efficient delivery of data/service to the vehicles via edge devices that are closer to the vehicles. In this work, we propose an optimization framework that can be used to deliver data/service to the connected vehicles such that a bandwidth cost objective is optimized. For the first time, we also integrate a ...


Data Freshness Over-Engineering: Formulation And Results, Dagaen Golomb, Deepak Gangadharan, Sanjian Chen, Oleg Sokolsky, Insup Lee May 2018

Data Freshness Over-Engineering: Formulation And Results, Dagaen Golomb, Deepak Gangadharan, Sanjian Chen, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

In many application scenarios, data consumed by real-time tasks are required to meet a maximum age, or freshness, guarantee. In this paper, we consider the end-to-end freshness constraint of data that is passed along a chain of tasks in a uniprocessor setting. We do so with few assumptions regarding the scheduling algorithm used. We present a method for selecting the periods of tasks in chains of length two and three such that the end-to-end freshness requirement is satisfied, and then extend our method to arbitrary chains. We perform evaluations of both methods using parameters from an embedded benchmark suite (E3S ...


Generic Formal Framework For Compositional Analysis Of Hierarchical Scheduling Systems, Jalil Boudjadar, Jin Hyun Kim, Linh Thi Xuan Phan, Insup Lee, Kim G. Larsen, Ulrik Nyman May 2018

Generic Formal Framework For Compositional Analysis Of Hierarchical Scheduling Systems, Jalil Boudjadar, Jin Hyun Kim, Linh Thi Xuan Phan, Insup Lee, Kim G. Larsen, Ulrik Nyman

Departmental Papers (CIS)

We present a compositional framework for the specification and analysis of hierarchical scheduling systems (HSS). Firstly we provide a generic formal model, which can be used to describe any type of scheduling system. The concept of Job automata is introduced in order to model job instantiation patterns. We model the interaction between different levels in the hierarchy through the use of state-based resource models. Our notion of resource model is general enough to capture multi-core architectures, preemptiveness and non-determinism.


Openice-Lite: Towards A Connectivity Platform For The Internet Of Medical Things, Radoslav Ivanov, Hung Nguyen, James Weimer, Oleg Sokolsky, Insup Lee May 2018

Openice-Lite: Towards A Connectivity Platform For The Internet Of Medical Things, Radoslav Ivanov, Hung Nguyen, James Weimer, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

The Internet of Medical Things (IoMT) is poised to revolutionize medicine. However, medical device communication, coordination, and interoperability present challenges for IoMT applications due to safety, security, and privacy concerns. These challenges can be addressed by developing an open platform for IoMT that can provide guarantees on safety, security and privacy. As a first step, we introduce OpenICE-lite, a middleware for medical device interoperability that also provides security guarantees and allows other IoMT applications to view/analyze the data in real time. We describe two applications that currently utilize OpenICE-lite, namely (i) a critical pulmonary shunt predictor for infants during ...


Joint Rate Control And Demand Balancing For Electric Vehicle Charging, Fanxin Kong, Xue Liu, Insup Lee Apr 2018

Joint Rate Control And Demand Balancing For Electric Vehicle Charging, Fanxin Kong, Xue Liu, Insup Lee

Departmental Papers (CIS)

Charging stations have become indispensable infrastructure to support the rapid proliferation of electric vehicles (EVs). The operational scheme of charging stations is crucial to satisfy the stability of the power grid and the quality of service (QoS) to EV users. Most existing schemes target either of the two major operations: charging rate control and demand balancing. This partial focus overlooks the coupling relation between the two operations and thus causes the degradation on the grid stability or customer QoS. A thoughtful scheme should manage both operations together. A big challenge to design such a scheme is the aggregated uncertainty caused ...


Parameter Invariant Monitoring For Signal Temporal Logic, Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, Insup Lee Apr 2018

Parameter Invariant Monitoring For Signal Temporal Logic, Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

Signal Temporal Logic (STL) is a prominent specification formalism for real-time systems, and monitoring these specifications, specially when (for different reasons such as learning) behavior of systems can change over time, is quite important. There are three main challenges in this area: (1) full observation of system state is not possible due to noise or nuisance parameters, (2) the whole execution is not available during the monitoring, and (3) computational complexity of monitoring continuous time signals is very high. Although, each of these challenges has been addressed by different works, to the best of our knowledge, no one has addressed ...


Cyber-Physical System Checkpointing And Recovery, Fanxin Kong, Meng Xu, James Weimer, Oleg Sokolsky, Insup Lee Apr 2018

Cyber-Physical System Checkpointing And Recovery, Fanxin Kong, Meng Xu, James Weimer, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

Transitioning to more open architectures has been making Cyber-Physical Systems (CPS) vulnerable to malicious attacks that are beyond the conventional cyber attacks. This paper studies attack-resilience enhancement for a system under emerging attacks in the environment of the controller. An effective way to address this problem is to make system state estimation accurate enough for control regardless of the compromised components. This work follows this way and develops a procedure named CPS checkpointing and recovery, which leverages historical data to recover failed system states. Specially, we first propose a new concept of physical-state recovery. The essential operation is defined as ...


Logsafe: Secure And Scalable Data Logger For Iot Devices, Hung Nguyen, Radoslav Ivanov, Linh T.X. Phan, Oleg Sokolsky, James Weimer, Insup Lee Apr 2018

Logsafe: Secure And Scalable Data Logger For Iot Devices, Hung Nguyen, Radoslav Ivanov, Linh T.X. Phan, Oleg Sokolsky, James Weimer, Insup Lee

Departmental Papers (CIS)

As devices in the Internet of Things (IoT) increase in number and integrate with everyday lives, large amounts of personal information will be generated. With multiple discovered vulnerabilities in current IoT networks, a malicious attacker might be able to get access to and misuse this personal data. Thus, a logger that stores this information securely would make it possible to perform forensic analysis in case of such attacks that target valuable data. In this paper, we propose LogSafe, a scalable, fault-tolerant logger that leverages the use of Intel Software Guard Extensions (SGX) to store logs from IoT devices efficiently and ...


Context-Aware Detection In Medical Cyber-Physical Systems, Radoslav Ivanov, James Weimer, Insup Lee Apr 2018

Context-Aware Detection In Medical Cyber-Physical Systems, Radoslav Ivanov, James Weimer, Insup Lee

Departmental Papers (CIS)

This paper considers the problem of incorporating context in medical cyber-physical systems (MCPS) applications for the purpose of improving the performance of MCPS detectors. In particular, in many applications additional data could be used to conclude that actual measurements might be noisy or wrong (e.g., machine settings might indicate that the machine is improperly attached to the patient); we call such data context. The first contribution of this work is the formal definition of context, namely additional information whose presence is associated with a change in the measurement model (e.g., higher variance). Given this formulation, we developed the ...


Multi-Mode Virtualization For Soft Real-Time Systems, Haoran Li, Meng Xu, Chong Li, Chenyang Lu, Christopher Gill, Linh T.X. Phan, Insup Lee, Oleg Sokolsky Apr 2018

Multi-Mode Virtualization For Soft Real-Time Systems, Haoran Li, Meng Xu, Chong Li, Chenyang Lu, Christopher Gill, Linh T.X. Phan, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

Real-time virtualization is an emerging technology for embedded systems integration and latency-sensitive cloud applications. Earlier real-time virtualization platforms require offline configuration of the scheduling parameters of virtual machines (VMs) based on their worst-case workloads, but this static approach results in pessimistic resource allocation when the workloads in the VMs change dynamically. Here, we present Multi-Mode-Xen (M2-Xen), a real-time virtualization platform for dynamic real-time systems where VMs can operate in modes with different CPU resource requirements at run-time. M2-Xen has three salient capabilities: (1) dynamic allocation of CPU resources among VMs in response to their mode changes, (2) overload avoidance at ...


Parameter-Invariant Monitor Design For Cyber Physical Systems, James Weimer, Radoslav Ivanov, Sanjian Chen, Alexander Roederer, Oleg Sokolsky, Insup Lee Jan 2018

Parameter-Invariant Monitor Design For Cyber Physical Systems, James Weimer, Radoslav Ivanov, Sanjian Chen, Alexander Roederer, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

The tight interaction between information technology and the physical world inherent in Cyber-Physical Systems (CPS) can challenge traditional approaches for monitoring safety and security. Data collected for robust CPS monitoring is often sparse and may lack rich training data describing critical events/attacks. Moreover, CPS often operate in diverse environments that can have significant inter/intra-system variability. Furthermore, CPS monitors that are not robust to data sparsity and inter/intra-system variability may result in inconsistent performance and may not be trusted for monitoring safety and security. Towards overcoming these challenges, this paper presents recent work on the design of parameter-invariant ...


Mc-Adapt: Adaptive Task Dropping In Mixed-Criticality Scheduling, Jaewoo Lee, Hoon Sung Chwa, Linh T.X. Phan, Insik Shin, Insup Lee Oct 2017

Mc-Adapt: Adaptive Task Dropping In Mixed-Criticality Scheduling, Jaewoo Lee, Hoon Sung Chwa, Linh T.X. Phan, Insik Shin, Insup Lee

Departmental Papers (CIS)

Recent embedded systems are becoming integrated systems with components of different criticality. To tackle this, mixed-criticality systems aim to provide different levels of timing assurance to components of different criticality levels while achieving efficient resource utilization. Many approaches have been proposed to execute more lower-criticality tasks without affecting the timeliness of higher-criticality tasks. Those previous approaches however have at least one of the two limitations; i) they penalize all lower-criticality tasks at once upon a certain situation, or ii) they make the decision how to penalize lowercriticality tasks at design time. As a consequence, they underutilize resources by imposing an ...


Monitoring Time Intervals, Teng Zhang, John Wiegley, Insup Lee, Oleg Sokolsky Sep 2017

Monitoring Time Intervals, Teng Zhang, John Wiegley, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

Run-time checking of timed properties requires to monitor events occurring within a specified time interval. In a distributed setting, working with intervals is complicated due to uncertainties about network delays and clock synchronization. Determining that an interval can be closed - i.e., that all events occurring within the interval have been observed - cannot be done without a delay. In this paper, we consider how an appropriate delay can be determined based on parameters of a monitoring setup, such as network delay, clock skew and clock rate. We then propose a generic scheme for monitoring time intervals, parameterized by the detection ...


Process Algebraic Approach To The Schedulability Analysis And Workload Abstraction Of Hierarchical Real-Time Systems, Junkil Park, Insup Lee, Oleg Sokolsky, Dae Yon Hwang, Sojin Ahn, Jin-Young Choi, Inhye Kang Jul 2017

Process Algebraic Approach To The Schedulability Analysis And Workload Abstraction Of Hierarchical Real-Time Systems, Junkil Park, Insup Lee, Oleg Sokolsky, Dae Yon Hwang, Sojin Ahn, Jin-Young Choi, Inhye Kang

Departmental Papers (CIS)

Real-time embedded systems have increased in complexity. As microprocessors become more powerful, the software complexity of real-time embedded systems has increased steadily. The requirements for increased functionality and adaptability make the development of real-time embedded software complex and error-prone. Component-based design has been widely accepted as a compositional approach to facilitate the design of complex systems. It provides a means for decomposing a complex system into simpler subsystems and composing the subsystems in a hierarchical manner. A system composed of real-time subsystems with hierarchy is called a hierarchical real-time system

This paper describes a process algebraic approach to schedulability analysis ...


Security Of Cyber-Physical Systems In The Presence Of Transient Sensor Faults, Junkil Park, Radoslav Ivanov, James Weimer, Miroslav Pajic, Sang Hyuk Son, Insup Lee Jul 2017

Security Of Cyber-Physical Systems In The Presence Of Transient Sensor Faults, Junkil Park, Radoslav Ivanov, James Weimer, Miroslav Pajic, Sang Hyuk Son, Insup Lee

Departmental Papers (CIS)

This paper is concerned with the security of modern Cyber-Physical Systems in the presence of transient sensor faults. We consider a system with multiple sensors measuring the same physical variable, where each sensor provides an interval with all possible values of the true state. We note that some sensors might output faulty readings and others may be controlled by a malicious attacker. Different from previous works, in this paper we aim to distinguish between faults and attacks and develop an attack detection algorithm for the latter only. To do this, we note that there are two kinds of faults – transient ...


Extensible Energy Planning Framework For Preemptive Tasks, Jin Hyun Kim, Deepak Gangadharan, Oleg Sokolsky, Axel Legay, Insup Lee May 2017

Extensible Energy Planning Framework For Preemptive Tasks, Jin Hyun Kim, Deepak Gangadharan, Oleg Sokolsky, Axel Legay, Insup Lee

Departmental Papers (CIS)

Cyber-physical systems (CSPs) are demanding energy-efficient design not only of hardware (HW), but also of software (SW). Dynamic Voltage and and Frequency Scaling (DVFS) and Dynamic Power Manage (DPM) are most popular techniques to improve the energy efficiency. However, contemporary complicated HW and SW designs requires more elaborate and sophisticated energy management and efficiency evaluation techniques. This paper is concerned about energy supply planning for real-time scheduling systems (units) of which tasks need to meet deadlines. This paper presents a modelbased compositional energy planning technique that computes a minimal ratio of processor frequency that preserves schedulability of independent and preemptive ...


Automatic Verification Of Finite Precision Implementations Of Linear Controllers, Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee Apr 2017

Automatic Verification Of Finite Precision Implementations Of Linear Controllers, Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

We consider the problem of verifying finite precision implementation of linear time-invariant controllers against mathematical specifications. A specification may have multiple correct implementations which are different from each other in controller state representation, but equivalent from a perspective of input-output behavior (e.g., due to optimization in a code generator). The implementations may use finite precision computations (e.g. floating-point arithmetic) which cause quantization (i.e., roundoff) errors. To address these challenges, we first extract a controller's mathematical model from the implementation via symbolic execution and floating-point error analysis, and then check approximate input-output equivalence between the extracted model ...


Resilient Linear Classification: An Approach To Deal With Attacks On Training Data, Sangdon Park, James Weimer, Insup Lee Apr 2017

Resilient Linear Classification: An Approach To Deal With Attacks On Training Data, Sangdon Park, James Weimer, Insup Lee

Departmental Papers (CIS)

Data-driven techniques are used in cyber-physical systems (CPS) for controlling autonomous vehicles, handling demand responses for energy management, and modeling human physiology for medical devices. These data-driven techniques extract models from training data, where their performance is often analyzed with respect to random errors in the training data. However, if the training data is maliciously altered by attackers, the effect of these attacks on the learning algorithms underpinning data-driven CPS have yet to be considered. In this paper, we analyze the resilience of classification algorithms to training data attacks. Specifically, a generic metric is proposed that is tailored to measure ...


Vcat: Dynamic Cache Management Using Cat Virtualization, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Insup Lee Apr 2017

Vcat: Dynamic Cache Management Using Cat Virtualization, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Insup Lee

Departmental Papers (CIS)

This paper presents vCAT, a novel design for dynamic shared cache management on multicore virtualization platforms based on Intel’s Cache Allocation Technology (CAT). Our design achieves strong isolation at both task and VM levels through cache partition virtualization, which works in a similar way as memory virtualization, but has challenges that are unique to cache and CAT. To demonstrate the feasibility and benefits of our design, we provide a prototype implementation of vCAT, and we present an extensive set of microbenchmarks and performance evaluation results on the PARSEC benchmarks and synthetic workloads, for both static and dynamic allocations. The ...


Autov: An Automotive Testbed For Real-Time Virtualization, Meng Xu, Insup Lee Apr 2017

Autov: An Automotive Testbed For Real-Time Virtualization, Meng Xu, Insup Lee

Departmental Papers (CIS)

Timing isolation is critical for automotive systems. Real-time virtualization, such as RT-Xen, is a promising technique to integrate legacy automotive systems onto a powerful multi-core platform for achieving better performance and lower cost without breaking the timing isolation. However, the real-time virtualization has never been evaluated with real automotive applications in a non-simulation environment. In order to facilitate the evaluation of real-time virtualization for automotive systems, we propose the AutoV, an affordable and accessible automotive testbed for real-time virtualization. We present a case study to demonstrate the applications of the AutoV.


Design And Implementation Of Attack-Resilient Cyber-Physical Systems, Miroslav Pajic, James Weimer, Nicola Bezzo, Oleg Sokolsky, George Pappas, Insup Lee Apr 2017

Design And Implementation Of Attack-Resilient Cyber-Physical Systems, Miroslav Pajic, James Weimer, Nicola Bezzo, Oleg Sokolsky, George Pappas, Insup Lee

Departmental Papers (CIS)

Recent years have witnessed a significant increase in the number of security-related incidents in control systems. These include high-profile attacks in a wide range of application domains, from attacks on critical infrastructure, as in the case of the Maroochy Water breach [1], and industrial systems (such as the StuxNet virus attack on an industrial supervisory control and data acquisition system [2], [3] and the German Steel Mill cyberattack [4], [5]), to attacks on modern vehicles [6]-[8]. Even high-assurance military systems were shown to be vulnerable to attacks, as illustrated in the highly publicized downing of the RQ-170 Sentinel U ...


Data-Driven Adaptive Safety Monitoring Using Virtual Subjects In Medical Cyber-Physical Systems: A Glucose Control Case Study, Sanjian Chen, Oleg Sokolsky, James Weimer, Insup Lee Sep 2016

Data-Driven Adaptive Safety Monitoring Using Virtual Subjects In Medical Cyber-Physical Systems: A Glucose Control Case Study, Sanjian Chen, Oleg Sokolsky, James Weimer, Insup Lee

Departmental Papers (CIS)

Medical cyber-physical systems (MCPS) integrate sensors, actuators, and software to improve patient safety and quality of healthcare. These systems introduce major challenges to safety analysis because the patient’s physiology is complex, nonlinear, unobservable, and uncertain. To cope with the challenge that unidentified physiological parameters may exhibit short-term variances in certain clinical scenarios, we propose a novel run-time predictive safety monitoring technique that leverages a maximal model coupled with online training of a computational virtual subject (CVS) set. The proposed monitor predicts safety-critical events at run-time using only clinically available measurements. We apply the technique to a surgical glucose control ...


Smedl: Combining Synchronous And Asynchronous Monitoring, Teng Zhang, Peter Gebhard, Oleg Sokolsky Sep 2016

Smedl: Combining Synchronous And Asynchronous Monitoring, Teng Zhang, Peter Gebhard, Oleg Sokolsky

Departmental Papers (CIS)

Two major approaches have emerged in runtime verification, based on synchronous and asynchronous monitoring. Each approach has its advantages and disadvantages and is applicable in different situations. In this paper, we explore a hybrid approach, where low-level properties are checked synchronously, while higher-level ones are checked asynchronously. We present a tool for constructing and deploying monitors based on an architecture specification. Monitor logic and patterns of communication between monitors are specified in a language SMEDL. The language and the tool are illustrated using a case study of a robotic simulator.


Platform-Based Plug And Play Of Automotive Safety Features - Challenges And Directions, Deepak Gangadharan, Jin Hyun Kim, Insup Lee, Oleg Sokolsky, Baekgyu Kim, Shin'ichi Shiraishi Aug 2016

Platform-Based Plug And Play Of Automotive Safety Features - Challenges And Directions, Deepak Gangadharan, Jin Hyun Kim, Insup Lee, Oleg Sokolsky, Baekgyu Kim, Shin'ichi Shiraishi

Departmental Papers (CIS)

Optional software-based features are increasingly becoming an important cost driver in automotive systems. These include features pertaining to active safety, infotainment, etc. Currently, these optional features are integrated into the vehicles at the factory during assembly. This severely restricts the flexibility of the customer to select and use features on-demand and therefore, the customer will either have to be satisfied with an available set of feature options or pre-order a car with the required features from the manufacturer resulting in considerable delay. In order to increase flexibility and reduce the delay, it is necessary to provide the option to configure ...


Clinician-In-The-Loop Annotation Of Icu Bedside Alarm Data, Alexander Roederer, Joseph Dimartino, Jacob Gutsche, Margaret Mullen-Fortino, Sachin Shah, C. William Hanson Iii, Insup Lee Jun 2016

Clinician-In-The-Loop Annotation Of Icu Bedside Alarm Data, Alexander Roederer, Joseph Dimartino, Jacob Gutsche, Margaret Mullen-Fortino, Sachin Shah, C. William Hanson Iii, Insup Lee

Departmental Papers (CIS)

In this work, we describe the state of clinical monitoring in the intensive care unit and operating room, where patients are at their most fragile and thus monitoring is most heightened. We describe how large amounts of data generated by monitoring patients’ physiologic signals, along with the ubiquitous aspecific threshold alarms in use today, cause dangerous alarm fatigue for medical caregivers. In order to build more specific, more useful alarms, we gathered a novel data set that would allow us to assess the number, types, and utility of alarms currently in use in the intensive care unit. To do this ...


Cloud-Based Secure Logger For Medical Devices, Hung Nguyen, Bipeen Acharya, Radoslav Ivanov, Andreas Haeberlen, Linh T.X. Phan, Oleg Sokolsky, Jesse Walker, James Weimer, C. William Hanson Iii, Insup Lee Jun 2016

Cloud-Based Secure Logger For Medical Devices, Hung Nguyen, Bipeen Acharya, Radoslav Ivanov, Andreas Haeberlen, Linh T.X. Phan, Oleg Sokolsky, Jesse Walker, James Weimer, C. William Hanson Iii, Insup Lee

Departmental Papers (CIS)

A logger in the cloud capable of keeping a secure, time-synchronized and tamper-evident log of medical device and patient information allows efficient forensic analysis in cases of adverse events or attacks on interoperable medical devices. A secure logger as such must meet requirements of confidentiality and integrity of message logs and provide tamper-detection and tamper-evidence. In this paper, we propose a design for such a cloud-based secure logger using the Intel Software Guard Extensions (SGX) and the Trusted Platform Module (TPM). The proposed logger receives medical device information from a dongle attached to a medical device. The logger relies on ...


Monitoring Assumptions In Assume-Guarantee Contracts, Oleg Sokolsky, Teng Zhang, Insup Lee, Michael Mcdougall Jun 2016

Monitoring Assumptions In Assume-Guarantee Contracts, Oleg Sokolsky, Teng Zhang, Insup Lee, Michael Mcdougall

Departmental Papers (CIS)

Pre-deployment verification of software components with respect to behavioral specifications in the assume-guarantee form does not, in general, guarantee absence of errors at run time. This is because assumptions about the environment cannot be discharged until the environment is fixed. An intuitive approach is to complement pre-deployment verification of guarantees, up to the assumptions, with post-deployment monitoring of environment behavior to check that the assumptions are satisfied at run time. Such a monitor is typically implemented by instrumenting the application code of the component. An additional challenge for the monitoring step is that environment behaviors are typically obtained through an ...


Estimation Of Blood Oxygen Content Using Context-Aware Filtering, Radoslav Ivanov, Nikolay Atanasov, James Weimer, Miroslav Pajic, Allan F. Simpao, Mohamed A. Rehman, George Pappas, Insup Lee Apr 2016

Estimation Of Blood Oxygen Content Using Context-Aware Filtering, Radoslav Ivanov, Nikolay Atanasov, James Weimer, Miroslav Pajic, Allan F. Simpao, Mohamed A. Rehman, George Pappas, Insup Lee

Departmental Papers (CIS)

In this paper we address the problem of estimating the blood oxygen concentration in children during surgery.Currently, the oxygen content can only be measured through invasive means such as drawing blood from the patient. In this work, we attempt to perform estimation by only using other non-invasive measurements (e.g., fraction of oxygen in inspired air, volume of inspired air) collected during surgery. Although models mapping these measurements to blood oxygen content contain multiple parameters that vary widely across patients, the non-invasive measurements can be used to provide binary information about whether the oxygen concentration is rising or dropping ...