Thirty years ago, when the TCAS II modeling effort was undertaken, the notion of model-based design and model-based systems engineering were new concepts. The TCAS II modeling effort demonstrated that creating a formal model of a complex system and doing so in collaboration with a diverse group of application experts was eminently feasible and laid the groundwork for future research. In this retrospective, we revisit the effort in the context of model-based systems engineering, summarize the most relevant lessons learned, and discuss the state of model-based techniques today and steps to the future.

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.

Symbolic model checkers can construct proofs of properties over highly complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, measure completeness of a set of requirements over a model, and assist with design optimization given a set of requirements for an existing or synthesized implementation. In this paper, we present a comprehensive treatment of a suite of algorithms to compute inductive validity cores (IVCs), minimal sets of model elements necessary to construct inductive proofs of safety properties for sequential systems. The algorithms are based on the UNSAT core support built into current SMT solvers and novel encodings of the inductive problem to generate approximate and guaranteed minimal inductive validity cores as well as all inductive validity cores. We demonstrate that our algorithms are correct, describe their implementation in the JKind model checker for Lustre models, and present several use cases for the algorithms. We then present a substantial experiment in which we benchmark the efficiency and efficacy of the algorithms.

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.

When using formal verification on critical software, an important question involves whether we have we specified enough properties for a given implementation model. To address this question, coverage metrics for property-based formal verification have been proposed. Existing metrics are usually based on mutation, where the implementation model is repeatedly modified and re-analyzed to determine whether mutant models are "killed" by the property set. These metrics tend to be very expensive to compute, as they involve many additional verification problems. This paper proposes an alternate family of metrics that can be computed using the recently introduced idea of Inductive Validity Cores (IVCs). IVCs determine a minimal set of model elements necessary to establish a proof. One of the proposed metrics is both rigorous and substantially cheaper to compute than mutation-based metrics. In addition, unlike the mutation-based techniques, the design elements marked as necessary by the metric are guaranteed to preserve provability. We demonstrate the metrics on a large corpus of examples.

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.

Large software organizations seek internal professional staff development beyond traditional corporate training in specific technical skills (i.e., a new programming language or tool). This paper describes the results of one effort of delivery: the offering of a non-credit small, private, online course (SPOC) in software design. Participants spanned those with formal degrees in Computer Science or Software Engineering to those with no formal education in the area. After completing the course, a survey was administered. Intention to enroll in further non-credit SPOC courses was found to be more likely than intention in formal degrees in the area. Additionally, the course content was highly valued by the participants. These findings show a need for further investigation into the value and opportunity of exported education: bringing University expertise out of the traditional classroom and directly into the hands of industry professionals via corporate training-style SPOC offerings.

When establishing associations, known as tracelinks, between a requirement and the artifacts that lead to itssatisfaction, it is essential to know what the links mean. Whileresearch into this type of traceability-what we call RequirementsSatisfaction Traceability-has been an active research area forsome time, none of the literature discusses the fact that thereare often multiple ways in which a requirement can be satisfied, i.e., there are multiple satisfaction arguments. The distinctionbetween establishing a single satisfaction argument between arequirement and its implementation (tracing one way the requirement is implemented) vs. tracing all satisfaction arguments, and the possible ramifications for how the trace links can beused in analysis, has not been well studied. We examine how thisdistinction changes the way traceability is perceived, established, maintained, and used. In this RE@Next! paper, we introduce anddiscuss the notion of "complete" traceability, which considersall trace links between the requirements and the artifacts thatwork to satisfy the requirements, and contrast it with the partialtraceability common in practice.

Test adequacy metrics defined over the structure of a program, such as Modified Condition and Decision Coverage (MC/DC), are used to assess testing efforts. However, MC/DC can be “cheated” by restructuring a program to make it easier to achieve the desired coverage. This is concerning, given the importance of MC/DC in assessing the adequacy of test suites for critical systems domains. In this work, we have explored the impact of implementation structure on the efficacy of test suites satisfying the MC/DC criterion using four real-world avionics systems. Our results demonstrate that test suites achieving MC/DC over implementations with structurally complex Boolean expressions are generally larger and more effective than test suites achieving MC/DC over functionally equivalent, but structurally simpler, implementations. Additionally, we found that test suites generated over simpler implementations achieve significantly lower MC/DC and fault-finding effectiveness when applied to complex implementations, whereas test suites generated over the complex implementation still achieve high MC/DC and attain high fault finding over the simpler implementation. By measuring MC/DC over simple implementations, we can significantly reduce the cost of testing, but in doing so, we also reduce the effectiveness of the testing process. Thus, developers have an economic incentive to “cheat” the MC/DC criterion, but this cheating leads to negative consequences. Accordingly, we recommend that organizations require MC/DC over a structurally complex implementation for testing purposes to avoid these consequences.

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.

