Download Novel Enny Arrow Pdf 44
Vivien
[RHO12]
Clinical Decision Support for Integrated Cyber-Physical Systems: A Mixed Methods Approach
Alex Roederer, Andrew Hicks, Enny Oyeniran, Insup Lee and Soojin Park
We describe the design and implementation of a clinical decision support system for assessing risk of cerebral vasospasm in patients who have been treated for aneurysmal subarachnoid hemorrhage. We illustrate the need for such clinical decision support systems in the intensive care environment, and propose a three pronged approach to constructing them, which we believe presents a balanced approach to patient modeling. We illustrate the data collection process, choice and development of models, system architecture, and methodology for user interface design. We close with a description of future work, a proposed evaluation mechanism, and a description of the demo to be presented.
[WJL09]
Formally Verifiable Networking
Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu
This paper proposes Formally Verifiable Networking (FVN), a novel approach towards unifying the design, specification, implementation, and verification of networking protocols within a logic-based framework. In FVN, formal logical statements are used to specify the behavior and the properties of the protocol. FVN uses declarative networking as an intermediary layer between high-level logical specifications of the network model and low-level implementations. A theorem prover is used to statically verify the properties of declarative network protocols. Moreover, a property preserving translation exists for generating declarative networking implementations from verified formal specifications. We further demonstrate the possibility of designing and specifying well-behaved network protocols with correctness guarantees in FVN using meta-models in a systematic and compositional way.
[WLL09]
A Theorem Proving Approach towards Declarative Networking
Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky, and Prithwish Basu
We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative networking, a recent innovation that enables network protocols to be concisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, network designer can supply a component-based model of their routing design, automatically generate PVS specifications for verification and subsequent compilation into veriffied declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying a variety of well-known network routing protocols.
[KPL12]
A Model-Based I/O Interface Synthesis Framework for the Cross-Platform Software Modeling
BaekGyu Kim, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky
In model-based development, executable software (e.g., C or Java code) can be generated from a high-level model using a code generator. However, the execution of the generated software on a target platform remains a challenge due to a mismatch in communication semantics assumed by the model and the platform-dependent software (e.g., sampling/actuation routines). This paper proposes an input/output (I/O) interface module that bridges this semantic gap by means of buffers and interface policies, which explicitly capture the information required to adapt the models communication semantics to that of the platform. We present a framework that can be used to systematically synthesize directly from the model the I/O interfaces and accompanying APIs that the generated software and the platform-dependent software need to communicate with one another. Our interface policies can also encode relaxations of a model semantics that may not be implementable, thus making derivations of the implemented systems from the model traceable. We illustrate the applicability and the benefits of our framework with a case study of an infusion pump.
[ZSL09]
DMaC: Distributed Monitoring and Checking
Wenchao Zhou, Oleg Sokolsky, Boon Thau Loo, and Insup Lee
We consider monitoring and checking formally specified properties in a network. We are addressing the problem of deploying the checkers on different network nodes that provide correct and efficient checking. We present the DMaC system that builds upon two bodies of work: the Monitoring and Checking (MaC) framework, which provides means to monitor and check running systems against formally specified requirements, and declarative networking, a declarative domain-specific approach for specifying and implementing distributed network protocols. DMaC uses a declarative networking system for both specifying network protocols and performing checker execution. High-level properties are automatically translated from safety property specifications in the MaC framework into declarative networking queries and integrated into the rest of the network for monitoring the safety properties. We evaluate the flexibility and efficiency of DMaC using simple but realistic network protocols and their properties.
[WAS11]
Runtime Verification of Traces under Recording Uncertainty
Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky, and Insup Lee
We present an on-line algorithm for the runtime checking of temporal properties, expressed as past-time Linear Temporal Logic (LTL) over the traces of observations recorded by a "black box"-like device. The recorder captures the observed values but not the precise time of their occurrences, and precise truth evaluation of a temporal logic formula cannot always be obtained. In order to handle this uncertainty, the checking algorithm is based on a three-valued semantics for pasttime LTL defined in this paper. In addition to the algorithm, the paper presents results of an evaluation that aimed to study the effects of the recording uncertainty on different kinds of temporal logic properties.
[PMS13]
Model-Driven Safety Analysis of Closed-Loop Medical Systems
Miroslav Pajic, Rahul Mangharam, Oleg Sokolsky, David Arney, Julian M. Goldman, and Insup Lee
In modern hospitals, patients are treated using a wide array of medical devices that are increasingly interacting with each other over the network, thus offering a perfect example of a cyber-physical system. We study the safety of a medical device system for the physiologic closed-loop control of drug infusion. The main contribution of the paper is the verification approach for the safety properties of closed-loop medical device systems. We demonstrate, using a case study, that the approach can be applied to a system of clinical importance. Our method combines simulation-based analysis of a detailed model of the system that contains continuous patient dynamics with model checking of a more abstract timed automata model. We show that the relationship between the two models preserves the crucial aspect of the timing behavior that ensures the conservativeness of the safety analysis. We also describe system design that can provide open-loop safety under network failure.
[CBC12]
Extending Task-level to Job-level Fixed Priority Assignment and Schedulability Analysis Using Pseudo-deadlines
Hoon Sung Chwa, Hyoungbu Back, Sanjian Chen, Jinkyu Lee, Arvind Easwaran, Insik Shin and Insup Lee
In global real-time multiprocessor scheduling, arecent analysis technique for Task-level Fixed-Priority (TFP)scheduling has been shown to outperform many of the analysesfor Job-level Fixed-Priority (JFP) scheduling on average. SinceJFP is a generalization of TFP scheduling, and the TFP analysistechnique itself has been adapted from an earlier JFP analysis,this result is counter-intuitive and in our opinion highlights thelack of good JFP scheduling techniques. Towards generalizingthe superior TFP analysis to JFP scheduling, we proposethe Smallest Pseudo-Deadline First (SPDF) JFP schedulingalgorithm. SPDF uses a simple task-level parameter calledpseudo-deadline to prioritize jobs, and hence can behave as aTFP or JFP scheduler depending on the values of the pseudodeadlines.This natural transition from TFP to JFP schedulinghas enabled us to incorporate the superior TFP analysistechnique in an SPDF schedulability test. We also present apseudo-deadline assignment algorithm for SPDF schedulingthat extends the well-known Optimal Priority Assignment(OPA) algorithm for TFP scheduling. We show that ouralgorithm is optimal for the derived schedulability test, and alsopresent a heuristic to overcome the computational complexityissue of the optimal algorithm. Our simulation results showthat the SPDF algorithm with the new analysis significantlyoutperforms state-of-the-art TFP and JFP analysis.
[KFS12]
Evaluation of a Smart Alarm for Intensive Care using Clinical Data
Andrew King, Kelsea Fortino, Nicholas Stevens, Sachin Shah, Margaret Fortino-Mullen and Insup Lee
We describe and report the results of an evaluation of a smart alarm algorithm for post coronary artery bypass graft (CABG) patients. The algorithm (CABG-SA) was applied to vital sign data streams recorded in a surgical intensive care unit (SICU) at a hospital in the University of Pennsylvania Health System. In order to determine the specificity of CABGSA, the alarms generated by CABG-SA were compared against the actual interventions performed by the staff of the critical care unit. Overall, CABG-SA alarmed for 55% of the time relative to traditional alarms while still generating alarms for 12 of the 13 recorded interventions.