Timed Safety Automata and Logic Conformance.
AIR FORCE INST OF TECH WRIGHT-PATTERSONAFB OH
Pagination or Media Count:
Timed Logic Conformance TLC is used to verify the behavioral and timing properties of detailed digital circuits against abstract circuit specifications when both are modeled as Timed Safety Automata TSA with real-valued clocks. TLC is a bisimulation-style partial order relationship defined over TSA state space. In contrast to timed simulation, Calculus of Timed Refinement, and time-abstracted bisimulation, TLC defines when one system is an acceptable implementation of another by asymmetric action-matching requirements for specification inputs and implementation outputs. TLC intuitively and pragmatically supports writing abstract specifications and verifying them against implementations. TLC scales up by substituting verified specifications for implementations and hierarchically verifying larger systems. The TLC verification process is more efficient than the circularly dependent assumes-guarantees verification methodology. Instead of building models of the systems environment and using them in the verification process, the TLC verification methodology explicitly captures environmental timing properties in the system specification and automatically ensures they are satisfied in the TLC relation. The region-automata-based Timed Logic Conformance System TLCS implements TSA parallel composition and a TLC decision procedure. TLCS is used to hierarchically verify the STARI Self-Timed at Receivers Input asynchronous circuit for communicating safely between clock-skewed systems.
- Electrical and Electronic Equipment
- Computer Hardware