This paper introduces Claycode, a novel 2D scannable code designed for extensive stylization and deformation. Unlike traditional matrix-based codes (e.g. , QR codes), Claycodes encode their message in a tree structure. During the encoding process, bits are mapped into a topology tree, which is then depicted as a nesting of color regions drawn within the boundaries of a target polygon shape. When decoding, Claycodes are extracted and interpreted in real-time from a camera stream. We detail the end-to-end pipeline and show that Claycodes allow for extensive stylization without compromising their functionality. We then empirically demonstrate Claycode's high tolerance to heavy deformations, outperforming traditional 2D scannable codes in scenarios where they typically fail.

A recent survey of industry practices by Akesson et al. [1] indicates that the use of response-time analysis (RTA) is surprisingly limited. In particular, in response to Question 23 of Akesson et al.’s survey, the majority of respondents (61%) indicated that the presence of potential deadline violations is assessed by running tests and checking for overruns. In contrast, the use of in-house schedulability analyses or commercially-available schedulability tools is far less widespread (31% and 9%, respectively).

Response-time analysis (RTA) is a key technique for the analysis of (not only) safety-critical real-time systems. It is hence crucial for published RTAs to be safe (i.e., correct), but historically this has not always been the case. To ensure the trustworthiness of RTAs, recent work has pioneered the use of formal verification. The Prosa open-source project, in particular, relies on the Coq proof assistant to mechanically check all proofs. While highly effective at eradicating human error, such formalization and automatic validation of mathematical reasoning still faces barriers to more widespread adoption as most researchers active today are not yet accustomed to the use of proof assistants. To make this approach more broadly accessible, this paper presents a case study in the verification of a novel RTA for sporadic tasks under FIFO scheduling using the Coq proof assistant. The RTA is derived twice, first using traditional, intuition-based reasoning, and once more formally in a style that highlights the similarity to the intuitive argument. The verified RTA is of interest in itself: experiments with synthetic workloads based on an automotive benchmark show the new RTA to clearly outperform a prior RTA for FIFO scheduling. The paper further explores the performance of FIFO scheduling relative to traditional fixed-priority and earliest-deadline-first approaches, showing that FIFO scheduling can benefit lower-rate tasks.

The purpose of a response-time analysis (RTA) is to obtain safe bounds on the worst-case response times of all critical tasks in a real-time system. To this end, the system is described with a mathematical model (typically, comprising a workload model, a resource model, and a scheduling policy), which is then analyzed to derive response-time bounds. This procedure requires (i) a theory that rigorously justifies that the RTA correctly characterizes the worst-case scenario, and (ii) an RTA tool that executes the concrete calculations.