This document proposes an architecture to produce software for use by U.S. soldiers on commercially available smart phones and other mobile hardware to increase their productivity. The architecture decreases time to production while maintaining Department of Defense Information Assurance standards.

The paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process to validate the evolving requirements. The results were fed back into the projects to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhanced the existing verification and validation processes by testing key properties of the evolving requirements and helping to identify weaknesses. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.

Studies show that early stages of the system development life cycle are especially prone to errors. Problems which originate in early stages can have a lasting influence on the reliability, safety, and cost of a system. The National Aeronautics and Space Administration (NASA) is investigating the use and effectiveness of Formal Methods (FM) in trial projects to improve the quality of software and system requirements. The study reports on the application of FM to the Failure Detection, Isolation, and Recovery (FDIR) system for the Space Station. Abstraction, type checking formal specification, and proof were used to assess the adequacy of several related views of the FDIR requirements. Results indicate that abstraction revealed underlying conceptual simplicity that was hard to recognize in the original description. Furthermore, the use of automated formal methods tools permitted rapid and comprehensive consistency checks which would have been impractical manually. We believe the analysis methodology outlined in the paper is a cost effective way to help ensure that requirements will be interpreted correctly by system designers.

Before Expert System (ES) technology can be effectively used for complex systems a comprehensive verification and validation (V&V) methodology must be defined. Evidence from the computer industry suggests that without such a methodology Expert Systems will not be considered safe and reliable for field use. to this end, we have defined a design language called TOP (Terms, Operators, and Productions) for specifying knowledge-base designs which support verification and validation. This article discusses the key features of TOP which are: term subsumption, operator methods, sequence expressions, and a method for translating TOP designs into C-Language Production System (CLIPS) rules. to put these features of TOP into perspective, several illustrations from applications using TOP are presented. We believe that the concepts presented here serve as a solid foundation for practical application of Expert Systems and continued research into the verification and validation of Expert Systems. © 1994 John Wiley & Sons, Inc.