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

Engineering Commons

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

Articles 1 - 13 of 13

Full-Text Articles in Engineering

Detecting Security Leaks In Hybrid Systems With Information Flow Analysis, Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, Rajeev Alur Oct 2019

Detecting Security Leaks In Hybrid Systems With Information Flow Analysis, Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, Rajeev Alur

Departmental Papers (CIS)

Information flow analysis is an effective way to check useful security properties, such as whether secret information can leak to adversaries. Despite being widely investigated in the realm of programming languages, information-flow- based security analysis has not been widely studied in the domain of cyber-physical systems (CPS). CPS provide interesting challenges to traditional type-based techniques, as they model mixed discrete-continuous behaviors and are usually expressed as a composition of state machines. In this paper, we propose a lightweight static analysis methodology that enables information security properties for CPS models.We introduce a set of security rules for hybrid automata that ...


Overhead-Aware Deployment Of Runtime Monitors, Teng Zhang, Greg Eakman, Insup Lee, Oleg Sokolsky Oct 2019

Overhead-Aware Deployment Of Runtime Monitors, Teng Zhang, Greg Eakman, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

One important issue needed to be handled when applying runtime verification is the time overhead introduced by online monitors. According to how monitors are deployed with the system to be monitored, the overhead may come from the execution of monitoring logic or asynchronous communication. In this paper, we present a method for deciding how to deploy runtime monitors with awareness of minimizing the overhead. We first propose a parametric model to estimate the overhead given the prior knowledge on the distribution of incoming events and the time cost of sending a message and executing monitoring logic. Then, we will discuss ...


A Retrospective Look At The Monitoring And Checking (Mac) Framework, Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan Oct 2019

A Retrospective Look At The Monitoring And Checking (Mac) Framework, Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan

Departmental Papers (CIS)

The Monitoring and Checking (MaC) project gave rise to a framework for runtime monitoring with respect to formally specified properties, which later came to be known as runtime verification. The project also built a pioneering runtime verification tool, Java-MaC, that was an instantiation of the approach to check properties of Java programs. In this retrospective, we discuss decisions made in the design of the framework and summarize lessons learned in the course of the project.


Runtime Verification Of Parametric Properties Using Smedl, Teng Zhang, Ramneet Kaur, Insup Lee, Oleg Sokolsky Sep 2019

Runtime Verification Of Parametric Properties Using Smedl, Teng Zhang, Ramneet Kaur, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

Parametric properties are typical properties to be checked in runtime verification (RV). As a common technique for parametric monitoring, trace slicing divides an execution trace into a set of sub traces which are checked against non-parametric base properties. An efficient trace slicing algorithm is implemented in MOP. Another RV technique, QEA further allows for nested use of universal and existential quantification over parameters. In this paper, we present a methodology for parametric monitoring using the RV framework SMEDL. Trace slicing algorithm in MOP can be expressed by execution of a set of SMEDL monitors. Moreover, the semantics of nested quantifiers ...


Fly-By-Logic: A Tool For Unmanned Aircraft System Fleet Planning Using Temporal Logic, Yash Vardhan Pant, Rhudii A. Quaye, Houssam Abbas, Akarsh Varre, Rahul Mangharam May 2019

Fly-By-Logic: A Tool For Unmanned Aircraft System Fleet Planning Using Temporal Logic, Yash Vardhan Pant, Rhudii A. Quaye, Houssam Abbas, Akarsh Varre, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

Safe planning for fleets of Unmaned Aircraft Systems (UAS) performing complex missions in urban environments has typically been a challenging problem. In the United States of America, the National Aeronautics and Space Administration (NASA) and the Federal Aviation Administration (FAA) have been studying the regulation of the airspace when multiple such fleets of autonomous UAS share the same airspace, outlined in the Concept of Operations document (ConOps). While the focus is on the infrastructure and management of the airspace, the Unmanned Aircraft System (UAS) Traffic Management (UTM) ConOps also outline a potential airspace reservation based system for operation where operators ...


Electroanatomic Mapping To Determine Scar Regions In Patients With Atrial Fibrillation, Jiyue He, Kuk Jin Jang, Katie Walsh, Jackson Liang, Sanjay Dixit, Rahul Mangharam Apr 2019

Electroanatomic Mapping To Determine Scar Regions In Patients With Atrial Fibrillation, Jiyue He, Kuk Jin Jang, Katie Walsh, Jackson Liang, Sanjay Dixit, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