A number of structural coverage criteria have been proposed to measure the adequacy of testing efforts. In the avionics and other critical systems domains, test suites satisfying structural coverage criteria are mandated by standards. With the advent of powerful automated test generation tools, it is tempting to simply generate test inputs to satisfy these structural coverage criteria. However, while techniques to produce coverage-providing tests are well established, the effectiveness of such approaches in terms of fault detection ability has not been adequately studied. In this work, we evaluate the effectiveness of test suites generated to satisfy four coverage criteria through counterexample-based test generation and a random generation approach-where tests are randomly generated until coverage is achieved-contrasted against purely random test suites of equal size. Our results yield three key conclusions. First, coverage criteria satisfaction alone can be a poor indication of fault finding effectiveness, with inconsistent results between the seven case examples (and random test suites of equal size often providing similar-or even higher-levels of fault finding). Second, the use of structural coverage as a supplement-rather than a target-for test generation can have a positive impact, with random test suites reduced to a coverage-providing subset detecting up to 13.5 percent more faults than test suites generated specifically to achieve coverage. Finally, Observable MC/DC, a criterion designed to account for program structure and the selection of the test oracle, can-in part-address the failings of traditional structural coverage criteria, allowing for the generation of test suites achieving higher levels of fault detection than random test suites of equal size. These observations point to risks inherent in the increase in test automation in critical systems, and the need for more research in how coverage criteria, test generation approaches, the test oracle used, and system structure jointly influence test effectiveness.

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 percent observed (with typical improvements of up to 50 percent).

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.

In many critical systems domains, test suite adequacy is currently measured using structural coverage metrics over the source code. Of particular interest is the modified condition/decision coverage (MC/DC) criterion required for, e.g., critical avionics systems. In previous investigations we have found that the efficacy of such test suites is highly dependent on the structure of the program under test and the choice of variables monitored by the oracle. MC/DC adequate tests would frequently exercise faulty code, but the effects of the faults would not propagate to the monitored oracle variables. In this report, we combine the MC/DC coverage metric with a notion of observability that helps ensure that the result of a fault encountered when covering a structural obligation propagates to a monitored variable; we term this new coverage criterion Observable MC/DC (OMC/DC). We hypothesize this path requirement will make structural coverage metrics 1.) more effective at revealing faults, 2.) more robust to changes in program structure, and 3.) more robust to the choice of variables monitored. We assess the efficacy and sensitivity to program structure of OMC/DC as compared to masking MC/DC using four subsystems from the civil avionics domain and the control logic of a microwave. We have found that test suites satisfying OMC/DC are significantly more effective than test suites satisfying MC/DC, revealing up to 88% more faults, and are less sensitive to program structure and the choice of monitored variables.

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.

We are considering the challenges that regulators face in approving modern medical devices, which are software intensive and increasingly network enabled. We then consider assurance cases, which offer the means of organizing the evidence into a coherent argument demonstrating the level of assurance provided by a system, and discuss research directions that promise to make construction and evaluation of assurance cases easier and more precise. Finally, we discuss some recent trends that will further complicate the regulatory approval of medical cyber-physical systems.

In previous decades, researchers have explored the formal foundations of program testing. By exploring the foundations of testing largely separate from any specific method of testing, these researchers provided a general discussion of the testing process, including the goals, the underlying problems, and the limitations of testing. Unfortunately, a common, rigorous foundation has not been widely adopted in empirical software testing research, making it difficult to generalize and compare empirical research.

In software testing, the test oracle determines if the application under test has performed an execution correctly. In current testing practice and research, significant effort and thought is placed on selecting test inputs, with the selection of test oracles largely neglected. Here, we argue that improvements to the testing process can be made by considering the problem of oracle selection. In particular, we argue that selecting the test oracle and test inputs together to complement one another may yield improvements testing effectiveness. We illustrate this using an example and present selected results from an ongoing study demonstrating the relationship between test suite selection, oracle selection, and fault finding.

In avionics and other critical systems domains, adequacy of test suites is currently measured using the MC/DC metric on source code (or on a model in model-based development). We believe that the rigor of the MC/DC metric is highly sensitive to the structure of the implementation and can therefore be misleading as a test adequacy criterion. We investigate this hypothesis by empirically studying the effect of program structure on MC/DC coverage.

