Physical Sciences and Mathematics Commons^™

Platform-Specific Code Generation From Platform-Independent Timed Models, Baekgyu Kim, Lu Feng, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

Many safety-critical real-time embedded systems need to meet stringent timing constraints such as preserving delay bounds between input and output events. In model-based development, a system is often implemented by using a code generator to automatically generate source code from system models, and integrating the generated source code with a platform. It is challenging to guarantee that the implemented systems preserve required timing constraints, because the timed behavior of the source code and the platform is closely intertwined. In this paper, we address this challenge by proposing a model transformation approach for the code generation. Our approach compensates the platform-processing …

From Requirements To Code: Model Based Development Of A Medical Cyber Physical System, Anitha Murugesan, Mats Heimdahl, Michael Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, Baekgyu Kim, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

The advanced use of technology in medical devices has improved the way health care is delivered to patients. Unfortunately, the increased complexity of modern medical devices poses challenges for development, assurance, and regulatory approval. In an e ort to improve the safety of advanced medical devices, organizations such as FDA have supported exploration of techniques to aid in the development and regulatory approval of such systems. In an ongoing research project, our aim is to provide effective development techniques and exemplars of system development artifacts that demonstrate state of the art development techniques.

In this paper we present an end-to-end …

Verified Ros-Based Deployment Of Platform-Independent Control Systems, Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee

Oleg Sokolsky

The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces. Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always …

Verified Ros-Based Deployment Of Platform-Independent Control Systems, Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee

Oleg Sokolsky

The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces. Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always …

Automatic Verification Of Linear Controller Software, Miroslav Pajic, Junkil Park, Insup Lee, George Pappas, Oleg Sokolsky

Oleg Sokolsky

We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller’s state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller’s transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.

From Requirements To Code: Model Based Development Of A Medical Cyber Physical System, Anitha Murugesan, Mats Heimdahl, Michael Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, Baekgyu Kim, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

The advanced use of technology in medical devices has improved the way health care is delivered to patients. Unfortunately, the increased complexity of modern medical devices poses challenges for development, assurance, and regulatory approval. In an e ort to improve the safety of advanced medical devices, organizations such as FDA have supported exploration of techniques to aid in the development and regulatory approval of such systems. In an ongoing research project, our aim is to provide effective development techniques and exemplars of system development artifacts that demonstrate state of the art development techniques.

In this paper we present an end-to-end …

Platform-Specific Code Generation From Platform-Independent Timed Models, Baekgyu Kim, Lu Feng, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

Many safety-critical real-time embedded systems need to meet stringent timing constraints such as preserving delay bounds between input and output events. In model-based development, a system is often implemented by using a code generator to automatically generate source code from system models, and integrating the generated source code with a platform. It is challenging to guarantee that the implemented systems preserve required timing constraints, because the timed behavior of the source code and the platform is closely intertwined. In this paper, we address this challenge by proposing a model transformation approach for the code generation. Our approach compensates the platform-processing …

A Data-Driven Behavior Modeling And Analysis Framework For Diabetic Patients On Insulin Pumps, Sanjian Chen, Lu Feng, Michael Rickels, Amy Peleckis, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

About 30%-40% of Type 1 Diabetes (T1D) patients in the United States use insulin pumps. Current insulin infusion systems require users to manually input meal carb count and approve or modify the system-suggested meal insulin dose. Users can give correction insulin boluses at any time. Since meal carbohydrates and insulin are the two main driving forces of the glucose physiology, the user-specific eating and pump-using behavior has a great impact on the quality of glycemic control.

In this paper, we propose an “Eat, Trust, and Correct” (ETC) framework to model the T1D insulin pump users’ behavior. We use machine learning …

A Safety-Assured Development Approach For Real-Time Software, Eunkyoung Jee, Shaohui Wang, Jeong Ki Kim, Jaewoo Lee, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

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 …

Co-Design Of Control And Platform With Dropped Signals, Damoon Soudbakhsh, Linh T.X. Phan, Oleg Sokolsky, Insup Lee, Anuradha Annaswamy

Oleg Sokolsky

