Several test adequacy criteria have been developed for quantifying the the coverage of deep neural networks (DNNs) achieved by a test suite. Being dependent on the structure of the DNN, these can be costly to measure and use, especially given the highly iterative nature of the model training workflow. Further, testing provides higher overall assurance when such implementation dependent measures are used along with implementation independent ones. In this paper, we rigorously define a new black-box coverage criterion that is independent of the DNN model under test. We further describe a few desirable properties and associated evaluation metrics for assessing test coverage criteria and use those to empirically compare and contrast the black-box criterion with several DNN structural coverage criteria. Results indicate that the black-box criterion has comparable effectiveness and provides benefits that complement white-box criteria. The results also reveal a few weaknesses of coverage criteria for DNNs.

Using third-party executable components to build control systems poses challenges for verification. This is because the informal behavior descriptions that typically accompany the components often fall short of the needed rigor. Consequently, there is a need to formalize a component contract that is strong enough to help establish system properties and also weak enough to account for all potential component behaviors in the system’s context. In this paper, we present a novel approach that allows an analyst to hypothesize a component contract, explore if the component meets the contract, and, if not, have automated support to help repair the contract. Preliminary results show that, in more than 32% of the cases, the repaired contract is logically equivalent to a developer-written one; in a further 63% of cases, it is a distinct, valid, and non-trivial property of the component.

Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification, while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed framework unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.

Reference models such as Parnas' four-variable model, Jackson's and Zaves' world machine model, and Gunther et al.'s WRSPM model abstractly define and relate key artifacts in requirements engineering. Such reference models are intended to serve as a frame of reference for engineers to understand and reason about the artifacts involved in requirements engineering. However, when discussing the requirements of modern systems that are developed in a hierarchical and middle-out manner, these reference models do not provide a framework in which the relationship between requirements and architecture is explicitly discussed. Conceptual clarity about this relationship is crucial since the architecture and requirements for such systems become intrinsically intertwined as the architectural choices made during development influence the requirements and vice-versa. Hence, to precisely determine the scope of specifying requirements, distinguish requirements from architecture details, reason about the requirements, and determine how the requirements are realized in the system, we argue that a requirements reference model intended as a reference for such systems must explicitly discuss the architecture - requirements relationship. To that end, we define a hierarchical reference model that formally, yet abstractly, captures the intertwined relationship between the architecture and requirements in a way that will serve the same purpose as other models, but be more suitable for modern systems where architecture and requirements co-evolve. To illustrate the concepts in this model, we use a generic patient-controlled analgesic infusion pump system as a case example.

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.

Object-branch coverage (OBC) is often used as a measure of the thoroughness of tests suites, augmenting or substituting source-code based structural criteria such as branch coverage and modified condition/decision coverage (MC/DC). In addition, with the increasing use of third-party components for which source-code access may be unavailable, robust object-code coverage criteria are essential to assess how well the components are exercised during testing. While OBC has the advantage of being programming language independent and is amenable to non-intrusive coverage measurement techniques, variations in compilers and the optimizations they perform can substantially change the structure of the generated code and the instructions used to represent branches. To address the need for a robust object coverage criterion, this paper proposes a rigorous definition of OBC such that it captures well the semantics of source code branches for a given instruction set architecture. We report an empirical assessment of these criteria for the Intel x86 instruction set on several examples from embedded control systems software. Preliminary results indicate that object-code coverage can be made robust to compilation variations and is comparable in its bug-finding efficacy to source level MC/DC.

The test 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 test 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 test 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 the differences in behavior that are acceptable) and is based on a search process attempting to minimize a dissimilarity metric. This framework allows non-deterministic, but bounded, behavioral 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, testing and debugging costs while improving the quality of the testing process.

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.

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.

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.

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 low-level 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.

Model-based development (MBD) tool suites such as Simulink and Stateflow offer powerful tools for design, development, and analysis of models. These models can be used for several purposes: for code generation, for prototyping, as descriptions of an environment (plant) that will be controlled by software, as oracles for a testing process, and many other aspects of software development. In addition, a goal of model-based development is to develop reusable models that can be easily managed in a version-controlled continuous integration process.

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.

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.

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.

Verification and Validation (V&V) of software for critical embedded control systems often consumes upto 70% of the development resources. Testing is one of the most frequently used V&V technique for verifying such systems. Many regulatory agencies that certify control systems for use require that the software be tested to certain specified levels of coverage. Currently, developing test cases to meet these requirements takes a major portion of the resources. Automating this task would result in significant time and cost savings. The objective of this paper is to automate the generation of such test cases. We propose an approach where we rely on a formal model of the required software behavior for test-case generation, as well as, an oracle to determine if the implementation produced the correct output during testing.

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.

This paper presents the agent architecture of an Internet application development tool called Distributed Interactive Web-site Builder (DIWB). Together with the component object model and a layering framework, the agent architecture can be used to build Internet applications that support individualized services. The DIWB can construct pages dynamically at runtime and can be easily customized for individual users. The architecture consists of two cooperating agents that compose pages at runtime using components and data stored in various databases (agencies). The page agent composes a page by retrieving page definition and requesting the component agent to construct individual components. The component agent retrieves user preferences, and page component definitions from the databases and returns the results to the page agent.

Many real time systems evolve over time due to new requirements and technology improvements. Each revision requires regression resting to ensure that existing functionality is not affected by such changes. Testing these systems often require specialized hardware and software, and both are expensive. While the overall regression testing process is similar across different organizations, the strategies and tools used by them vary according to their product needs. Hence a good framework for regression testing should provide the flexibility to configure it depending on the particular organization's needs while at the same time maximizing utilization. Manual processes are typically slow and error prone and result in under-utilization of valuable test resources. The paper proposes an automated distributed regression testing framework that provides flexibility to the user to configure it to their needs while at the same time optimizing resource usage.

In this interview, Takashi Sano reviews the origin and history of the year 2000 problem in Japan, and summarizes its status in Japan as of late 1996. He presents a way for software vendors to make this problem known to the software community because the problem is very serious, with far reaching impacts on an organization's economics, demand for talent and workforce scheduling. Then, he discusses the core techniques used at Fujitsu to tackle the year 2000 problem when a re-engineering approach is used. Finally, he provides an overview of a relevant software tool developed by Fujitsu. © 1997 John Wiley & Sons, Ltd.

Proposes several new object-oriented (OO) software-specific techniques that are useful in the maintenance of OO software, especially C++ programs. The proposed techniques include: (1) new OO-specific dependence relations (such as class, message and declaration dependence); (2) algorithms to construct a hierarchical C++ dependence graph (C++DG) to capture these dependences from the source code; (3) several new slicing techniques (such as class, message, constrained and recursive slicing), besides the existing slicing techniques (such as program, variable and condition slicing) for OO programs. Next, the paper discusses the application of the dependence and slicing concepts to other maintenance activities such as ripple effect analysis (REA) and regression testing. Finally, the paper presents the design of an integrated environment, Omega, that implements many of these techniques for C++ program maintenance. Omega has been demonstrated in various industrial sites in the USA and Japan since May 1995.