Data processing: structural design – modeling – simulation – and em – Modeling by mathematical expression
Reexamination Certificate
2000-05-22
2004-03-16
Thomson, W. D. (Department: 2123)
Data processing: structural design, modeling, simulation, and em
Modeling by mathematical expression
C703S013000, C703S022000, C716S030000, C714S033000
Reexamination Certificate
active
06708143
ABSTRACT:
BACKGROUND OF THE INVENTION
This invention relates to system verification, and more particularly to a method for ascertaining coverage obtained from a given collection of queries.
An ongoing problem in the design of large systems is verifying that the system will indeed behave in the manner intended by its designers. One approach has been to simply try out the system, either by building and testing the system itself or by building and testing a model of the system. Another approach is to test a software model of the system through simulations that test the functionality and/or properties of the system.
In testing a system design artisans classically create a model of the hardware or the software system being tested, and run the model through a number of simulations, where each simulation focuses on a functional aspect (property) of the hardware or software design. Since a single simulation is rarely sufficient to test a given property, a number of related simulations are executed for each functional aspect of the design to determine whether the property is correctly implemented in the hardware or software. Together, the group of related simulations is called a test suite.
Running a test suite can be a time consuming and costly process, requiring set-up, running the simulations, and evaluating the results. Moreover, it is quite possible that a test run would result in an error condition, indicating that the system model does not perform as desired. Such a condition calls for a modification of the system design and a repeat run of the tests.
Another method for testing a hardware and/or software design is formal verification. In formal verification, the designer provides to a formal verification system a logical definition of the intended behavior of the design or system, and a logical definition of the implementation of the system. The formal verification system then determines whether the logical definition of the implementation implies the logical definition of the system's intended behavior. That is, the formal verification system determines whether the implementation can perform the functions or tasks it is intended to perform, as defined by the system specification.
In U.S. Pat. No. 5,691,925, issued Nov. 25, 1997, an efficient method is disclosed where a system design is verified by forming a reduced model with respect to a tested property of the system, and running a verification operation on the reduced model. This localization reduction consists of eliminating some program variables, and decreasing the range of other program variables. This reduction is conservative, in the sense that it guarantees that a property will hold in the unreduced model if it holds in the reduced model. Performing the verification operation on the reduced model is quicker, and a verification that a query is satisfied in the reduced model extends to the unreduced system.
At some point in the course of testing properties it may be determined that a property is not satisfied, requiring a modification to the system's model. This raises the issue of whether properties that had been verified need to be verified again, for the modified system. The decision whether verification of a property needs to be undertaken following a modification to the system may be reached by saving a checksum with each localization reduction and, then, after the model has changed, recompute the checksum for the localization reductions. If a checksum of a localization reduction with respect to a particular property after the system model is modified matches the checksum of the localization reduction with respect to that property in the unmodified system model, one can conclude that property need not be verified for the modified model. This technique is described by Hardin et al in “Efficient Regression Verification,” IEE Proc. WODES'96, 1996, pp. 147-150.
Although the methods described above are very beneficial, it still remains that the set of queries that are used to verify the system might not be sufficient to verify the entirety of the system. There may be variables of the system that have not been exercised and values of variables that have not been employed. Knowledge about coverage may lead to the creation of additional queries to be tested, or it may lead to a conclusion that some system portions are unnecessary to the system's functionality.
SUMMARY OF THE INVENTION
An advance in the art is realized with respect to the coverage issue by verifying the system design in accordance with any of the above teachings, and maintaining a store of variables employed and the ranges of the employed variables. In one illustrative embodiment, for example, a given a system model is verified by verifying one property at a time. With respect to each verification, the system model is reduced to form a reduced model, by eliminating all variables having no effect on the property being verified, leaving only those variables and ranges of those variable upon which the given property has a dependence. As the model is verified with respect to each property, the variables and their ranges that are employed in the verifications are collected and, at the conclusion of the verifications, a report is generated for the designer that identifies variables and ranges of variables that have not been employed in verifying any of the properties. If the coverage is less than complete, the designer can assess whether other queries ought to be formulated, or whether portions of the system are superfluous.
REFERENCES:
patent: 5163016 (1992-11-01), Har'El et al.
patent: 5691925 (1997-11-01), Hardin et al.
patent: 5901073 (1999-05-01), Kurshan et al.
patent: 5926622 (1999-07-01), Hardin et al.
patent: 5946481 (1999-08-01), Kurshan et al.
patent: 6102959 (2000-08-01), Hardin et al.
patent: 6185516 (2001-02-01), Hardin et al.
Caughlin, “Verification, Validation, and Accreditation (VV&A) of Models and Simulations through Reduced Order Metamodels”, Proceedings of the 27th Conference on Winter Simulation, Dec. 1995, pp. 1405-1412.*
Clarke et al., “Formal Methods: State of the Art and Future Directions”, ACM Computing Surveys, vol. 28, No. 4, 1996, pp. 626-643.5163016.
Lucent Technologies - Inc.
Thomson W. D.
LandOfFree
Verification coverage method does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Verification coverage method, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verification coverage method will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3206089