This paper examines a co-design of control and platform in the presence of dropped signals. In a cyber-physical system, due to increasing complexities such as the simultaneous control of several applications, limited resources, and complex platform architectures, some of the signals transmitted may often be dropped. In this paper, we address the challenges that arise both from the control design and the platform design point of view. A dynamic model is proposed that accommodates these drops, and a suitable switching control design is proposed. A Multiple Lyapunov function based approach is used to guarantee the stability of the system with …

Challenges In The Regulatory Approval Of Medical Cyber-Physical Systems, Oleg Sokolsky, Insup Lee, Mats Heimdahl

Oleg Sokolsky

We are considering the challenges that regulators face in approving modern medical devices, which are software intensive and increasingly network enabled. We then consider assurance cases, which o er the means of organizing the evidence into a coherent argument demonstrating the level of assurance provided by a system, and discuss research directions that promise to make construction and evaluation of assurance cases easier and more precise. Finally, we discuss some recent trends that will further complicate the regulatory approval of medical cyber-physical systems.

Model-Based Development Of The Generic Pca Infusion Pump User Interface Prototype In Pvs, Paolo Masci, Anaheed Ayoub, Paul Curzon, Insup Lee, Oleg Sokolsky, Harold Thimbleby

Oleg Sokolsky

A realistic user interface is rigorously developed for the US Food and Drug Administration (FDA) Generic Patient Controlled Analgesia (GPCA) pump prototype. The GPCA pump prototype is intended as a realistic workbench for trialling development methods and techniques for improving the safety of such devices. A model-based approach based on the use of formal methods is illustrated and implemented within the Prototype Verification System (PVS) verification system. The user interface behaviour is formally specified as an executable PVS model. The specification is verified with the PVS theorem prover against relevant safety requirements provided by the FDA for the GPCA pump. …

Cache-Aware Compositional Analysis Of Real-Time Multicore Virtualization Platforms, Meng Xu, Linh T.X. Phan, Insup Lee, Oleg Sokolsky, Sisu Xi, Chenyang Lu, Christopher Gill

Oleg Sokolsky

Multicore processors are becoming ubiquitous, and it is becoming increasingly common to run multiple real-time systems on a shared multicore platform. While this trend helps to reduce cost and to increase performance, it also makes it more challenging to achieve timing guarantees and functional isolation. One approach to achieving functional isolation is to use virtualization. However, virtualization also introduces many challenges to the multicore timing analysis; for instance, the overhead due to cache misses becomes harder to predict, since it depends not only on the direct interference between tasks but also on the indirect interference between virtual processors and the …

Towards Synthesis Of Platform-Aware Attack-Resilient Control Systems: Extended Abstract, Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, Insup Lee

Oleg Sokolsky

No abstract provided.

Model-Based Testing Of Gui-Driven Applications, Vivien Chinnapongse, Insup Lee, Oleg Sokolsky, Shaohui Wang, Paul L. Jones

Oleg Sokolsky

While thorough testing of reactive systems is essential to ensure device safety, few testing methods center on GUI-driven applications. In this paper we present one approach for the model-based testing of such systems. Using the AHLTA-Mobile case study to demonstrate our approach, we first introduce a high-level method of modeling the expected behavior of GUI-driven applications. We show how to use the NModel tool to generate test cases from this model and present a way to execute these tests within the application, highlighting the challenges of using an API-geared tool in a GUI-based setting. Finally we present the results of …

Platform-Dependent Code Generation For Embedded Real-Time Software, Baekgyu Kim, Linh T.X. Phan, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

Code generation for embedded systems is challenging, since the generated code (e.g., C code) is expected to run on a heterogeneous set of target platforms with different characteristics, such as hardware/software architectures and programming interfaces. We propose a code generation framework that provides the flexibility to generate different source code that is executable on each target platform. In our framework, the platform-dependent characteristics of a target platform are explicitly specified by an Architectural Analysis Description Language (AADL) model and a code snippet repository. The AADL model captures hardware/software architectural aspects of the platform, such as periodic/aperiodic threads and their interactions …

Linking Abstract Analysis To Concrete Design: A Hierarchical Approach To Verify Medical Cps Safety, Anitha Murugesan, Oleg Sokolsky, Sanjai Rayadurgam, Michael Whalen, Mats Heimdahl, Insup Lee

Oleg Sokolsky

