Lee, Insup
Email Address
ORCID
Disciplines
Search Results
Now showing 1 - 10 of 321
Publication Towards Assurance Cases for Resilient Control Systems(2014-08-01) Weimer, James; Sokolsky, Oleg; Bezzo, Nicola; Lee, InsupThe paper studies the problem of constructing assurance cases for embedded control systems developed using a model-based approach. Assurance cases aim to provide a convincing argument that the system delivers certain guarantees, based on the evidence obtained during the design and evaluation of the system. We suggest an argument strategy centered around properties of models used in the development and properties of tools that manipulate these models. The paper presents the case study of a resilient speed estimator for an autonomous ground vehicle and takes the reader through a detailed assurance case arguing that the estimator computes speed estimates with bounded error.Publication The Soundness and Completeness of ACSR (Algebra of Communicating Shared Resources)(1993-11-01) Brémond-Grégoire, Patrice; Choi, Jin-Young; Lee, InsupRecently, significant progress has been made in the development of timed process algebras for the specification and analysis of real-time systems; one of which is a timed process algebra called ACSR. ACSR supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. Equivalence between ACSR terms is defined in terms of strong bisimulation. The paper contains a set of algebraic laws that are proven sound and complete for finite ACSR agents.Publication Extensible Energy Planning Framework for Preemptive Tasks(2017-05-01) Kim, Jin Hyun; Gangadharan, Deepak; Sokolsky, Oleg; Lee, Insup; Legay, AxelCyber-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 tasks. The minimal ratio of processor frequency can be used to plan the energy supply of real-time components. Our model-based technique is extensible by refining our model with additional features so that energy management techniques and their energy efficiency can be evaluated by model checking techniques. We exploit the compositional framework for hierarchical scheduling systems and provide a new resource model for the frequency computation. As results, our use-case for avionics software components shows that our new method outperforms the classical real-time calculus (RTC) method, requiring 36.21% less frequency ratio on average for scheduling units under RM than the RTC method.Publication A Safety-Assured Development Approach for Real-Time Software(2010-08-23) Jee, Eunkyoung; Wang, Shaohui; Kim, Jeong Ki; Lee, Jaewoo; Sokolsky, Oleg; Lee, InsupGuaranteeing 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.Publication 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, QiIn 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.Publication Towards Secure Cloud Data Management(2010-01-01) Zhou, Wenchao; Marczak, William R.; Sherr, Micah; Tao, Tao; Loo, Boon Thau; Zhang, Zhuoyao; Lee, InsupThis 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.Publication Communicating Shared Resources: A Paradigm for Integrating Real-Time Specification and Implementation(1991-03-15) Lee, Insup; Davidson, Susan B; Gerber, RichardThe timed behavior of distributed real-time systems can be specified using a formalism called Communicating Shared Resources, or CSR. The underlying computation model of CSR is resource-based in which multiple resources execute synchronously, while processes assigned to the same resource are interleaved according to their priorities. CSR bridges the gap between an abstract computation model and implementation environments, but is too complex to be treated as a process algebra. We therefore give a calculus for CSR (CCSR), that provides the ability to perform equivalence proofs by syntactic manipulation. We illustrate how a CSR specification can be translated into the CCSR formalism using a periodic timed producer-consumer example, and how a translated CSR specification can be shown correct using syntactic manipulations.Publication VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems(1993-09-01) Clarke, Duncan; Lee, Insup; Xie, Hong-liangVERSA is a tool that assists in the algebraic analysis of real-time systems. It is based on ACSR, a timed process algebra designed to express resource-bound real-time distributed systems. VERSA supports the analysis of real-time processes through algebraic rewriting, interactive execution, and equivalence testing. This paper begins by presenting a brief overview of the process algebra ACSR, its syntax, operational semantics, and equivalence relations. VERSA'S process and command syntax, its algebraic rewrite system, and its state-based analysis features are described fully. The presentation includes examples that illustrate the salient features of ACSR, and output from sample VERSA sessions that demonstrate the application of the tool to real-time systems analysis.Publication Scalable Verification of Linear Controller Software(2016-04-01) Park, Junkil; Lee, Insup; Sokolsky, Oleg; Pajic, MiroslavWe consider the problem of verifying software implementations of linear time-invariant controllers against mathematical specifications. Given a controller specification, multiple correct implementations may exist, each of which uses a different representation of controller state (e.g., due to optimizations in a third-party code generator). To accommodate this variation, we first extract a controller's mathematical model from the implementation via symbolic execution, and then check input-output equivalence between the extracted model and the specification by similarity checking. We show how to automatically verify the correctness of C code controller implementation using the combination of techniques such as symbolic execution, satisfiability solving and convex optimization. Through evaluation using randomly generated controller specifications of realistic size, we demonstrate that the scalability of this approach has significantly improved compared to our own earlier work based on the invariant checking method.Publication Estimation of Blood Oxygen Content Using Context-Aware Filtering(2016-04-01) Ivanov, Radoslav; Atanasov, Nikolay; Weimer, James; Simpao, Allan F; Rehman, Mohamed A; Pappas, George; Lee, Insup; Pajic, MiroslavIn 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. This information can then be incorporated in a context-aware filter that is used to combine regular continuous measurements with discrete detection events in order to improve estimation. We evaluate the filter using real-patient data collected over the last decade at the Children’s Hospital of Philadelphia and show that it is a promising approach for the estimation of unobservable physiological variables.