Browsing by Author "Rayadurgam, Sanjai"

Now showing 1 - 20 of 31

A Reference Model for Simulating Agile Processes
(ACM, 2015) De Silva, Ian; Rayadurgam, Sanjai; Heimdahl, Mats
Agile development processes are popular when attempting to respond to changing requirements in a controlled manner; however, selecting an ill-suited process may increase project costs and risk. Before adopting a seemingly promising agile approach, we desire to evaluate the approach's applicability in the context of the specific product, organization, and staff. Simulation provides a means to do this. However, in order to simulate agile processes we require both the ability to model individual behavior as well as the decoupling of the process and product. To our knowledge, no existing simulator nor underlying simulation model provide a means to do this. To address this gap, we introduce a process simulation reference model that provides the constructs and relationships for capturing the interactions among the individuals, product, process, and project in a holistic fashion---a necessary first step towards an agile-process evaluation environment.
Automatic Abstraction for Model Checking Software Systems with Interrelated Numeric Constraints
(2001) Choi, Yunja; Rayadurgam, Sanjai; Heimdahl, Mats
Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. Various model abstraction techniques have been proposed to address this problem. In this paper, we wish to propose domain abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition system. Our technique is automatable with some minor restrictions.
Compositional Verification of a Medical Device System
(ACM, 2013) Murugesan, Anitha; Whalen, Michael; Rayadurgam, Sanjai; Heimdahl, Mats
Complex systems are by necessity hierarchically organized; they are decomposed into subsystems for intellectual control as well as the ability to have the subsystems created by several distinct teams. This decomposition affects both requirements and architecture; the architecture describes the structure and this affects how requirements are ``flowed down'' to each subsystem, and discoveries in the design process may affect the requirements. Demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem. In this paper, we present a medical device case example where we apply an iterative approach to architecture and verification based on software architectural models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe the requirements at different levels of abstraction for compositional verification. The component-level behavior for the model is described in Simulink/Stateflow. We assemble proofs of system level properties by using the Simulink Design Verifier to establish component-level properties and an open-source plug-in for the OSATE AADL environment to perform the compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design, verification, and detailed behavioral models, and to scale formal analysis to large software systems.
Contract discovery from black-box components
(2018) Sharma, Vaibhav; Byun, Taejoon; McCamant, Stephen; Rayadurgam, Sanjai; Heimdahl, Mats
Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior -- its contract -- is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.
Coverage Based Test-Case Generation using Model Checkers
(2001) Rayadurgam, Sanjai; Heimdahl, Mats
This paper presents a method for automatically generating test cases to structural coverage criteria. We show how a model checker can be used to automatically generate complete test sequences that will provide a predefined coverage of any software development artifact that can be represented as a finite state model. Our goal is to help reduce the high cost of developing test cases for safety-critical software applications that require a certain level of coverage for certification, for example, safety-critical avionics systems that need to demonstrate MC/DC (modified condition and decision) coverage of the code. We define a formal framework suitable for modeling software artifacts, like, requirements models, software specifications, or implementations. We then show how various structural coverage criteria can be formalized and used to make a model checker provide test sequences to achieve this coverage. To illustrate our approach, we demonstrate, for the first time, how a model checker can be used to generate test sequences for MC/DC coverage of a small case example.
Coverage Based Test-Data Generation using Model Checkers
(2001-01-26) Rayadurgam, Sanjai; Heimdahl, Mats
We present a method for automatically generating test cases that satisfy certain structural coverage criteria. We show how a model checker can be used to automatically generate complete test sequences that provide a predefined coverage of any software development artifact, given a finite state model of the artifact. Our goal is to help reduce the high cost of developing test cases for safety-critical software applications that require a certain level of coverage for certification, for example, safety-critical avionics systems that need to demonstrate MC/DC (modified condition and decision) coverage of the code. We define a formal framework suitable for modeling various software artifacts, for example, requirements models, software specifications, or implementations. We then demonstrate how various structural coverage criteria can be formalized and used to make a model checker provide test sequences to achieve this coverage. To illustrate our approach, we demonstrate, for the first time, how a model checker can be used to generate test sequences for MC/DC coverage of a small case example.
Cyber-Physical System Requirements - A Model Driven Approach
(2013) Murugesan, Anitha; Duan, Lian; Rayadurgam, Sanjai; Heimdahl, Mats
Systems where the physical world interacts extensively with often distributed and networked-software are referred to as Cyber-Physical Systems (CPS). Gathering and analyzing CPS requirements poses unique challenges to the requirements engineering community - a perspective that is sensitive to the scoping and interplay between the cyber, physical and behavioral aspects of the system. The major challenges were identifying and analyzing (1)requirements to address the complexity in the continuous domain, (2)requirements related to the continual behavior of the system, (3)the precise scope of the system, (4)requirements flow down during system decomposition, (5)mode logic and features interactions and, (6)system behavior during mode transitions. Unfortunately there is little guidance in the literature to systematically address these issues. We pursued a model-driven approach to overcome these challenges, which we believe is broadly applicable to CPS requirements elicitation and specification. The variety of modeling techniques we used, served as a crucial aid in the elicitation and discovery of requirements and provided an initial classification of the types of requirements and modeling patterns needed to describe crucial aspects of a CPS. We used a generic patient controlled analgesia (GPCA) infusion pump system as case example to investigate the requirements of a medical CPS and provide an archetype of system development artifacts that could serve as a generic reference standard used by CPS researchers and practitioners.
Design Considerations for Modeling Modes in Cyber-Physical Systems
(2015) Murugesan, Anitha; Rayadurgam, Sanjai; Whalen, Michael; Heimdahl, Mats
Safety critical systems such as cruise control in automotive systems and variable rate bolus in medical device infusion pumps introduce complexity and reduce the flexibility of incremental code modifications. This paper proposes a generic pattern to structure the mode logic such that additions, modifications, and removal of behaviors could be done in a quick and localized fashion without losing model integrity. The authors illustrate the proposed pattern using the infusion pump as a case study and describe a design pattern for the mode logic of reactive systems that allows for flexible, understandable, and maintainable models.
Discovering Instructions for Robust Binary-level Coverage Criteria
(2017) Sharma, Vaibhav; Byun, Taejoon; McCamant, Stephen; Rayadurgam, Sanjai; Heimdahl, Mats
Object-Branch Coverage (OBC) is often used to measure e ective- ness of test suites, when source code is unavailable. The traditional OBC de nition can be made more resilient to variations in compil- ers and the structure of generated code by creating more robust de nitions. However nding which instructions should be included in each new de nition is laborious, error-prone, and architecture- dependent. We automate the discovery of instructions to be in- cluded for an improved OBC de nition on the X86 and ARM archi- tectures. We discover all possible valid instructions by symbolically executing instruction decoders for X86 and ARM instructions. For each discovered instruction, we translate it to Vine IR, and check if the Vine IR translation satis es the OBC de nition. We verify the correctness of our tool by comparing its output with the X86 and ARM architecture manuals. Our automated instruction clas- si cation facilitates development of more robust OBC de nitions with better bug- nding ability and lesser sensitivity to compiler variations.
Domain Modeling for Development Process Simulation
(ACM, 2017) De Silva, Ian; Rayadurgam, Sanjai; Heimdahl, Mats
Simulating agile processes prior to adoption can reduce the risk of enacting an ill-fitting process. Agent-based simulation is well-suited to capture the individual decision-making valued in agile. Yet, agile's lightweight nature creates simulation difficulties as agents must fill-in gaps within the specified process. Deliberative agents can do this given a suitable planning domain model. However, no such model, nor guidance for creating one, currently exists. In this work, we propose a means for constructing an agile planning domain model suitable for agent-based simulation. As such, the domain model must ensure that all activity sequences derived from the model are executable by a software agent. We prescribe iterative elaboration and decomposition of an existing process to generate successive internally-complete and -consistent domain models, thereby ensuring plans derived from the model are valid. We then demonstrate how to generate a domain model and exemplify its use in planning the actions of a single agent.
Domain Reduction Abstraction
(2002-04-03) Choi, Yunja; Heimdahl, Mats; Rayadurgam, Sanjai
We suggest "domain reduction abstraction" for model checking systems with numeric guarding conditions and data transition constraints. The technique abstracts the domain of data variables using "data equivalence" and "trajectory reduction" in order to reduce the (possibly infinite) state space. Earlier work introduced the technique for systems with no data constraints or deterministic data constraints. Here, we extend the work to "non-deterministic constrained data transition systems". We provide a formal definition andproof of the soundness of the technique, and illustrate the abstraction technique with a small example.
Efficient Observability-based Test Generation by Dynamic Symbolic Execution
(IEEE, 2015) You, Dongjiang; Rayadurgam, Sanjai; Whalen, Michael; Heimdahl, Mats; Gay, Gregory
Structural coverage metrics have been widely used to measure test suite adequacy as well as to generate test cases. In previous investigations, we have found that the fault-finding effectiveness of tests satisfying structural coverage criteria is highly dependent on program syntax â€“ even if the faulty code is exercised, its effect may not be observable at the output. To address these problems, observability-based coverage metrics have been defined. Specifically, Observable MC/DC (OMC/DC) is a criterion that appears to be both more effective at detecting faults and more robust to program restructuring than MC/DC. Traditional counterexample-based test generation for OMC/DC, however, can be infeasible on large systems. In this study, we propose an incremental test generation approach that combines the notion of observability with dynamic symbolic execution. We evaluated the efficiency and effectiveness of our approach using seven systems from the avionics and medical device domains. Our results show that the incremental approach requires much lower generation time, while achieving even higher fault finding effectiveness compared with regular OMC/DC generation.
Executing Model-based Tests on Platform-specific Implementations
(IEEE, 2015) You, Dongjiang; Rayadurgam, Sanjai; Heimdahl, Mats; Komp, John; Kim, Baek-Gyu; Sokolsky, Oleg
Model-based testing of embedded real-time systems is challenging because platform-specific details are often abstracted away to make the models amenable to various analyses. Testing an implementation to expose non-conformance to such a model requires reconciling differences arising from these abstractions. Due to stateful behavior, naive comparisons of model and system behaviors often fail causing numerous false positives. Previously proposed approaches address this by being reactively permissive: passing criteria are relaxed to reduce false positives, but may increase false negatives, which is particularly bothersome for safety-critical systems. To address this concern, we propose an automated approach that is proactively adaptive: test stimuli and system responses are suitably modified taking into account platform-specific aspects so that the modified test when executed on the platform-specific implementation exercises the intended scenario captured in the original model-based test. We show that the new framework eliminates false negatives while keeping the number of false positives low for a variety of platform-specific configurations.
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.
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.
Generating MC/DC Adequate Test Sequences Through Model Checking
(2003) Rayadurgam, Sanjai; Heimdahl, Mats
We present a method for automatically generating test sequences to satisfy MC/DC like structural coverage criteria of software behavioral models specified in state-based formalisms. The use of temporal logic for characterizing test criteria and the application of model-checking techniques for generating test sequences to those criteria have been of interest in software verification research for some time. Nevertheless, criteria for which constraints span more than one test sequence, such as the Modified Condition/Decision Coverage (MC/DC) mandated for critical avionics software, cannot be characterized in terms of a single temporal property. This paper discusses a method for recasting two-sequence constraints in the original model as a single sequence constraint expressed in temporal logic on a slightly modified model. The test-sequence generated by a model-checker for the modified model can be easily separated into two different test-sequences for the original model, satisfying the given test criteria. The approach has been successful in generating MC/DC test sequences from a model of the mode-logic in a flight-guidance system.
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.
Improving the Accuracy of Oracle Verdicts Through Automated Model Steering
(2014) Gay, Gregory; Rayadurgam, Sanjai; Heimdahl, Mats
The oracle--a judge of the correctness of the system under test (SUT)--is a major component of the testing process. Specifying test oracles is challenging for some domains, such as real-time embedded systems, where small changes in timing or sensory input may cause large behavioral differences. Models of such systems, often built for analysis and simulation, are appealing for reuse as oracles. These models, however, typically represent an idealized system, abstracting away certain issues such as non-deterministic timing behavior and sensor noise. Thus, even with the same inputs, the model's behavior may fail to match an acceptable behavior of the SUT, leading to many false positives reported by the oracle. We propose an automated steering framework that can adjust the behavior of the model to better match the behavior of the SUT to reduce the rate of false positives. This model steering is limited by a set of constraints (defining acceptable differences in behavior) and is based on a search process attempting to minimize a dissimilarity metric. This framework allows non-deterministic, but bounded, behavior differences, while preventing future mismatches, by guiding the oracle--within limits--to match the execution of the SUT. Results show that steering significantly increases SUT-oracle conformance with minimal masking of real faults and, thus, has significant potential for reducing false positives and, consequently, development costs.
Modeling and Requirements on the Physical Side of Cyber-Physical Systems
(IEEE, 2013) Heimdahl, Mats; Duan, Lian; Murugesan, Anitha; Rayadurgam, Sanjai
In a cyber-physical system (a system where the physical world interacts extensively withâ€”often networkedâ€” software), the physical portion of the system resides in the continuous and continual domain. Thus, on the physical side of cyber-physical systems we will have to contend with not only real time requirements but also the continuous and continual nature of the system. This poses a new set of challenges for requirements engineering; we must write well defined requirements to address crucial issues not commonly addressed in the software domain. For example, the rate of change of a controlled variable, the time it takes for a controlled variable to settle sufficiently close to a set-point, and the cumulative errors built up over time may be of critical importance. In this paper we outline how early modeling in the continuous domain serves as a crucial aid in the elicitation and discovery of requirements for cyber-physical systems and provide an initial classification of the types of requirements needed to describe crucial aspects of the physical side of a cyber-physical system.
Modes, Features, and State-Based Modeling for Clarity and Flexibility
(IEEE, 2013) Murugesan, Anitha; Rayadurgam, Sanjai; Heimdahl, Mats
The behavior of a complex system is frequently defined in terms of operational modesâ€”mutually exclusive sets of the system behaviors. Within the operational modes, collections of features define the behavior of the system. Lucent and understandable modeling of operational modes and features using common state-based notations such as Statecharts or Stateflow can be challenging. In this paper we share some of our experiences from modeling modes and features in the medical device domain. We discuss the challenges and present a generic approach to structuring the modes and features of a generic Patient-Controlled Analgesia infusion pump.

University Digital Conservancy

Browse by Author

Browsing by Author "Rayadurgam, Sanjai"