Autonomous systems use independent decision-making with only limited human intervention to accomplish goals in complex and unpredictable environments. As the autonomy technologies that underpin them continue to advance, these systems will find their way into an increasing number of applications in an ever wider range of settings. If we are to deploy them to perform safety-critical or mission-critical roles, it is imperative that we have justified confidence in their safe and correct operation. Verification is a key process for establishing such confidence. However, autonomous systems pose challenges to existing verification practices. This paper highlights viewpoints of the Roadmap Working Group of the IEEE Robotics and Automation Society Technical Committee for Verification of Autonomous Systems, identifying these grand challenges, and providing a vision for future research efforts that will be needed to address them.

Many sequential decision problems involve optimizing one objective function while imposing constraints on other objectives. Constrained Partially Observable Markov Decision Processes (C-POMDP) model this case with transition uncertainty and partial observability. In this work, we first show that C-POMDPs violate the optimal substructure property over successive decision steps and thus may exhibit behaviors that are undesirable for some (e.g., safety critical) applications. Additionally, online re-planning in C-POMDPs is often ineffective due to the inconsistency resulting from this violation. To address these drawbacks, we introduce the Recursively-Constrained POMDP (RC-POMDP), which imposes additional history-dependent cost constraints on the C-POMDP. We show that, unlike C-POMDPs, RC-POMDPs always have deterministic optimal policies and that optimal policies obey Bellman’s principle of optimality. We also present a point-based dynamic programming algorithm for RC-POMDPs. Evaluations on benchmark problems demonstrate the efficacy of our algorithm and show that policies for RC-POMDPs produce more desirable behaviors than policies for C-POMDPs.

Partially Observable Markov Decision Processes (POMDPs) are powerful models for sequential decision making under transition and observation uncertainties. This paper studies the challenging yet important problem in POMDPs known as the (indefinite-horizon) Maximal Reachability Probability Problem (MRPP), where the goal is to maximize the probability of reaching some target states. This is also a core problem in model checking with logical specifications and is naturally undiscounted (discount factor is one). Inspired by the success of point-based methods developed for discounted problems, we study their extensions to MRPP. Specifically, we focus on trial-based heuristic search value iteration techniques and present a novel algorithm that leverages the strengths of these techniques for efficient exploration of the belief space (informed search via value bounds) while addressing their drawbacks in handling loops for indefinite-horizon problems. The algorithm produces policies with two-sided bounds on optimal reachability probabilities. We prove convergence to an optimal policy from below under certain conditions. Experimental evaluations on a suite of benchmarks show that our algorithm outperforms existing methods in almost all cases in both probability guarantees and computation time.

Successful and convincing operation of a prototype, deployed in a real setting, is a key step in advancement of many a new technology from research laboratory to real-world use. Often, however, such a deployment must be interjected into a pre-existing context of ongoing activities, established designs and standard practices. That context can pose a number of obstacles, which if unaddressed can preclude success. Careful selection of what demonstration opportunities to pursue, and determination of how best to pursue them, are therefore crucial. A study was conducted to select and plan for deployment of prototypes of integrated system health management (ISHM) software on NASA spacecraft. The study itself utilized our seasoned technology maturation assessment process, based on a quantitative requirements analysis technique. However, this process is typically applied to scrutinize a single technology application at once. In this case there were a number of candidate deployment opportunities. Since it would have been tedious and time-consuming to consider each of them one-by-one, we adapted our assessment process to accommodate their simultaneous consideration. We relate our experience in doing this - the shortcuts we took, the similarities we exploited, and the workarounds we adopted to complete this study in a timely yet effective manner.

