Computer Engineering 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 …

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 …

A Semantic Framework For Mode Change Protocols, Linh T.X. Phan, Insup Lee, Oleg Sokolsky

Oleg Sokolsky

We present a unified framework for the specification and analysis of mode-change protocols used in multi-mode realtime systems. We propose a highly expressive formalism, called MCP, to model the system behavior during mode transitions, and show how various existing mode change protocols can be described as MCPs. The explicit representation of the MCP model provides a means to analyze the system state during a mode transition as well as during an intra-mode execution. We introduce the concept of feasibility with respect to the MCP model, and give a decidable method for checking the feasibility of a MCP for a given …

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.

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 …

Permission To Speak: A Logic For Access Control And Conformance, Nikhil Dinesh, Aravind Joshi, Insup Lee, Oleg Sokolsky

Oleg Sokolsky

Formal languages for policy have been developed for access control and conformance checking. In this paper, we describe a formalism that combines features that have been developed for each application. From access control, we adopt the use of a saying operator. From conformance checking, we adopt the use of operators for obligation and permission. The operators are combined using an axiom that permits a principal to speak on behalf of another. The combination yields benefits to both applications. For access control, we overcome the problematic interaction between hand-off and classical reasoning. For conformance, we obtain a characterization of legal power …

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.

From Verification To Implementation: A Model Translation Tool And A Pacemaker Case Study, Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, Rahul Mangharam

Oleg Sokolsky

Model-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling of the real-time system, followed by the model’s verification at an early stage. The verified model must then be translated to a more detailed model for simulation-based testing and finally translated into executable code in a physical implementation. As later stages build on the same core model, it is essential that models used earlier in the pipeline are valid approximations of the more detailed models developed downstream. The focus of this effort is on the design and development of a model translation tool, UPP2SF, and …

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 …

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.

Safety-Critical Medical Device Development Using The Upp2sf Model, Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, Rahul Mangharam

Oleg Sokolsky

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to …

A Safety Argument Strategy For Pca Closed-Loop Systems: A Preliminary Proposal, Lu Feng, Andrew L. King, Sanjian Chen, Anaheed Ayoub, Junkil Park, Nicola Bezzo, Oleg Sokolsky, Insup Lee

Oleg Sokolsky

The emerging network-enabled medical devices impose new challenges for the safety assurance of medical cyber-physical systems (MCPS). In this paper, we present a case study of building a high-level safety argument for a patient-controlled analgesia (PCA) closed-loop system, with the purpose of exploring potential methodologies for assuring the safety of MCPS.