Timed Safety Automata and Logic Conformance.
Abstract
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 system's 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 Receiver's Input) asynchronous circuit for communicating safely between clock-skewed systems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1999
- Accession Number
- ADA364388
Entities
People
- Frank C. Young
Organizations
- Air Force Institute of Technology