In the design of critical systems and software, validation and verification (VV a subset must be chosen that maximizes the chances of mission success by reducing risk while meeting budget constraints. By explicitly modeling the contributions that various V&V activities make to reducing risks, and the costs of these activities, we are able to convert this to a classical optimization problem. We then use search, clustering and visualization algorithms to examine the large space of options.

Adoption of advanced automated SE (ASE) tools would be favored if a business case could be made that these tools are more valuable than alternate methods. In theory, software prediction models can be used to make that case. In practice, this is complicated by the "local tuning" problem. Normally, predictors for software effort and defects and threat use local data to tune their predictions. Such local tuning data is often unavailable.

We present the ongoing NASA research infusion initiative, a sub-group of the NASA software working group which encourages the use of advanced technologies and the products of software engineering research in NASA projects and missions. An emphasis is placed on technologies and products that address software assurance. Technology infusion is generally a difficult process, but the effort described here seems to have found a modest approach that is successful for some types of technologies. We outline the process and report on the outcomes of some infusions run over in the past. We also present some lessons learned from our experiences.

A vision is presented for fusing quantitative requirements analysis with model-based systems engineering. This vision draws upon and combines emergent themes in the engineering milieu. "Requirements engineering" provides means to explicitly represent requirements (both functional and non-functional) as constraints and preferences on acceptable solutions, and emphasizes early-lifecycle review, analysis and verification of design and development plans. "Design by shopping" emphasizes revealing the space of options available from which to choose (without presuming that all selection criteria have previously been elicited), and provides means to make understandable the range of choices and their ramifications. "Model-based engineering" emphasizes the goal of utilizing a formal representation of all aspects of system design, from development through operations, and provides powerful tool suites that support the practical application of these principles. A first step prototype towards this vision is described, embodying the key capabilities. Illustrations, implications, further challenges and opportunities are outlined

In this paper, we elaborate on the decision support needs during conceptual, concurrent design. For this purpose, we consider the type of decision aids that might be helpful to the designers during design, and the information needed by the applications of the products of the design that could be captured and structured by these decision aid tools and processes. We explain our current thoughts and recommendations with respect to the research challenges in this area based on our experience with conceptual, concurrent design teams, as well as our synthesis of the first NASA sponsored workshop on "Decision Based Design Structures" that was held on October 6, 7, & 8/sup th/ 2004 to address some of the same issues. The design context under consideration is space missions.

Early risk assessment is key in planning the development of systems, including systems that involve software. Such risk assessment needs a combination of the following elements; 1) Severity estimates for the potential effects of failures, and likelihood estimates for their causes; 2) Fault trees that link causes to failures; 3) Efficacy estimates of design and process steps towards reducing risk; 4) Distinctions between preventing, alleviating and detecting (thereafter removing), risks; 5) Risk preventions that have potential side effects of themselves introducing risks. The paper shows a unified approach that accommodates all these elements. The approach combines fault trees (from probabilistic risk assessment methods) with explicit treatment of risk mitigations (a generalization of the notion of a "detection" seen in FMECA analyses). Fault trees capture the causal relationships by which failure mechanisms may combine to lead to failure modes. Risk mitigations encompass (and distinguish among) options to prevent risks, detect risks, and alleviate risks (i.e., decrease their impact should they occur). This approach has been embodied in extensions to a JPL-developed risk assessment tool, and is illustrated here on software risk assessment information drawn from an actual project's software system FMECA (failure modes, effects and criticality analysis). Since its elements are typical of risk assessment of software and its system interface, the findings should be relevant to a wide range of software systems.

We present an approach to matching software practitioners' needs to software researchers' activities. It uses an accepted taxonomical software classification scheme as intermediary, in terms of which practitioners express needs, and researchers express activities. A decision support tool is used to combine these expressions of needs/activities, and to assist in studying the implications of that combined knowledge. This enables identification of fruitful connections between researchers and practitioners, of areas of common interest among researchers, and practitioners, and of "gaps": areas of unfulfilled needs or unmotivated research. We discuss the software engineering underpinning this approach, illustrating its utility by reporting on experiments with a real-world dataset gathered from researchers and practitioners. We also suggest that this same approach would be applicable to understanding the distribution of interests represented by presenters and attendees of a conference such as APSEC.

