The accurate, reliable, and precise operation of NIT systems will underscore the public acceptance and success of the information age, given that they will be increasingly more encompassing, powerful, highly capable, and greatly beneficial in the future. The stakes for NIT systems will be increasingly high and even the slightest error may not be tolerable. For example, should a design error in a nationwide patient medical record network accidentally release the medical records of thousands of patients even once, irreversible damage will result, causing the public to lose confidence in the system. Logic dictates that the precision of an NIT system will depend, in turn, on the functional accuracy of the underlying ADDM algorithm, which implies the indispensable need to construct proof of correctness of the algorithm. In the absence of a proof, there is the strong likelihood of the algorithm executing erroneously.
ADDM algorithms are characterized by a significant number of interactions between the constituent entities. The asynchrony and distributed nature of these interactions manifest in the form of complex timing relationships between the events and complex system states. While the precise execution of the events is crucial to the overall correct functioning of the system, for the system to manifest in any of the states in the course of its operation is a distinct possibility. Where the correctness of every conceivable state and event is not proven, freedom from errors cannot be guaranteed. From experience with. ADDM algorithms,...
TABLE OF CONTENTS 
