Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Author "Lee, Insup"

Now showing 1 - 5 of 5
  • Thumbnail Image
    Item
    Exploring the Twin Peaks using Probabilistic Verification Techniques
    (2014) Murugesan, Anitha; Feng, Lu; Heimdahl, Mats; Rayadurgam, Sanjai; Whalen, Michael; Lee, Insup
    System requirements and system architecture/design co-evolve as the understanding of both the problem at hand as well as the solution to be deployed evolve---the Twin Peaks concept. Modeling of requirements and solution is a promising approach for exploring the Twin Peaks. Commonly, such models are deterministic because of the choice of modeling notation and available analysis tools. Unfortunately, most systems operate in an uncertain environment and contain physical components whose behaviors are stochastic. Although much can be learned from modeling and analysis with commonly used tools, e.g., Simulink/Stateflow and the Simulink Design Verifier, the SCADE toolset, etc., the results from the exploration of the Twin Peaks will---by necessity---be inaccurate and can be misleading; inclusion of the probabilistic behavior of the physical world provides crucial additional insight into the system's required behavior, its operational environment, and the solution proposed for its software. Here, we share our initial experiences with model-based deterministic and probabilistic verification approaches while exploring the Twin Peaks. The intent of this paper is to demonstrate how probabilistic reasoning helps illuminate weaknesses in system requirements, environmental assumptions, and the intended software solution, that could not be identified when using deterministic techniques. We illustrate our experience through a medical device subsystem, modeled and analyzed using the Simulink/Stateflow (deterministic) and PRISM (probabilistic) tools.
  • Thumbnail Image
    Item
    From Requirements to Code: Model Based Development of A Medical Cyber Physical System?
    (2014) Murugesan, Anitha; Heimdahl, Mats; Whalen, Michael; Rayadurgam, Sanjai; Komp, John; Duan, Lian; Kim, Baek-Gyu; Sokolsky, Oleg; Lee, Insup
    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 eort 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 model-based approach to medical device software development along with the artifacts created in the process. While outlining the approach, we also describe our experiences, challenges, and lessons learned in the process of formulating and analyzing the requirements, modeling the system, formally verifying the models, generating code, and executing the generated code in the hardware for generic patient controlled analgesic infusion pump (GPCA). We believe that the development artifacts and techniques presented in this paper could serve as a generic reference to be used by researchers, practitioners, and authorities while developing and evaluating cyber physical medical devices.
  • Thumbnail Image
    Item
    Hierarchical Multi-Formalism Proofs of Cyber-Physical Systems
    (University of Minnesota, 2015) Whalen, Michael; Rayadurgam, Sanjai; Ghassabani, Elaheh; Murugesan, Anitha; Sokolsky, Oleg; Heimdahl, Mats; Lee, Insup
    To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. High-level analysis explores interactions of the system with its physical environment, while embedded software is developed separately based on derived requirements. This separation of lowlevel and high-level analysis also gives hope to scalability, because we are able to use tools that are appropriate for each level. When attempting to perform compositional reasoning in such an environment, care must be taken to ensure that results from one tool can be used in another to avoid errors due to “mismatches� in the semantics of the underlying formalisms. This paper proposes a formal approach for linking high-level continuous time models and lower-level discrete time models. Specifically, we lift a discrete-time controller specified using synchronous observer properties into continuous time for proof using timed automata (UPPAAL). To define semantic compatibility between the models, we propose a direct semantics for a network of timed automata with a discrete-time component called Contract- Extended Network of Timed Automata (CENTA) and examine semantic issues involving timing and events with the combination. We then propose a translation of the discrete-time controller into a timed automata state machine and show the equivalence of the translation with the CENTA formulation. We demonstrate the usefulness of the approach by proving that a complex medical infusion pump controller is safe with respect to a continuous time clinical scenario.
  • Thumbnail Image
    Item
    Reasoning about Confidence and Uncertainty in Assurance Cases: A Survey
    (2014) Duan, Lian; Rayadurgam, Sanjai; Heimdahl, Mats; Ayoub, Anaheed; Sokolsky, Oleg; Lee, Insup
    Assurance cases are structured logical arguments supported by evidence that explain how systems, possibly software systems, satisfy desirable properties for safety, security or reliability. The confidence in both the logical reasoning and the underlying evidence is a factor that must be considered carefully when evaluating an assurance case; the developers must have confidence in their case before the system is delivered and the assurance case reviewer, such as a regulatory body, must have adequate confidence in the case before approving the system for use. A necessary aspect of gaining confidence in the assurance case is dealing with uncertainty, which may have several sources. Uncertainty, often impossible to eliminate, nevertheless undermines confidence and must therefore be sufficiently bounded. It can be broadly classified into two types, aleatory (statistical) and epistemic (systematic). This paper surveys how researchers have reasoned about uncertainty in assurance cases. We analyze existing literature to identify the type of uncertainty addressed and distinguish between qualitative and quantitative approaches for dealing with uncertainty.
  • Thumbnail Image
    Item
    Representation of Confidence in Assurance Case Evidence
    (2015) Duan, Lian; Rayadurgam, Sanjai; Heimdahl, Mats; Sokolsky, Oleg; Lee, Insup
    When evaluating assurance cases, being able to capture the confidence one has in the individual evidence nodes is crucial, as these values form the foundation for determining the confidence one has in the assurance case as a whole. Human opinions are subjective, oftentimes with uncertainty---it is difficult to capture an opinion with a single probability value. Thus, we believe that a distribution best captures a human opinion such as confidence. Previous work used a doubly-truncated normal distribution or a Dempster-Shafer theory-based belief mass to represent confidence in the evidence nodes, but we argue that a beta distribution is more appropriate. The beta distribution models a variety of shapes and we believe it provides an intuitive way to represent confidence. Furthermore, there exists a duality between the beta distribution and subjective logic, which can be exploited to simplify mathematical calculations. This paper is the first to apply this duality to assurance cases.