Browsing by Author "Heimdahl, Mats"

Now showing 1 - 20 of 94
  • Thumbnail Image
    Item
    A Case for Requirements Validation
    (2004) Heimdahl, Mats
    In software engineering we make a distinction between the validation and the verifi- cation of a software system under development. Verification is concerned with demonstrating that the software implements the functional and non-functional requirements. Verification answers the question "is this implementation correct with respect to its requirements?" Validation, on the other hand, is concerned with determining if the functional and non-functional requirements are the right requirements. Validation answers the question "will this system, if build correctly, be safe and effective for its intended use?" There is ample evidence that most safety problems can be traced to erroneous and inadequate requirements. Therefore, to improve the safety of software intensive systems it is critical that the requirements are properly validated. Unfortunately, current certication standards, for example, DO-178B, focus almost exclusively on various verication activities; consequently, most industry practices are geared towards verification activities such as extensive testing and code inspections. Thus, one of the most critical problems with current certification standards is a lack of robust and reliable ways of assessing whether the requirements have been adequately validated.
  • Thumbnail Image
    Item
    A Proposal for Model-Based Safety Analysis
    (2005) Joshi, Anjali; Miller, Steven; Whalen, Michael; Heimdahl, Mats
    System safety analysis techniques are well es-tablished and are used extensively during the design of safety-critical systems. Despite this, most of the techniques are highly subjective and dependent on the skill of the practitioner. Since these analyses are usually based on an informal system model, it is unlikely that they will be complete, consistent, and error free. In fact, the lack of precise models of the system architecture and its failure modes often forces the safety analysts to devote much of their effort to finding undocumented details of the sys-tem behavior and embedding this information in the safety artifacts such as the fault trees. In this paper we propose an approach, Model-Based Safety Analysis, in which the system and safety engineers use the same system models cre-ated during a model-based development process. By extending the system model with a fault model as well as relevant portions of the physical system to be controlled, automated support can be provided for much of the safety analysis. We believe that by using a common model for both system and safety engineering and automating parts of the safety analysis, we can both reduce the cost and improve the quality of the safety analysis. Here we present our vision of model-based safety analysis and dis-cuss the advantages and challenges in making this approach practical.
  • Thumbnail Image
    Item
    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.
  • Thumbnail Image
    Item
    An Approach to Automatic Code Generation for Safety-Critical Systems
    (1999) Whalen, Michael; Heimdahl, Mats
    Although formal requirements specifications can provide rigorous and unambiguous description of a safety-critical software system, designing and developing production quality code from high-level specifications can be a time-consuming and error-prone process. Automated translation, or code generation, of the specification to production code can alleviate many of the problems associated with design and implementation. In this report we outline the requirements of such code generation to obtain a high level of confidence in the correctness of the translation process. We then describe a translator for a state-based modeling language called RSML that largely meets these requirements. The process is based on the denotational semantics of both RSML and a simplified imperative target language (SIMPL), which are used to prove that the translator correctly implements the RSML semantics in SIMPL. The SIMPL code can then trivially be translated to any popular imperative language. The translation process also provides for informal arguments of the correctness of the code and traceability information.
  • Thumbnail Image
    Item
    An Integrated Development Environment Prototyping Safety Critical Systems
    (1999) Thompson, Jeffrey; Heimdahl, Mats
  • Thumbnail Image
    Item
    Architecture Modeling and Analysis for Safety Engineering
    (Springer, 2017) Stewart, Danielle; Whalen, Michael; Cofer, Darren; Heimdahl, Mats
    Architecture description languages such as AADL allow systems engineers to specify the structure of system architectures and perform several analyses over them, including schedulability, resource analysis, and information flow. In addition, they permit system-level requirements to be specified and analyzed early in the development process of airborne and ground-based systems. These tools can also be used to perform safety analysis based on the system architecture and initial functional decomposition. Using AADL-based system architecture modeling and analysis tools as an exemplar, we extend existing analysis methods to support system safety objectives of ARP4754A and ARP4761. This includes extensions to existing modeling languages to better describe failure conditions, interactions, and mitigations, and improvements to compositional reasoning approaches focused on the specific needs of system safety analysis. We develop example systems based on the Wheel Braking System in SAE AIR6110 to evaluate the effectiveness and practicality of our approach.
  • Thumbnail Image
    Item
    Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites
    (Springer, 2015) Murugesan, Anitha; Whalen, Michael; Rungta, Neha; Tkachuk, Oksana; Person, Suzette; Heimdahl, Mats; You, Dongjiang
    Structural coverage metrics have traditionally categorized code as either covered or uncovered. Recent work presents a stronger notion of coverage, checked coverage, which counts only statements whose execution contributes to an outcome checked by an oracle. While this notion of coverage addresses the adequacy of the oracle, for Model-Based Development of safety critical systems, it is still not enough; we are also interested in how much of the oracle is covered, and whether the values of program variables are masked when the oracle is evaluated. Such information can help system engineers identify missing requirements as well as missing test cases. In this work, we combine results from checked coverage with results from requirements coverage to help provide insight to engineers as to whether the requirements or the test suite need to be improved. We implement a dynamic backward slicing technique and evaluate it on several systems developed in Simulink. The results of our preliminary study show that even for systems with comprehensive test suites and good sets of requirements, our approach can identify cases where more tests or more requirements are needed to improve coverage numbers.
  • Thumbnail Image
    Item
    Assessing Requirements Quality Through Requirements Coverage
    (2008) Rajan, Ajitha; Heimdahl, Mats; Woodham, Kurt
  • Thumbnail Image
    Item
    Automated Oracle Creation Support, or: How I Learned to Stop Worrying About Fault Propagation and Love Mutation Testing
    (IEEE Press, 2012) Staats, Matt; Gay, Gregory; Heimdahl, Mats
    In testing, the test oracle is the artifact that determines whether an application under test executes correctly. The choice of test oracle can significantly impact the effectiveness of the testing process. However, despite the prevalence of tools that support the selection of test inputs, little work exists for supporting oracle creation. In this work, we propose a method of supporting test oracle creation. This method automatically selects the oracle data - the set of variables monitored during testing - for expected value test oracles. This approach is based on the use of mutation analysis to rank variables in terms of fault-finding effectiveness, thus automating the selection of the oracle data. Experiments over four industrial examples demonstrate that our method may be a cost-effective approach for producing small, effective oracle data, with fault finding improvements over current industrial best practice of up to 145.8% observed.
  • Thumbnail Image
    Item
    Automated Oracle Data Selection Support
    (IEEE, 2015-06) Gay, Gregory; Staats, Matt; Whalen, Michael; Heimdahl, Mats
    The choice of test oracle—the artifact that determines whether an application under test executes correctly—can significantly impact the effectiveness of the testing process. However, despite the prevalence of tools that support test input selection, little work exists for supporting oracle creation. We propose a method of supporting test oracle creation that automatically selects the oracle data—the set of variables monitored during testing—for expected value test oracles. This approach is based on the use of mutation analysis to rank variables in terms of fault-finding effectiveness, thus automating the selection of the oracle data. Experimental results obtained by employing our method over six industrial systems (while varying test input types and the number of generated mutants) indicate that our method—when paired with test inputs generated either at random or to satisfy specific structural coverage criteria—may be a cost-effective approach for producing small, effective oracle data sets, with fault finding improvements over current industrial best practice of up to 1,435% observed (with typical improvements of up to 50%).
  • Thumbnail Image
    Item
    Automated Oracle Data Selection Support
    (2015-11) Gay, Gregory; Staats, Matt; Whalen, Michael; Heimdahl, Mats
    The choice of test oracle—the artifact that determines whether an application under test executes correctly—can significantly impact the effectiveness of the testing process. However, despite the prevalence of tools that support test input selection, little work exists for supporting oracle creation. We propose a method of supporting test oracle creation that automatically selects the oracle data—the set of variables monitored during testing—for expected value test oracles. This approach is based on the use of mutation analysis to rank variables in terms of fault-finding effectiveness, thus automating the selection of the oracle data. Experimental results obtained by employing our method over six industrial systems (while varying test input types and the number of generated mutants) indicate that our method—when paired with test inputs generated either at random or to satisfy specific structural coverage criteria—may be a cost-effective approach for producing small, effective oracle data sets, with fault finding improvements over current industrial best practice of up to 1,435% observed (with typical improvements of up to 50%).
  • Thumbnail Image
    Item
    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.
  • Thumbnail Image
    Item
    Behavioral Fault Modeling for Model-based Safety Analysis
    (2007) Joshi, Anjali; Heimdahl, Mats
    Recent work in the area of Model-based Safety Analysis has demonstrated key advantages of this methodology over traditional approaches, for example, the capability of automatic generation of safety artifacts. Since safety analysis requires knowledge of the component faults and failure modes, one also needs to formalize and incorporate the system fault behavior into the nominal system model. Fault behaviors typically tend to be quite varied and complex, and incorporating them directly into the nominal system model can clutter it severely. This manual process is error-prone and also makes model evolution difficult. These issues can be resolved by separating the fault behavior from the nominal system model in the form of a "fault model", and providing a mechanism for automatically combining the two for analysis. Towards implementing this approach we identify key requirements for a flexible behavioral fault modeling notation. We formalize it as a domain-specific language based on Lustre, a textual synchronous dataflow language. The fault modeling extensions are designed to be amenable for automatic composition into the nominal system model.
  • Thumbnail Image
    Item
    Community-Assisted Software Engineering Decision Making
    (2013-04-15) Gay, Gregory; Heimdahl, Mats
    There are a class of problems - such as deciding on a series of development practices - that challenge AI approaches for two reasons: (1) well-defined data is necessary, but it is not clear which factors are important and (2) multiple recommendations must be made, and dependence must be considered. Recommender systems offer inspiration for addressing these problems. First, they can make use of data models that broadly pair a series of recommendations with generalized information like project descriptions and design documents. More importantly, they offer feedback mechanisms to refine the calculated recommendations. Detailed feedback could be factored back into the data model to, over time, build evidence and context for recommendations. Existing algorithms and data models would be amenable to the addition of feedback mechanisms, and the use of these dynamic models could lower start-up costs and generate more accurate results as the model grows. We believe that feedback-driven dynamic prediction models will become an exciting research topic in the field of AI-based software engineering.
  • Thumbnail Image
    Item
    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.
  • Thumbnail Image
    Item
    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.
  • Thumbnail Image
    Item
    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.
  • Thumbnail Image
    Item
    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.
  • Thumbnail Image
    Item
    Coverage Metrics for Requirements-Based Testing
    (ACM, 2006) Whalen, Michael; Rajan, Ajitha; Heimdahl, Mats
    In black-box testing, one is interested in creating a suite of tests from requirements that adequately exercise the behavior of a software system without regard to the internal structure of the implementation. In current practice, the adequacy of black box test suites is inferred by examining coverage on an executable artifact, either source code or a software model. In this paper, we define structural coverage metrics directly on high-level formal software requirements. These metrics provide objective, implementation-independent measures of how well a black-box test suite exercises a set of requirements. We focus on structural coverage criteria on requirements formalized as LTL properties and discuss how they can be adapted to measure finite test cases. These criteria can also be used to automatically generate a requirements-based test suite. Unlike model or code-derived test cases, these tests are immediately traceable to high-level requirements. To assess the practicality of our approach, we apply it on a realistic example from the avionics domain.
  • Thumbnail Image
    Item
    Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness
    (NASA, 2010) Staats, Matt; Whalen, Michael; Rajan, Ajitha; Heimdahl, Mats
    In black-box testing, the tester creates a set of tests to exercise a system under test without regard to the internal structure of the system. Generally, no objective metric is used to measure the adequacy of black-box tests. In recent work, we have proposed three requirements coverage metrics, allowing testers to objectively measure the adequacy of a black-box test suite with respect to a set of requirements formalized as Linear Temporal Logic (LTL) properties. In this report, we evaluate the effectiveness of these coverage metrics with respect to fault finding. Specifically, we conduct an empirical study to investigate two questions: (1) do test suites satisfying a requirements coverage metric provide better fault finding than randomly generated test suites of approximately the same size?, and (2) do test suites satisfying a more rigorous requirements coverage metric provide better fault finding than test suites satisfying a less rigorous requirements coverage metric? Our results indicate (1) that test suites satisfying more rigorous coverage metrics provide better fault finding than test suites satisfying less rigorous coverage metrics and (2) only one coverage metric proposed—Unique First Cause (UFC) coverage—is sufficiently rigorous to ensure test suites satisfying the metric outperform randomly generated test suites of similar size.