Lee, Insup

Collection

Researcher profiles

View all metadata

Search Results

Now showing 1 - 10 of 321

Resilient Parameter-Invariant Control With Application to Vehicle Cruise Control
(2013-03-20) Weimer, James; Bezzo, Nicola; Pajic, Miroslav; Pappas, George J.; Sokolsky, Oleg; Lee, Insup
This work addresses the general problem of resilient control of unknown stochastic linear time-invariant (LTI) systems in the presence of sensor attacks. Motivated by a vehicle cruise control application, this work considers a first order system with multiple measurements, of which a bounded subset may be corrupted. A frequency-domain-designed resilient parameter-invariant controller is introduced that simultaneously minimizes the effect of corrupted sensors, while maintaining a desired closed-loop performance, invariant to unknown model parameters. Simulated results illustrate that the resilient parameter-invariant controller is capable of stabilizing unknown state disturbances and can perform state trajectory tracking.
Compositional Real-Time Scheduling Framework
(2004-12-06) Shin, Insik; Lee, Insup
Our goal is to develop a compositional real-time scheduling framework so that global (system-level) timing properties can be established by composing independently (specified and) analyzed local (component-level) timing properties. The two essential problems in developing such a framework are (1) to abstract the collective real-time requirements of a component as a single real-time requirement and (2) to compose the component demand abstraction results into the system-level real-time requirement. In our earlier work, we addressed the problems using the Liu and Layland periodic model. In this paper, we address the problems using another well-known model, a bounded-delay resource partition model, as a solution model to the problems. To extend our framework to this model, we develop an exact feasibility condition for a set of bounded-delay tasks over a bounded-delay resource partition. In addition, we present simulation results to evaluate the overheads that the component demand abstraction results incur in terms of utilization increase. We also present new utilization bound results on a bounded-delay resource model.
A Safety-Assured Development Approach for Real-Time Software
(2010-08-23) Jee, Eunkyoung; Wang, Shaohui; Kim, Jeong Ki; Lee, Jaewoo; Sokolsky, Oleg; Lee, Insup
Guaranteeing timing properties is an important issue as we develop safety-critical real-time systems such as cardiac pacemakers. We present a safety assured development approach of real-time software using a pacemaker as our case study. Following the model-driven development techniques, measurement-based timing analysis is used to guarantee timing properties in implementation as well as in the formal model. Formal specification with timed automata is checked with respect to timing properties by model checking technique and is transformed into implementation systematically. When timing properties may be violated in the implementation due to timing delay, it is suggested to measure the time deviation and reflect it to the code explicitly by modifying guards. The model is altered according to the modifications in the code. These changes of the code and the model are considered safe if all the properties are still satisfied by the modified model in re-performed model hecking. We demonstrate how the suggested approach can be applied to single-threaded and multi-threaded versions of implementation. This approach can provide developers with a useful time-guaranteeing technique applicable to several code generation schemes without imposing many restrictions.
Improving Patient Safety With X-Ray and Anesthesia Machine Ventilator Synchronization: A Medical Device Interoperability Case Study
(2009-01-14) Arney, David; Goldman, Julian M.; Whitehead, Susan F; Lee, Insup
When a x-ray image is needed during surgery, clinicians may stop the anesthesia machine ventilator while the exposure is made. If the ventilator is not restarted promptly, the patient may experience severe complications. This paper explores the interconnection of a ventilator and simulated x-ray into a prototype plug-and-play medical device system. This work assists ongoing interoperability framework development standards efforts to develop functional and non-functional requirements and illustrates the potential patient safety benefits of interoperable medical device systems by implementing a solution to a clinical use case requiring interoperability.
Statistical Runtime Checking of Probabilistic Properties
(2007-03-13) Sammapun, Usa; Lee, Insup; Sokolsky, Oleg; Regehr, John
Probabilistic correctness is an important aspect of reliable systems. A soft real-time system, for instance, may be designed to tolerate some degree of deadline misses under a threshold. Since probabilistic systems may behave differently from their probabilistic models depending on their current environments, checking the systems at runtime can provide another level of assurance for their probabilistic correctness. This paper presents a statistical runtime verification for probabilistic properties using statistical analysis. However, while this statistical analysis collects a number of execution paths as samples to check probabilistic properties within some certain error bounds, runtime verification can only produce one single sample. This paper provides a technique to produce such a number of samples and applies this methodology to check probabilistic properties in wireless sensor network applications.
Distributed-Code Generation from Hybrid Systems Models for Time-delayed Multirate Systems
(2005-09-19) Anand, Madhukar; Fischmeister, Sebastian; Kim, Jesung; Lee, Insup
Hybrid systems are an appropriate formalism to model embedded systems as they capture the theme of continuous dynamics with discrete control. A simple extension, a network of communicating hybrid automata, allows for modeling distributed embedded systems. Although it is possible to generate code from such models, it is difficult to provide formal guarantees in the code with respect to the model. One of the reasons for this is that, the model is set in continuous time and concurrent execution with instantaneous communication, whereas the generated code is set in discrete time with delayed communication. This can introduce semantic differences between the model and the code such as missed transitions, faulty transitions, and altered continuous behavior. The goal of faithful code generation is to minimize these differences. In this paper, we propose a relaxed criteria of relative faithful implementation. Based on this criteria, we propose dynamically adjusting the guard at runtime using estimates of errors for preventing faulty transitions. We also identify a sufficient condition to ensure no missed transitions in the code.
Runtime verification of parametric properties using SMEDL
(2019-09-01) Zhang, Teng; Kaur, Ramneet; Lee, Insup; Sokolsky, Oleg
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 is encoded by a hierarchy of monitors for aggregating verdicts of sub traces. Through case studies, we demonstrate that SMEDL provides a natural way to monitor parametric properties with more potentials for flexible deployment and optimizations.
Towards Secure Cloud Data Management
(2010-01-01) Zhou, Wenchao; Marczak, William R.; Sherr, Micah; Tao, Tao; Loo, Boon Thau; Zhang, Zhuoyao; Lee, Insup
This paper explores the security challenges posed by data-intensive applications deployed in cloud environments that span administrative and network domains. We propose a data-centric view of cloud security and discuss data management challenges in the areas of secure distributed data processing, end-to-end query result verification, and cross-user trust policy management. In addition, we describe our current and future efforts to investigate security challenges in cloud data management using the Declarative Secure Distributed Systems (DS2) platform, a declarative infrastructure for specifying, analyzing, and deploying secure information systems.
An Empirical Analysis of Scheduling Techniques for Real-Time Cloud-Based Data Processing
(2011-12-01) Phan, Linh T.X.; Loo, Boon Thau; Zhang, Zhuoyao; Lee, Insup; Zheng, Qi
In this paper, we explore the challenges and needs of current cloud infrastructures, to better support cloud-based data-intensive applications that are not only latency-sensitive but also require strong timing guarantees. These applications have strict deadlines (e.g., to perform time-dependent mission critical tasks or to complete real-time control decisions using a human-in-the-loop), and deadline misses are undesirable. To highlight the challenges in this space, we provide a case study of the online scheduling of MapReduce jobs executed by Hadoop. Our evaluations on Amazon EC2 show that the existing Hadoop scheduler is ill-equipped to handle jobs with deadlines. However, by adapting existing multiprocessor scheduling techniques for the cloud environment, we observe significant performance improvements in minimizing missed deadlines and tardiness. Based on our case study, we discuss a range of challenges in this domain posed by virtualization and scale, and propose our research agenda centered around the application of advanced real-time scheduling techniques in the cloud environment.
Real-Time Traffic Congestion Prediction
(2008-11-01) Mangharam, Rahul; Lee, Insup; Sokolsky, Oleg

Lee, Insup

Email Address

ORCID

Disciplines

relationships.isProjectOf

relationships.isOrgUnitOf

Position

Introduction

Research Interests

Collection

Filters

Settings

Sort By

Results per page

Search Results

Penn's Heritage