On specifications and proofs of timed circuits

DOI10.1007/978-3-031-22337-2_6MaRDI QIDQ6113972zbMATH OpenOpenAlexFDO

Authors Matthias Függer, Christoph Lenzen, Ulrich Schmid

Publication date 10 August 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2208.08147

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Switching theory, applications of Boolean algebras to circuits and networks (94C11)

Abstract: Given a discrete-state continuous-time reactive system, like a digital circuit, the classical approach is to first model it as a state transition system and then prove its properties. Our contribution advocates a different approach: to directly operate on the input-output behavior of such systems, without identifying states and their transitions in the first place. We discuss the benefits of this approach at hand of some examples, which demonstrate that it nicely integrates with concepts of self-stabilization and fault-tolerance. We also elaborate on some unexpected artefacts of module composition in our framework, and conclude with some open research questions.

Recommendations

• Temporal proof methodologies for timed transition systems
• scientific article; zbMATH DE number 1955911
• scientific article; zbMATH DE number 1304998
• Functional specification and proof of correctness for time dependent behaviour of reactive systems
• scientific article; zbMATH DE number 3982506

Cites work

• A theory of timed automata
• Asynchronous Sequential Switching Circuits with Unrestricted Input Changes
• Complexity of network synchronization
• Fault tolerance in the cardiac ganglion of the lobster
• Fault-tolerant algorithms for tick-generation in asynchronous logic: robust pulse generation
• Forward and backward simulations. I. Untimed Systems
• Forward and backward simulations. II: Timing-based systems
• General theory of metastable operation
• HEX: scaling honeycombs is easier than scaling clock trees
• scientific article; zbMATH DE number 3819094 (Why is no real title available?)
• scientific article; zbMATH DE number 2017345 (Why is no real title available?)
• scientific article; zbMATH DE number 2061537 (Why is no real title available?)
• Impossibility of distributed consensus with one faulty process
• Metastability-Containing Circuits
• On the minimal synchronism needed for distributed consensus
• Reaching Agreement in the Presence of Faults
• Reconciling fault-tolerant distributed computing and systems-on-chip
• Rigorously modeling self-stabilizing fault-tolerant circuits: an ultra-robust clocking scheme for systems-on-chip
• Self-stabilization
• Self-stabilizing systems in spite of distributed control
• Specification and Development of Interactive Systems
• The Theory of Timed I/O Automata
• The topology of the regulatory interactions predicts the expression pattern of the segment polarity genes in \textit{Drosophila melanogaster}
• Time, clocks, and the ordering of events in a distributed system
• Unfaithful Glitch Propagation in Existing Binary Circuit Models

Cited in

(3)

• On the determinization of timed systems
• scientific article; zbMATH DE number 791802 (Why is no real title available?)
• Translational lemmas for DLOGTIME-uniform circuits, alternating TMs, and PRAMs

This page was built for publication: On specifications and proofs of timed circuits

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6113972)