When creating test cases for software, a common approach is to create tests that exercise requirements. Determining the adequacy of test cases, however, is generally done through inspection or indirectly by measuring structural coverage of an executable artifact (such as source code or a software model). We present ReqsCov, a tool to directly measure requirements coverage provided by test cases. ReqsCov allows users to measure Linear Temporal Logic requirements coverage using three increasingly rigorous requirements coverage metrics: naive coverage, antecedent coverage, and Unique First Cause coverage. By measuring requirements coverage, users are given insight into the quality of test suites beyond what is available when solely using structural coverage metrics over an implementation.

Model-based software development is gaining interest in domains such as avionics, space, and automotives. The model serves as the central artifact for the development efforts (such as, code generation), therefore, it is crucial that the model be extensively validated. Automatic generation of interaction test suites is a candidate for partial automation of this model validation task. Interaction testing is a combinatorial approach that systematically tests all t-way combinations of inputs for a system. In this paper, we report how well interaction test suites (2-way through 5-way interaction test suites) structurally cover a model of the modelogic of a flight guidance system. We conducted experiments to (1) compare the coverage achieved with interaction test suites to that of randomly generated tests and (2) determine if interaction test suites improve the coverage of black-box test suites derived from system requirements. The experiments show that the interaction test suites provide little benefit over the randomly generated tests and do not improve coverage of the requirements-based tests. These findings raise questions on the application of interaction testing in this domain.

Model-checking techniques are successfully used in the verification of both hardware and software systems of industrial relevance. Unfortunately, the capability of current techniques is still limited and the effort required for verification can be prohibitive (if verification is possible at all). As a complement, fast, but incomplete, search tools may provide practical benefits not attainable with full verification tools, for example, reduced need for manual abstraction and fast detection of property violations during model development. In this report we investigate the performance of a simple random search technique. We conducted an experiment on a production-sized formal model of the mode-logic of a flight guidance system. Our results indicate that random search quickly finds the vast majority of property violations in our case-example. In addition, the times to detect various property violations follow an acutely right-skewed distribution and are highly biased toward the easy side. We hypothesize that the observations reported here are related to the phase transition phenomenon seen in Boolean satisfiability and other NP-complete problems. If so, these observations could be revealing some of the fundamental aspects of software (model) faults and have implications on how software engineering activities, such as analysis, testing, and reliability modeling, should be performed

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.

When using tools to automatically generate tests-suites from a specification, the selection of coverage criterion that guides the generation process is of imperative importance. In a previous study that evaluated test generation with model checking, we observed that although a coverage criterion may seem reasonable when instrumenting a model or code to measure the adequacy of a test suite, it may be unsuitable when formalized and used to guide the model checker to generate a test suite; the generated tests technically provide adequate coverage according to the formalization, but do so in a way that exercises only small portions of the system under study and finds few faults. Based on those results, we concluded that fully automated test-suite generation techniques must be pursued with great caution and that coverage criteria specifically addressing test-suite generation from formal specifications are needed. In this report, we attempt to better understand these concerns by evaluating several coverage criteria that bring together aspects from condition and control based criteria. We evaluate the fault finding capability of the criteria on a close to production flight guidance system and discuss the opportunities and challenges that arise from the increased use of fully automated model-based testing.

In model-based testing, models derived from the informal requirements (or models developed as part of the requirements process) are used to drive the testing; these models are used to generate the tests as well as serve as oracles, and the testing process can be largely automated. This move towards models, tools, and automation holds enormous promise, but it also raises new challenges that, in our experience, must be addressed before we can reap the full benefits.

As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time; a feature suitable for regression verification.

Assurance that a formal specification (system specification or software specification) possesses desired properties can be achieved through (1) manual inspections, (2) formal verification of the desired properties, or (3) simulation and testing of the specification. To achieve the high level of confidence in the correctness required in a safety-critical system, all three approaches must be used in concert. We have developed an specification language, called RSML/sup -e/, and an environment, called NIMBUS, which provides support for all these activities. The three V&V techniques fill complementary roles within the validation and verification process. Manual inspections and visualization provide the specification team, customers, and regulatory representatives the means to informally verify that the behavior described formally matches the desired "real world" behavior of the system. RSML/sup -e/ is a fully formal, synchronous, data-flow language. NIMBUS supports large-scale, distributed simulation of specifications through communications over Microsoft's distributed COM or OMG's CORBA.

