On Specifications and Proofs of Timed Circuits

TL;DR

This paper proposes a novel approach for verifying timed circuits by directly analyzing their input-output behavior, bypassing traditional state-based modeling, which enhances integration with self-stabilization and fault-tolerance concepts.

Contribution

It introduces a direct input-output analysis method for timed circuits, offering new insights into module composition and system robustness without relying on state transition models.

Findings

Demonstrates benefits of behavior-based analysis in timed circuits

Highlights unexpected effects of module composition

Discusses open questions in the framework's development

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.