NASA NTRS1990
Software is playing increasingly important roles in avionics systems. It is widely used in navigation and, in some cases, in control loops that maintain aircraft stability. To guarantee the safety of flight systems, the FAA requires that critical components have a probability of failure no greater than 10(exp -9) per hour of flight. Software is being used to diagnose system components for failure. SIFT (Software Implemented Fault Tolerance) was a computer system developed to study the use of software to check for failure and manage processor reconfiguration. To guarantee that software satisfies its specifications, formal verification can be used. With this a program and its specification are viewed as mathematical objects, and a mathematical proof is used to show that the program and its specification are equivalent. In previous research, a theory of checking was developed to offer assistance in analyzing specifications and designing run-time checks. In the theory, checking is considered abstractly in terms of n-ary relations much like those of relational database theory. Within the theory check are categorized, checks on input and checks on results are considered, and formal attention is given to the minimization and logical combination of checks. The focus is upon input checks and the obstacles in checking input to critical systems. A central concern is with a property referred to as independence. The concern is with circumstances under which it is possible to apply isolated, independent checks to separate sensor inputs and be assure that all illegal input will be properly detected. Presently, independence is being investigated and checked in the context of the GCS (Guidance and Control System). The GCS simulator is intended for testing software that implements control laws for landing spacecraft. The large number of inputs and their complex interrelationships provide an exciting context in which to investigate independence and the difficulties of supplying input checks.