We have been exploring LURCH, an approximate (not necessarily complete) alternative to traditional model checking based on a randomized search algorithm. Randomized algorithms like LURCH have been known to outperform their deterministic counterparts for search problems representing a wide range of applications. The cost of an approximate strategy is the potential for inaccuracy. If complete algorithms terminate, they find all the features they are searching for. On the other hand, by its very nature, randomized search can miss important features. Our experiments suggest that this inaccuracy problem is not too serious. In the case studies presented here and elsewhere, LURCHS random search usually found the correct results. Also, these case studies strongly suggest that LURCH can scale to much larger models than standard model checkers like NuSMV and SPIN. The two case studies presented in this paper are selected for their simplicity and their complexity. The simple problem of the dining philosophers has been widely studied. By making the dinner more crowded, we can compare the memory and runtimes of standard methods (SPIN) and LURCH. When hundreds of philosophers sit down to eat, both LURCH and SPIN can find the deadlock case. However, SPINS memory and runtime requirements can grow exponentially while LURCHS requirements stay quite low. Success with highly symmetric, automatically generated problems says little about the generality of a technique. Hence, our second example is far more complex: a real-world flight guidance system from Rockwell Collins. Compared to NuSMV, LURCH performed very well on this model. Our random search finds the vast majority of faults (close to 90%); runs much faster (seconds and minutes as opposed to hours); and uses very little memory (single digits to 10s of megabytes as opposed to 10s to 100s of megabytes). The rest of this paper is structured as follows. We begin with a theoretical rationale for why random search methods like LURCH can be incomplete, yet still successful. Next, we note that for a class of problems, the complete search of standard model checkers can be overkill. LURCH is then briefly introduced and our two case studies are presented.

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.

Inaccuracies, or deviations, in the measurements of monitored variables in a control system are facts of life that control software must accommodate $the software is expected to continue functioning correctly in the face of an expected range of deviations in the inputs. Deviation analysis can be used to determine how a software specification will behave in the face of such deviations in data from the environment. The idea is to describe the correct values of an environmental quantity; along with a range of potential deviations, and then determine the effects on the outputs of the system. The analyst can then check whether the behavior of the software is acceptable with respect to these deviations. In this report we wish to propose a new approach to deviation analysis using model checking techniques. This approach allows for more precise analysis than previous techniques, and refocuses deviation analysis from an exploratory analysis to a verification task, allowing us to investigate a different range of questions regarding a system's response to deviations.

The software product-line approach (for software product families) is one of the success stories of software reuse. When applied, it can result in cost savings and increases in productivity. In addition, in safety-critical systems the approach has the potential for reuse of analysis and testing results, which can lead to safer systems. Nevertheless, there are times when it seems like a product family approach should work when, in fact, there are difficulties in properly defining the boundaries of the product family. The authors draw on their experiences in applying the software product-line approach to a family of mobile robots as well as case studies done by others to: (1) illustrate how domain structure can currently limit applicability of product-line approaches to certain domains, and (2) demonstrate our initial progress towards a solution using a set-theoretic approach to reason about domains of what we call n-dimensional and hierarchical product families.

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.

Annotation of software artifacts is common in software development, and vital for software inspection. People viewing annotated artifacts encounter delocalization: they must understand various parts of an artifact (and their annotations) to understand the part they are viewing. We taxonomize delocalization within software systems into lateral delocalization (different items of the artifact within the same development phase), longitudinal delocalization (related items in different phases), and historical delocalization (successive versions of the same item). We report on a pilot study of code inspection with AnnoSpec, an inspection tool supporting visibility of laterally-delocalized annotations. Our results suggest that addressing delocalization may help people perform inspections more effectively.

Automated translation, or code generation, of a formal requirements model to production code can alleviate many of the problems associated with design and implementation. In this paper, 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 (Requirements Specification Modeling Language) that largely meets these requirements.

Computer-supported annotation of software systems and their documentation, including design documentation and source code, is a common and important software engineering activity. Annotated documentation is used in both formal software inspection and informal software maintenance. Viewers of annotated systems may understand the software more easily if annotations are visible not just from the annotated item itself but from other, related items. We propose a general framework for interconnecting annotatable items in software systems to achieve this visibility. We describe filtering and broadening rules that viewers can use to select the annotations they desire to see. We illustrate this framework in the context of object-oriented software system development.

Statically analyzing requirements specifications to assure that they possess desirable properties is an important activity in any rigorous software development project. The analysis is performed on an abstraction of the original requirements specification. Abstractions in the model may lead to spurious errors in the analysis output. Spurious errors are conditions that are reported as errors, but information abstracted out of the model precludes the reported conditions from being satisfied. A high ratio of spurious errors to true errors in the analysis output makes it difficult, error-prone, and time consuming to find and correct the true errors. We describe an iterative and integrative approach for analyzing state-based requirements that capitalizes on the strengths of a symbolic analysis component and a reasoning component while circumventing their weaknesses. The resulting analysis method is fast enough and automated enough to be used on a day-to-day basis by practicing engineers, and generates analysis reports with a small ratio of spurious errors to true errors.