Complex cyber-physical systems are typically hierarchically organized into multiple layers of abstraction in order to manage design complexity and provide verification tractability. Formal reasoning about such systems, therefore, necessarily involves the use of multiple modeling formalisms, verification paradigms, and concomitant tools, chosen as appropriate for the level of abstraction at which the analysis is performed. System properties verified using an abstract component specification in one paradigm must then be shown to logically follow from properties verified, possibly using a different paradigm, on a more concrete component description, if one is to claim that a particular component when deployed in the …

Assuring The Safety Of On-Demand Medical Cyber-Physical Systems, Andrew L. King, Lu Feng, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

We present an approach to establish safety of on-demand medical cyber-physical systems which are assembled to treat a patient in a specific clinical scenario. We treat such a system as a virtual medial device (VMD) and propose a model-based framework that includes a modeling language with formal semantics and a medical application platform (MAP) that provides the necessary deployment support for the VMD models.

Robustness Of Attack-Resilient State Estimators, Miroslav Pajic, James Weimer, Nicola Bezzo, Paulo Tabuada, Oleg Sokolsky, Insup Lee, George Pappas

Oleg Sokolsky

The interaction between information technology and physical world makes Cyber-Physical Systems (CPS) vulnerable to malicious attacks beyond the standard cyber attacks. This has motivated the need for attack-resilient state estimation. Yet, the existing state-estimators are based on the non-realistic assumption that the exact system model is known. Consequently, in this work we present a method for state estimation in presence of attacks, for systems with noise and modeling errors. When the the estimated states are used by a state-based feedback controller, we show that the attacker cannot destabilize the system by exploiting the difeerence between the model used for the …

Biomedical Devices And Systems Security, David Arney, Krishna Venkatasubramanian, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

Medical devices have been changing in revolutionary ways in recent years. One is in their form-factor. Increasing miniaturization of medical devices has made them wearable, light-weight, and ubiquitous; they are available for continuous care and not restricted to clinical settings. Further, devices are increasingly becoming connected to external entities through both wired and wireless channels. These two developments have tremendous potential to make healthcare accessible to everyone and reduce costs. However, they also provide increased opportunity for technology savvy criminals to exploit them for fun and profit. Consequently, it is essential to consider medical device security issues. In this paper, …

As-Trust: A Trust Quantification Scheme For Autonomous Systems In Bgp, Jian Chang, Krishna Venkatasubramanian, Andrew West, Sampath Kannan, Boon Thau Loo, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

The Border Gateway Protocol (BGP) works by frequently exchanging updates that disseminate reachability information about IP prefixes (i.e., IP address blocks) between Autonomous Systems (ASes) on the Internet. The ideal operation of BGP relies on three major behavioral assumptions (BAs): (1) information contained in the update is legal and correct, (2) a route to a prefix is stable, and (3) the route adheres to the valley free routing policy. The current operation of BGP implicitly trusts all ASes to adhere to these assumptions. However, several documented violation of these assumptions attest to the fact that such an assumption of trust …

Functional Alarms For Systems Of Interoperable Medical Devices, Krishna Venkatasubramanian, Eugene Vasserman, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

Alarms are essential for medical systems in order to ensure patient safety during deteriorating clinical situations and inevitable device malfunction. As medical devices are connected together to become interoperable, alarms become crucial part in making them high-assurance, in nature. Traditional alarm systems for interoperable medical devices have been patient-centric. In this paper, we introduce the need for an alarm system that focuses on the correct functionality of the interoperability architecture itself, along with several considerations and design challenges in enabling them.

Runtime Assurance Based On Formal Specifications, Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan

Oleg Sokolsky

We describe the Monitoring and Checking (MaC) framework which assures the correctness of the current execution at run-time. Monitoring is performed based on a formal specification of system requirements. MaC bridges the gap between formal specification and verification, which ensures the correctness of a design rather than an implementation, and testing, which partially validates an implementation. An important aspect of the framework is a clear separation between implementation-dependent description of monitored objects and high-level requirements specification. Another salient feature is automatic instrumentation of executable code. The paper presents an overview of the framework and two languages to specify monitoring scripts …

Compositional Analysis Of Real-Time Embedded Systems, Linh T.X. Phan, Insup Lee, Oleg Sokolsky

Oleg Sokolsky

