Timed safety automata and logic conformance.

摘要

Major Young's research, sponsored by the Air Force Research Laboratory, defined a formal relationship between timed models of digital electronic circuits. He defined how to model detailed electronic circuits and circuit specifications, and he developed a verification methodology and automated proof system for computing when the circuit timing and behavior properties are consistent. When they are consistent, the detailed circuit implements the specification and the specification model is then used to design and prove properties about larger systems hierarchically. Major Young's research will significantly improve Air Force electronics modeling, verification, and synthesis.