A critical issue in software engineering is how to construct high assurance software systems, i.e., software Systems where compelling evidence is required that the system delivers its services in a manner satisfying critical properties, such as safety and security. This two-day XSE workshop, the third in a series of workshops on high assurance systems, will provide a forum for researchers and practitioners to exchange ideas and experiences relevant to the development of software for aerospace systems, medical systems, systems controlling nuclear power plants, and other critical systems. Participants of the SEHAS 2003 workshop will explore the opportunities for, and benefits of, synergies between three important themes-product, process, and profiling-each theme reflecting an important aspect of software development for high assurance systems.

Many organizations look to research to yield new and improved products and practices. Connecting practitioners who have the need for research results to the researchers producing those results is important to guiding research and utilizing its results. Likewise, connecting researchers working on related topics to one another, and connecting practitioners with related needs to one another, is important to establishing communities of shared interests. We demonstrate an approach that helps identify fruitful such connections.

Many organizations would benefit from enterprise-wide, shared information systems. It is common for these organizations to have in place a number of smaller information systems, each of which solves a portion of the problem. Typically, these smaller systems will have been developed independently of one another. As a result, they exhibit many forms of heterogeneity, which pose many impediments to integration. In this paper, we propose and justify an architecture suitable for integrating these smaller systems into a shared information system. The architecture must, to varying degrees of importance, be flexible, responsive, space-efficient, scalable, easy to use, and reliable. The integration effort must also be taken into account. Illustrations are taken from an ongoing case study in which two systems that operate on complementary areas of risk management are being integrated and extended.

Planning for the optimal attainment of requirements is an important early lifecycle activity. However, such planning is difficult when dealing with competing requirements, limited resources, and the incompleteness of information available at requirements time. A novel approach to requirements optimization is described. A requirements interaction model is executed to randomly sample the space of options. This produces a large amount of data, which is then condensed by a summarization tool. The result is a small list of critical decisions (i.e., those most influential in leading towards the desired optimum). This focuses human experts' attention on a relatively few decisions and makes them aware of major alternatives. This approach is iterative. Each iteration allows experts to select from among the major alternatives. In successive iterations the execution and summarization modules are run again, but each time further constrained by the decisions made in previous iteration. In the case study shown here, out of 99 yes/no decisions (approximately 10/sup 30/ possibilities), five iterations were sufficient to find and make the 30 key ones.

Tools have been developed that support risk identification and management activities during different phases of a project lifecycle. For the earlier stages of the project lifecycle, a tool for the qualitative identification and manipulation of risk and risk mitigation data was developed. For the later stages of the lifecycle, a separate tool for the quantitative manipulation of requirements, risk and risk mitigation data was developed. These two tools were then combined into a single tool. The combination of these qualitative and quantitative risk management tools is the focus of this paper. The combination was first envisioned as simply a convenience, ensuring that the results from the early lifecycle risk management would flow smoothly into the later lifecycle management. However, it was found that the combination led to the possibility of extending many of the capabilities of each tool into the other tool's phases. The net result is a combination that exhibits the best attributes of both qualitative and quantitative risk management tool support.

There is a trend towards the increased use of automation in V&V (verification and validation). Automation can yield savings in time and effort. For critical systems, where thorough V&V is required, these savings can be substantial. We describe a progression from pilot studies to development and use of V&V automation. We used pilot studies to ascertain opportunities for, and suitability of automating various analyses whose results would contribute to V&V. These studies culminated in the development of an automatic generator of automated test oracles. This was then applied and extended in the course of testing an AI planning system that is a key component of an autonomous spacecraft.

Lightweight formal methods promise to yield modest analysis results in an extremely rapid manner. To fulfil this promise, they must be able to work with existing information sources, be able to analyze for manifestly desirable properties, be highly automated (especially if dealing with voluminous amounts of information), and be readily customizable and flexible in the face of emerging needs and understanding. Two pilot studies investigate the feasibility of lightweight formal methods that employ a database as the underlying reasoning engine to perform the analyses. The first study concerns aspects of software module interfaces, while the second concerns test logs' adherence to required and expected conditions.

