Verification of homomorphism between two system models

The invention concerns ascertaining whether the successful accomplishment of a defined task by a simpler model of a complex system implies that the complex system will also accomplish the defined task. The invention performs the ascertainment by checking language containment of the two models.

BACKGROUND OF THE INVENTION 
The designer of a complex system generally wishes to verify that the system 
will perform as expected, prior to actually constructing the system. The 
designer commonly generates a model of the system, in order to simulate 
operation of the system. 
Frequently, the model takes the form of a complex state machine. However, a 
complex state machine can reside in an astronomical number of states, and 
it is generally unfeasible to examine all states, in the testing process. 
Example of Large Number of States 
An illustration of a large number of states can be found in random access 
memory, RAM (which is not necessarily a state machine, but which 
illustrates the magnitude of the problem). Consider a RAM which contains 
one million bytes, giving a total of eight million bits of storage 
capacity. The number of possible different combinations of stored bits is 
2.sup.8,000,000, which is an utterly enormous number. The RAM, or even a 
model of it, cannot be tested by storing all possible bit combinations. 
Luckily, in the case of RAM, all possible combinations need not necessarily 
be used. It may be sufficient to write a specific word into every memory 
location (instead of every possible combination of words), and then read 
each word, to verify that the words have been stored properly. This 
process involves one million write operations, plus one million read 
operations, together with the analysis of each read operation. 
This simpler test can be done in a reasonable length of time. However, 
success of this test does not necessarily guarantee perfect functioning of 
the system. For example, it is possible (but unlikely) that use of a 
different word will produce errors. This fact will not be detected by use 
of the original word. As another example, it is possible that storing two 
different words at adjacent locations may cause an error, and this fact 
would also not be detected by the original word. 
Large State Machines 
State machines also possess large numbers of possible states, and it is not 
feasible, or even possible, in many cases, to cycle the state machine 
through all states. 
The invention is concerned with verifying whether a given simpler model, 
perhaps of a state machine, which accomplishes a specified task, is 
homomorphic to a larger model, thereby implying that the larger model also 
accomplishes the specified task. 
SUMMARY OF THE INVENTION 
In using one form of the invention, a designer postulates a simplified (or 
more abstract) model of a larger system. The invention checks automata 
language containment by representing the more abstract model in terms of a 
particular transformation which represents it as a conjunction of elements 
from a different class of automata.

DETAILED DESCRIPTION OF THE INVENTION 
Appendices A, B, C and D contain technical information sufficient to 
explain how to implement the invention using a programmable digital 
computer. Appendices A, B, C, and D are hereby incorporated by attachment. 
A method of verifying whether a reduced model is homomorphic to a more 
complex model is given in Appendix A, section 8.10, entitled "Automatic 
Reduction of Symmetries." FIG. 8.7 illustrates the method in tabular form. 
Appendices C and D provide C-code extracts which would assist a designer in 
writing a program which will run on a system known as COSPAN, and which is 
described in U.S. Pat. No. 5,163,016, issued to Alur et al. on Nov. 10, 
1992. This patent is hereby incorporated by reference. Alternately, a 
system known as SMV, available as public domain software, developed at 
Carnegie-Mellon University, can be used. 
Appendix B contains observations and suggestions which were developed based 
on the inventors' experience with application of the invention to the 
analysis of highly complex systems. These observations and suggestions 
will assist a designer in optimizing code which is written. 
U.S. Pat. No. 5,163,016, issued to Har'El et al. on Nov. 10, 1992, 
describes a development apparatus suitable for use with the present 
invention. This patent is hereby incorporated by reference. 
Numerous substitutions and modifications can be undertaken without 
departing from the true spirit and scope of the invention. 
##SPC1##