Display options
Cite
Dolev D, Függer M, Posch M, et al. Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip. J Comput Syst Sci. 2014;80(4):860-900doi: 10.1016/j.jcss.2014.01.001.
Dolev, D., Függer, M., Posch, M., Schmid, U., Steininger, A., & Lenzen, C. (2014). Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip. Journal of computer and system sciences, 80(4), 860-900. https://doi.org/10.1016/j.jcss.2014.01.001
Dolev, Danny, et al. "Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip." Journal of computer and system sciences vol. 80,4 (2014): 860-900. doi: https://doi.org/10.1016/j.jcss.2014.01.001
Dolev D, Függer M, Posch M, Schmid U, Steininger A, Lenzen C. Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip. J Comput Syst Sci. 2014 Jun;80(4):860-900. doi: 10.1016/j.jcss.2014.01.001. PMID: 26516290; PMCID: PMC4579925.
Copy Download .nbib Format: NLM
Share it on

J Comput Syst Sci. 2014 Jun;80(4):860-900. doi: 10.1016/j.jcss.2014.01.001.

Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip.

Journal of computer and system sciences

Danny Dolev, Matthias Függer, Markus Posch, Ulrich Schmid, Andreas Steininger, Christoph Lenzen

Affiliations

  1. School of Engineering and Computer Science, The Hebrew University of Jerusalem, Edmond Safra Campus, 91904 Jerusalem, Israel.
  2. Department of Computer Engineering, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria.
  3. Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 32 Vassar Street, 02139 Cambridge, MA, USA.

PMID: 26516290 PMCID: PMC4579925 DOI: 10.1016/j.jcss.2014.01.001

Abstract

We present the first implementation of a distributed clock generation scheme for Systems-on-Chip that recovers from an unbounded number of arbitrary transient faults despite a large number of arbitrary permanent faults. We devise self-stabilizing hardware building blocks and a hybrid synchronous/asynchronous state machine enabling metastability-free transitions of the algorithm's states. We provide a comprehensive modeling approach that permits to prove, given correctness of the constructed low-level building blocks, the high-level properties of the synchronization algorithm (which have been established in a more abstract model). We believe this approach to be of interest in its own right, since this is the first technique permitting to mathematically verify, at manageable complexity, high-level properties of a fault-prone system in terms of its very basic components. We evaluate a prototype implementation, which has been designed in VHDL, using the Petrify tool in conjunction with some extensions, and synthesized for an Altera Cyclone FPGA.

Keywords: Byzantine fault-tolerance; Clock synchronization; Dependability; Experiments; Hardware implementation; Hybrid state machines; Metastability; Modeling framework; Self-stabilization; Theoretical analysis

Publication Types