A formal investigation of checking the input to critical systems

Safe reliable systems must be able to detect component failure. Checks in software can be effective for detecting hardware and sensor failure as well as for detecting errors in the software itself. This work develops a formal theory of checking in which the nature and structure of checks are investigated. Important to the theory is the notion of independence, which can be defined in terms of n-ary relations. The utility of the theory is illustrated by analyses of checks on input in various software contexts. In particular, sensor input to the NASA Guidance and Control Software is analyzed