Congruent weak conformance.

摘要

This research addresses the problem of verifying implementations against specifications through an innovative logic approach. Congruent weak conformance, a formal relationship between agents and specifications, has been developed and proven to be a congruent partial order. This property, symbolized $\succ w$, arises from a set of relations called weak conformations . The largest, called weak conformance, is analogous to Milner's observational equivalence. Unlike observational equivalence, however, weak conformance is not an equivalence, but rather an ordering relation among processes. Like the previous property of logic conformance, weak conformance allows behaviors in the implementation that are unreachable in the specification. Unlike logic conformance, however, weak conformance exploits output concurrencies and allows interleaving of extraneous output actions in the implementation. Finally, reasonable restrictions in design models strengthen weak conformance to a congruence. Being both congruent and a partial order, it merits the customary term precongruence. At this writing, $\succ w$ is the best known formal relation for verifying implementations against specifications. This precongruence derives maximal flexibility and embodies all weaknesses in input, output, and no-connect signals while retaining a fully replaceable conformance to the specification. This desirable relation is described in four transitional laws with five constructional restrictions.; Congruent weak conformance has additional utility in verifying transformations between systems of incompatible semantics such as found in circuit development, security system design, and software engineering. This dissertation describes a hypothetical translator from the informal simulation semantics of VHDL to the bisimulation semantics of CCS. A second translator is described from VHDL to a broadcast-communication version of CCS. By showing that they preserve congruent weak conformance, both translators are verified.