Achieving understandable results in a formal design verification

摘要

An approach is presented for clarifying the process and the results of formal design specification and its verification. The approach is validated via a simple illustrative experiment. A further validation of the approach by its application to an internet system (the USAF Multinet Gateway System) is described. As a consequence of the approach, the verification results are made more understandable, and thus the credibility of the assurance demonstration of a system is increased.