This tutorial is concerned with various aspects of component-based design and compositional analysis of real-time embedded systems. It will first give an overview of component-based frameworks and their underlying principles. It will then go in-depth into abstraction methods for real-time components and techniques for computing their optimal interfaces, for both systems implemented on uniprocessor and multiprocessor platforms, as well as extensions to multi-mode systems. Besides theoretical aspects, the tutorial will also present an implementation of the compositional analysis framework on Xen virtualization and a demonstration of the CARTS toolset with several examples seeing the techniques in action. It will also …

The Medical Device Dongle: An Open-Source Standards-Based Platform For Interoperable Medical Device Connectivity, Philip Asare, Danyang Cong, Santosh Vattam, Baekgyu Kim, Andrew King, Oleg Sokolsky, Insup Lee, Shan Lin, Margaret Mullen-Fortino

Oleg Sokolsky

Emerging medical applications require device coordination, increasing the need to connect devices in an interoperable manner. However, many of the existing health devices in use were not originally developed for network connectivity and those devices with networking capabilities either use proprietary protocols or implementations of standard protocols that are unavailable to the end user. The first set of devices are unsuitable for device coordination applications and the second set are unsuitable for research in medical device interoperability. We propose the Medical Device Dongle (MDD), a low-cost, open-source platform that addresses both issues.

Process-Algebraic Interpretation Of Aadl Models, Oleg Sokolsky, Insup Lee, Duncan Clarke

Oleg Sokolsky

We present a toolset for the behavioral verification and validation of architectural models of embedded systems expressed in the language AADL. The toolset provides simulation and timing analysis of AADL models. Underlying both tools is a process-algebraic implementation of AADL semantics. The common implementation of the semantics ensures consistency in the analysis results between the tools.

As-Cred: Reputation And Alert Service For Inter-Domain Routing, Jian Chang, Krishna Venkatasubramanian, Andrew West, Sampath Kannan, Insup Lee, Boon Thau Loo, Oleg Sokolsky

Oleg Sokolsky

Being the backbone routing system of the Internet, the operational aspect of the inter-domain routing is highly complex. Building a trustworthy ecosystem for inter-domain routing requires the proper maintenance of trust relationships among tens of thousands of peer IP domains called Autonomous Systems (ASes). ASes today implicitly trust any routing information received from other ASes as part of the Border Gateway Protocol (BGP) updates. Such blind trust is problematic given the dramatic rise in the number of anomalous updates being disseminated, which pose grave security consequences for the inter-domain routing operation. In this paper, we present ASCRED, an AS reputation …

Resilient Parameter-Invariant Control With Application To Vehicle Cruise Control, James Weimer, Nicola Bezzo, Miroslav Pajic, George J. Pappas, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

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.

Challenges And Research Directions In Medical Cyber-Physical Systems, Insup Lee, Oleg Sokolsky, Sanjian Chen, John Hatcliff, Eunkyoung Jee, Baekgyu Kim, Andrew King, Margaret Mullen-Fortino, Soojin Park, Alexander Roederer, Krishna Venkatasubramanian

Oleg Sokolsky

Medical cyber-physical systems (MCPS) are lifecritical, context-aware, networked systems of medical devices. These systems are increasingly used in hospitals to provide highquality continuous care for patients. The need to design complex MCPS that are both safe and effective has presented numerous challenges, including achieving high assurance in system software, intoperability, context-aware intelligence, autonomy, security and privacy, and device certifiability. In this paper, we discuss these challenges in developing MCPS, some of our work in addressing them, and several open research issues

Link Spamming Wikipedia For Profit, Andrew West, Jian Chang, Krishna Venkatasubramanian, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

Collaborative functionality is an increasingly prevalent web technology. To encourage participation, these systems usually have low barriers-to-entry and permissive privileges. Unsurprisingly, ill-intentioned users try to leverage these characteristics for nefarious purposes. In this work, a particular abuse is examined -- link spamming -- the addition of promotional or otherwise inappropriate hyperlinks.

Our analysis focuses on the "wiki" model and the collaborative encyclopedia, Wikipedia, in particular. A principal goal of spammers is to maximize *exposure*, the quantity of people who view a link. Creating and analyzing the first Wikipedia link spam corpus, we find that existing spam strategies perform quite poorly …