BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Ulrich Schmid

Ulrich Schmid contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Distributed, Parallel, and Cluster Computingcond-mat.mtrl-scieess.SYFormal Languages and Automata TheoryHardware ArchitectureLogic in Computer ScienceNetworking and Internet ArchitectureOther Computer Sciencephysics.app-phSystems and Control

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
10topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

7 published item(s)

preprint2022arXiv

On Specifications and Proofs of Timed Circuits

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Time Complexity of Consensus in Dynamic Networks Under Oblivious Message Adversaries

Consensus is a most fundamental task in distributed computing. This paper studies the consensus problem for a set of processes connected by a dynamic directed network, in which computation and communication is lock-step synchronous but controlled by an oblivious message adversary. In this basic model, determining consensus solvability and designing consensus algorithms in the case where it is possible, has been shown to be surprisingly difficult. We present an explicit decision procedure to determine if consensus is possible under a given adversary. This in turn enables us, for the first time, to study the time complexity of consensus in this model. In particular, we derive time complexity upper bounds for consensus solvability both for a centralized decision procedure as well as for solving distributed consensus. We complement these results with time complexity lower bounds. Intriguingly, we find that reaching consensus under an oblivious message adversary can take exponentially longer than broadcasting the input value of some process to all other processes.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

3D arrangement of epitaxial graphene conformally grown on porousified crystalline SiC

Nanoporous materials represent a versatile solution for a number of applications ranging from sensing, energy applications, catalysis, drug delivery, and many others. The synergy between the outstanding properties of graphene with a three-dimensional porous structure, circumventing the limits of its 2D nature, constitutes therefore a breakthrough for many fields. We report the first three-dimensional growth of epitaxial graphene on a porousified crystalline 4H-SiC(0001). The wafer porosification is performed via a sequence of metal-assisted photochemical and photoelectrochemical etching in hydrofluoric acid based electrolytes. Pore dimensions of the matrix have been evaluated by electron tomography resulting in an average diameter of 180 nm. Graphene growth is performed in an ultra high vacuum environment at a base pressure of $10^{-11}$ mbar. The graphene growth inside the pores is uniform as confirmed by Transmission Electron Microscopy (TEM) analysis. Raman spectroscopy confirms the high quality of the graphene with a 2D/G ratio $>1$ and an average graphene crystal size of $\approx$ 100 nm. Furthermore, it demonstrates a uniform coverage of graphene across the whole sample area. The surface-to-volume ratio of this novel material, its properties, the tunability of the pore size and the scalability of the surface porosification process offer a game changing perspective for a large number of applications.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms

We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of Byzantine faulty processes. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking. We demonstrate the practical feasibility of our method by verifying several variants of the well-known distributed algorithm by Srikanth and Toueg. Our semi-decision procedures are complemented and motivated by an undecidability proof for FTDA verification which holds even in the absence of interprocess communication. To the best of our knowledge, this is the first paper to achieve parameterized automated verification of Byzantine FTDA.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Unfaithful Glitch Propagation in Existing Binary Circuit Models

We show that no existing continuous-time, binary value-domain model for digital circuits is able to correctly capture glitch propagation. Prominent examples of such models are based on pure delay channels (P), inertial delay channels (I), or the elaborate PID channels proposed by Bellido-Díaz et al. We accomplish our goal by considering the solvability/non-solvability border of a simple problem called Short-Pulse Filtration (SPF), which is closely related to arbitration and synchronization. On one hand, we prove that SPF is solvable in bounded time in any such model that provides channels with non-constant delay, like I and PID. This is in opposition to the impossibility of solving bounded SPF in real (physical) circuit models. On the other hand, for binary circuit models with constant-delay channels, we prove that SPF cannot be solved even in unbounded time; again in opposition to physical circuit models. Consequently, indeed none of the binary value-domain models proposed so far (and that we are aware of) faithfully captures glitch propagation of real circuits. We finally show that these modeling mismatches do not hold for the weaker eventual SPF problem.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

FATAL+: A Self-Stabilizing Byzantine Fault-tolerant Clocking Scheme for SoCs

We present concept and implementation of a self-stabilizing Byzantine fault-tolerant distributed clock generation scheme for multi-synchronous GALS architectures in critical applications. It combines a variant of a recently introduced self-stabilizing algorithm for generating low-frequency, low-accuracy synchronized pulses with a simple non-stabilizing high-frequency, high-accuracy clock synchronization algorithm. We provide thorough correctness proofs and a performance analysis, which use methods from fault-tolerant distributed computing research but also addresses hardware-related issues like metastability. The algorithm, which consists of several concurrent communicating asynchronous state machines, has been implemented in VHDL using Petrify in conjunction with some extensions, and synthetisized for an Altera Cyclone FPGA. An experimental validation of this prototype has been carried out to confirm the skew and clock frequency bounds predicted by the theoretical analysis, as well as the very short stabilization times (required for recovering after excessively many transient failures) achievable in practice.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms

Fault-tolerant distributed algorithms are central for building reliable spatially distributed systems. Unfortunately, the lack of a canonical precise framework for fault-tolerant algorithms is an obstacle for both verification and deployment. In this paper, we introduce a new domain-specific framework to capture the behavior of fault-tolerant distributed algorithms in an adequate and precise way. At the center of our framework is a parameterized system model where control flow automata are used for process specification. To account for the specific features and properties of fault-tolerant distributed algorithms for message-passing systems, our control flow automata are extended to model threshold guards as well as the inherent non-determinism stemming from asynchronous communication, interleavings of steps, and faulty processes. We demonstrate the adequacy of our framework in a representative case study where we formalize a family of well-known fault-tolerant broadcasting algorithms under a variety of failure assumptions. Our case study is supported by model checking experiments with safety and liveness specifications for a fixed number of processes. In the experiments, we systematically varied the assumptions on both the resilience condition and the failure model. In all cases, our experiments coincided with the theoretical results predicted in the distributed algorithms literature. This is giving clear evidence for the adequacy of our model. In a companion paper, we are addressing the new model checking techniques necessary for parametric verification of the distributed algorithms captured in our framework.

0 citations0 reviewsNo code linkedOpen access