Left atrial voltage maps are routinely acquired during electroanatomic mapping in patients undergoing catheter ablation for atrial fibrillation (AF). For patients, who have prior catheter ablation when they are in sinus rhythm (SR), the voltage map can be used to identify low voltage areas (LVAs) using a threshold of 0.2 - 0.45 mV. However, such a voltage threshold for maps acquired during AF has not been well established. A prerequisite for defining a voltage threshold is to maximize the topologically matched LVAs between the electroanatomic mapping acquired during AF and SR. This paper demonstrates a new technique to improve ...


Synthesizing Stealthy Reprogramming Attacks On Cardiac Devices, Nicola Paoletti, Zhihao Jiang, Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka Apr 2019

Synthesizing Stealthy Reprogramming Attacks On Cardiac Devices, Nicola Paoletti, Zhihao Jiang, Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka

Real-Time and Embedded Systems Lab (mLAB)

An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device’s parameters to induce unnecessary therapy or prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., are hard to detect. We focus on the discrimination algorithm underlying Boston Scientific devices (one ...


Temporal Logic Robustness For General Signal Classes, Houssam Abbas, Yash Vardhan Pant, Rahul Mangharam Apr 2019

Temporal Logic Robustness For General Signal Classes, Houssam Abbas, Yash Vardhan Pant, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

In multi-agent systems, robots transmit their planned trajectories to each other or to a central controller, and each receiver plans its own actions by maximizing a measure of mission satisfaction. For missions expressed in temporal logic, the robustness function plays the role of satisfaction measure. Currently, a Piece-Wise Linear (PWL) or piece-wise constant reconstruction is used at the receiver. This allows an efficient robustness computation algorithm - a.k.a. monitoring - but is not adaptive to the signal class of interest, and does not leverage the compression properties of more general representations. When communication capacity is at a premium, this is ...


Technical Report: Anytime Computation And Control For Autonomous Systems, Yash Vardhan Pant, Houssam Abbas, Kartik Mohta, Rhudii A. Quaye, Truong X. Nghiem, Joseph Devietti, Rahul Mangharam Apr 2019

Technical Report: Anytime Computation And Control For Autonomous Systems, Yash Vardhan Pant, Houssam Abbas, Kartik Mohta, Rhudii A. Quaye, Truong X. Nghiem, Joseph Devietti, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

The correct and timely completion of the sensing and action loop is of utmost importance in safety critical autonomous systems. A crucial part of the performance of this feedback control loop are the computation time and accuracy of the estimator which produces state estimates used by the controller. These state estimators, especially those used for localization, often use computationally expensive perception algorithms like visual object tracking. With on-board computers on autonomous robots being computationally limited, the computation time of a perception-based estimation algorithm can at times be high enough to result in poor control performance. In this work, we develop ...


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


Lcv: A Verification Tool For Linear Controller Software, Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee Apr 2019

Lcv: A Verification Tool For Linear Controller Software, Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

In the model-based development of controller software, the use of an unverified code generator/transformer may result in introducing unintended bugs in the controller implementation. To assure the correctness of the controller software in the absence of verified code genera- tor/transformer, we develop Linear Controller Verifier (LCV), a tool to verify a linear controller implementation against its original linear controller model. LCV takes as input a Simulink block diagram model and a C code implementation, represents them as linear time-invariant system models respectively, and verifies an input-output equivalence between them. We demonstrate that LCV successfully detects a known bug ...


Verisig: Verifying Safety Properties Of Hybrid Systems With Neural Network Controllers, Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, Insup Lee Apr 2019

Verisig: Verifying Safety Properties Of Hybrid Systems With Neural Network Controllers, Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, Insup Lee

Departmental Papers (CIS)

This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. We focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network’s hybrid system with the plant’s, we transform the problem into a hybrid system verification problem which can be solved using state-of-theart reachability tools. We show that reachability is decidable for networks with one hidden layer and decidable for general networks if ...


Robustness Evaluation Of Computer-Aided Clinical Trials For Medical Devices, Kuk Jin Jang, Yash Vardhan Pant, Bo Zhang, James Weimer, Rahul Mangharam Mar 2019

Robustness Evaluation Of Computer-Aided Clinical Trials For Medical Devices, Kuk Jin Jang, Yash Vardhan Pant, Bo Zhang, James Weimer, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

Medical cyber-physical systems, such as the implantable cardioverter defibrillator (ICD), require evaluation of safety and efficacy in the context of a patient population in a clinical trial. Advances in computer modeling and simulation allow for generation of a simulated cohort or virtual cohort which mimics a patient population and can be used as a source of prior information. A major obstacle to acceptance of simulation results as a source of prior information is the lack of a framework for explicitly modeling sources of uncertainty in simulation results and quantifying the effect on trial outcomes.

In this work, we formulate the ...