Towards Synthesis Of Platform-Aware Attack-Resilient Control Systems: Extended Abstract,
2014
University of Pennsylvania
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,
2014
University of Pennsylvania
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,
2014
University of Minnesota
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,
2014
University of Pennsylvania
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,
2014
University of Pennsylvania
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,
2014
University of Pennsylvania
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,
2014
Worcester Polytechnic Institute
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,
2014
University of Pennsylvania
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,
2014
University of Pennsylvania
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,
2014
OpenX, Pasadena, CA
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,
2014
University of Pennsylvania
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,
2014
University of Pennsylvania
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,
2014
University of Pennsylvania
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.
Deterministic Versus Randomized Kaczmarz Iterative Projection,
2014
Tennessee State University
Deterministic Versus Randomized Kaczmarz Iterative Projection, Tim Wallace, Ali Sekmen
Computer Science Faculty Research
The Kaczmarz’s alternating projection method has been widely used for solving a consistent (mostly over-determined) linear system of equations Ax = b. Because of its simple iterative nature with light computation, this method was successfully applied in computerized tomography. Since tomography generates a matrix A with highly coherent rows, randomized Kaczmarz algorithm is expected to provide faster convergence as it picks a row for each iteration at random, based on a certain probability distribution. It was recently shown that picking a row at random, proportional with its norm, makes the iteration converge exponentially in expectation with a decay constant that …
A Best-Worst Scaling Model Of Climate Change Abatement By Australian Farmers,
2014
University of Western Australia, Commonwealth Scientific and Indudstrial Research Organisation (CSIRO)
A Best-Worst Scaling Model Of Climate Change Abatement By Australian Farmers, Marit E. Kragt, Nikki Dumbrell, Fiona Gibson
International Congress on Environmental Modelling and Software
Storing carbon from the atmosphere in terrestrial sinks has been proposed as an important way to mitigate climate change and is a major focus in Australia's climate change policies. Mitigation by changing agricultural practices is seen as a promising way to achieve significant reductions in C02 concentrations. Several policies therefore aim to stimulate farmers to adopt so-called 'carbon farming' practices. However, there is little information about farmers' ability and willingness to adopt carbon farming. We present a best-worst scaling model to analyse farmers' decisions about adopting climate change mitigating practices. Best-worst scaling data was collected through a survey amongst mixed …
Assessing The Transition To A Low-Carbon Economy Using Actor-Based System-Dynamic Models,
2014
Nansen International Environmental and Remote Sensing Centre, Saint Petersburg State University, Nansen Environmental and Remote Sensing Center
Assessing The Transition To A Low-Carbon Economy Using Actor-Based System-Dynamic Models, Dmitry V. Kovalevsky, Klaus Hasselmann
International Congress on Environmental Modelling and Software
For a comprehensive analysis of climate mitigation policies, Integrated Assessment models (IAMs) of the coupled climate-socioeconomic system are needed. However, while there is general agreement on the physics of the climate system, the dynamics of the socioeconomic system is still the subject of considerable controversy. This has become particularly apparent since the recent global financial crisis. To explore the dynamics of the socio-economic system, a family of socio-economic models is proposed that incorporates the various alternative assumptions regarding the behaviour of the different economic actors that govern the evolution of the socio-economic system. The model family needs to be developed …
Integration Of Models For Low Carbon Economy,
2014
University of Twente
Integration Of Models For Low Carbon Economy, Getachew F. Belete, Alexey Voinov
International Congress on Environmental Modelling and Software
Designing the transition to low carbon economy is a very complex task that touches upon a wide variety of climate-energy-economic systems. We need to explore the various possible climate mitigation scenarios at different temporal and spatial scales. However, due to the diversity of the involved disciplines it is difficult to find one complete and unified modeling approach that works equally well in all those different domains. As a result we have to select 'appropriate' models, which represent only specific aspects of the scenarios and assemble them 'coherently'. In this research we have identified some challenges in integrating multidisciplinary models; and …
Enhancing The Policy Relevance Of Scenarios Through A Dynamic Analytical Approach,
2014
Ecole des Ponts ParisTech, Cired
Enhancing The Policy Relevance Of Scenarios Through A Dynamic Analytical Approach, Céline Guivarch, Vanessa Schweizer, Julia Rozenberg
International Congress on Environmental Modelling and Software
We present a new dynamic analytical approach for studying scenarios produced by an integrated assessment {IA) model. Our approach involves the analysis of a large number of scenarios, which can better address three principal shortcomings of how uncertainty is traditionally handled in IA scenario studies. The shortcomings are all a result of the prevailing practice of investigating a small number of scenarios and include (1) the ad hoc nature of exploring vast socioeconomic uncertainties with only a small number of scenarios; (2) the conventional representation of alternative scenario typologies as "parallel universes• or "diverging universes•, which provide little insight on …
Global Sensitivity Analysis Of Key Parameters In A Process-Based Sugarcane Growth Model - A Bayesian Approach,
2014
James Cook University
Global Sensitivity Analysis Of Key Parameters In A Process-Based Sugarcane Growth Model - A Bayesian Approach, Justin Sexton, Yvette Everingham
International Congress on Environmental Modelling and Software
While several statistical methods are available to analyse model sensitivity, their application to complex process-based models is often impractical due to the large number of simulation runs required. A Bayesian approach to global sensitivity analysis can greatly reduce the number of simulation runs required by building an emulator of the model which is less computationally demanding. A Gaussian Emulation Machine (GEM) was used to efficiently assess the sensitivity of key agronomic outputs from the APSIM-Sugar crop model to influential input parameters. The sensitivity of simulated biomass and sucrose at harvest was assessed on 14 parameters representing varietal differences and growth …
Hypothesis Testing For Management: Evolving And Answering Closed Questions Using Multiobjective Visualization,
2014
University of Colorado Boulder
Hypothesis Testing For Management: Evolving And Answering Closed Questions Using Multiobjective Visualization, Joseph Kasprzyk, Joseph Guillaume, Joshua Kollat, Chris Danilo
International Congress on Environmental Modelling and Software
In order to use models to understand deeply uncertain future conditions, managers must be able to pose and test hypotheses about their management problems. In Iterative Closed Question Methodology (ICQM), a series of closed questions are used to structure thinking about hypotheses while looking beyond a problem's existing modeling representation. Our research is exploring how ICQM can contribute to a framework called Many Objective Robust Decision Making (MORDM), which uses multiobjective optimization and ensembles of uncertain future states of the world to create and evaluate robust solutions for environmental management. A visualization software tool; AeroVis, has greatly aided implementation of …
