On Specifications and Proofs of Timed Circuits - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2022

On Specifications and Proofs of Timed Circuits

Résumé

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.

Dates et versions

hal-03935679 , version 1 (12-01-2023)

Identifiants

Citer

Matthias Függer, Christoph Lenzen, Ulrich Schmid. On Specifications and Proofs of Timed Circuits. Principles of Systems Design, 13660, Springer Nature Switzerland, pp.107-130, 2022, Lecture Notes in Computer Science, 978-3-031-22337-2. ⟨10.1007/978-3-031-22337-2_6⟩. ⟨hal-03935679⟩
32 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More