In embedded systems the interfaces between software and its embedding environment are a major source of costly errors. For example, R.R. Lutz (1993) reported that 20%-35% of the safety related errors discovered during integration and system testing of two spacecraft were related to the interfaces between the software and the embedding hardware. Also, the software's operating environment is likely to change over time further complicating the issues related to system level inter component communication. We discuss a formal approach to the specification and analysis of inter component communication using a revised version of the RSML (Requirements State Machine Language) specification language. The formalism allows rigorous specification of the physical aspects of the inter component communication and enables encapsulation of communication related properties in well defined interface specifications. This allows us to both analyze a system design and detect incompatibilities between connected components and use the interface specifications as simple safety kernels to enforce safety and sample liveness constraints.

Computer software is playing an increasingly important role in safety-critical embedded computer systems, where incorrect operation of the software could lead to loss of life, substantial material or environmental damage, or large monetary losses. Although software is a powerful and flexible tool for industry, these very advantages have contributed to a corresponding increase in system complexity. In a previous investigation, the Irvine Safety Research Group developed a requirements specification language called the Requirements State Machine Language (RSML) suitable for the specification of safety critical control embedded systems. To simplify and automate the design and implementation process, we have investigated the possibility of automatically generating code from RSML specifications.

This report highlights some of the experiences gathered while analyzing the requirements specification for a commercial avionics system called TCAS II (Traffic alert and Collision Avoidance System II) for consistency and completeness. Completeness in this context is defined as a complete set of requirements, that is, there is a behavior specified for every possible input and input sequence.Under the leadership of Dr. Nancy G. Leveson, the Irvine Safety Research Group has developed a state-based requirements specification language RSML (Requirements State Machine Language) using TCAS II as a testbed [6]. The TCAS requirements specification project was very successful; RSML was well liked by all participants in the project, and the formal specification has been adopted as the official TCAS II requirements. The requirements document has been delivered to the FAA and has undergone an extensive independent validation and verification effort (IV&V).In a previous investigation, we defined procedures for analyzing state-based requirements specifications for completeness and consistency [5]. To demonstrate that our approach is feasible and is applicable to realistic systems, we have implemented a draft analysis tool and we have applied the analysis to the TCAS II requirements. The initial results from the analysis effort were encouraging [4, 5] and scaled well to a large requirements specification. The most complex parts of the TCAS requirements specification have recently been analyzed. Even though the effort was largely successful, some limitations with the approach have surfaced. Most importantly, the accuracy of the analysis algorithms needs improvement. When analyzing the most complex parts of the TCAS requirements, the number of spurious error reports can occasionally be overwhelming. Furthermore, we discovered that once the analysis has identified problems, it has been unexpectedly difficult to correct some of them.

This paper describes methods for automatically analyzing formal, state-based requirements specifications for some aspects of completeness and consistency. The approach uses a low-level functional formalism, simplifying the analysis process. State-space explosion problems are eliminated by applying the analysis at a high level of abstraction; i.e., instead of generating a reachability graph for analysis, the analysis is performed directly on the model. The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. Airspace.

This paper describes methods for automatically analyzing formal, state-based requirements specifications for completeness and consistency.The approach uses a low-level functional formalism, simplifying the analysis process.State space exploslon problems are eliminated by applying the analysis at a high level of abstraction;i.e, instead of generating a reachability graph for analysis, the analysis is performed directly on the model.The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification.The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system reqmred on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.

The paper describes an approach to writing requirements specifications for process-control systems, a specification language that supports this approach, and an example application of the approach and the language on an industrial aircraft collision avoidance system (TCAS II). The example specification demonstrates: the practicality of writing a formal requirements specification for a complex, process-control system; and the feasibility of building a formal model of a system using a specification language that is readable and reviewable by application experts who are not computer scientists or mathematicians. Some lessons learned in the process of this work, which are applicable both to forward and reverse engineering, are also presented.>

A set of criteria is defined to help find errors in, software requirements specifications. Only analysis criteria that examine the behavioral description of the computer are considered. The behavior of the software is described in terms of observable phenomena external to the software. Particular attention is focused on the properties of robustness and lack of ambiguity. The criteria are defined using an abstract state-machine model for generality. Using these criteria, analysis procedures can be defined for particular state-machine modeling languages to provide semantic analysis of real-time process-control software requirements.>