No abstract available.

We propose requirements monitoring to aid in the maintenance of systems that reside in dynamic environments. By requirements monitoring we mean the insertion of code into a running system to gather information from which it can he determined whether, and to what degree, that running system is meeting its requirements. Monitoring is a commonly applied technique in support of performance tuning, but the focus therein is primarily on computational performance requirements in short runs of systems. We wish to address systems that operate in a long lived, ongoing fashion in nonscientific enterprise applications. We argue that the results of requirements monitoring can be of benefit to the designers, maintainers and users of a system-alerting them when the system is being used in an environment for which it was not designed, and giving them the information they need to direct their redesign of the system. Studies of two commercial systems are used to illustrate and justify our claims.

The ability to rapidly reconnoitre requirements, i.e., construct, critique, contrast and complete a system's requirements, necessitates dealing with the inherent nature of requirements (their incompleteness, inconsistency, ambiguity, etc.). It is shown how such explorations can be sustained by linking a network of domain requirements with instantiations of those requirements for a particular instance of that domain.>

The approach to representation and presentation of knowledge used in ARIES, an environment to experiment with support for analysts in modeling target domains and in entering and formalizing system requirements, is described. To effectively do this, ARIES must manage a variety of notations so that analysts can enter information in a natural manner, and ARIES can present it back in different notations and from different viewpoints. To provide this functionality, a single, highly expressive internal representation is used for all information in the system. The system architecture separates representation and presentation, in order to localize consistency and propagation issues. The presentation architecture is tailored to be flexible enough so that new notations can be easily introduced on top of the underlying representation. Presentation knowledge is coupled to specification evolution knowledge thereby leveraging common representations for both in order to provide automated focusing support to users who need informative guidance in creating and modifying specifications.>

In this panel session, the following topics are discussed: artificial intelligence in business; artificial intelligence in multimedia; neural networks as a tool for artificial intelligence: software engineering for knowledge-based systems: and artificial intelligence as a solution for software engineering.>

An incremental approach to construction is proposed, with the virtue of offering considerable opportunity for mechanized support. Following this approach one builds a specification through a series of elaborations that incrementally adjust a simple initial specification. Elaborations perform both refinements, adding further detail, and adaptations, retracting oversimplifications and tailoring approximations to the specifics of the task. It is anticipated that the vast majority of elaborations can be concisely described to a mechanism that will then perform them automatically. When elaborations are independent, they can be applied in parallel, leading to diverging specifications that must later be recombined. The approach is intended to facilitate comprehension and maintenance of specifications, as well as their initial construction.>

When a complex system is to be realized as a combination of interacting components, development of those components should commence from a specification of the behavior required of the composite system. A separate specification should be used to describe the decomposition of that system into components. The first phase of implementation from a specification in this style is the derivation of the individual component behaviors implied by these specifications. The virtues of this approach to specification are expounded, and specification language features that are supportive of it are presented. It is shown how these are incorporated in the specification language Gist, which our group has developed. These issues are illustrated in a development of a controller for elevators serving passengers in a multistory building.

article Free Access Share on A System for Assisting Program Transformation Author: Martin S. Feather USC/Information Sciences Institute, 4676 Admiralty Way, Marina del Rey, CA USC/Information Sciences Institute, 4676 Admiralty Way, Marina del Rey, CAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 4Issue 1Jan. 1982 pp 1–20https://doi.org/10.1145/357153.357154Published:01 January 1982Publication History 99citation430DownloadsMetricsTotal Citations99Total Downloads430Last 12 Months17Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Presentation of the fonnal specification of a small text formatter illustrates an approach to the construction of formal specifications. The key features of this approvach are described, and their beneficial influence on the construction and organization of specifications of tasks, especially those for which no concise descriptions are possible, are discussed. The intent is that in addition to serving as formal descriptions of tasks, such specifications will be of use in the processes of verification, development, and maintenance of their implementations.