Sacrificing a little space can significantly improve monitoring of time-sensitive cyber-physical systems
Bibliographic record
Abstract
The goal of runtime verification is to inspect the correctness of a system by incorporating a monitor during its execution. Predictability of time distribution of monitor invocations and memory usage are two indicators of the quality of a monitoring solution, specially in cyber-physical systems, where the physical environment is a part of the system dynamics. In our previous work, we proposed a control-theoretic approach for coordinating time predictability and memory utilization in runtime verification of time-sensitive systems. To this end, we designed controllers that attempt to improve time predictability, while ensuring the soundness of verification by incorporating a maximally utilized bounded memory buffer that accumulates events. Since the frequency of occurrence of environment actions in cyber-physical systems is not known a priori, the system may run into situations, where the buffer is full, but a monitor invocation has not yet been scheduled. In control theory, this is called the overshooting phenomenon, which inherently decreases time predictability. In this paper, we address the issue of overshoots, by employing a second controller that allows limited memory reservations to temporarily extend the size of the event buffer when the system is subject to bursts of environment actions. We apply our solution to the verification of the air/fuel ratio in a car engine exhaust. The acceptable ratio varies depending on the driving circumstances, and monitoring that ratio is important to control emissions in a vehicle. A highly predictable monitor imposes uniform load on the engine control unit (ECU), thus, not negatively or sporadically affecting its control tasks. The experimental results exhibit two significant contributions: we (1) demonstrate the advantages of applying our approach to achieve low variation in the frequency of monitor invocations for verication, while maintaining maximum memory utilization, and (2) clearly illustrate that by negligible temporary increases in the size of the event buffer, the number of overshoots decreases significantly, which in turn substantially increases time predictability of runtime verication.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.000 | 0.000 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.000 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.000 | 0.000 |
| Open science | 0.000 | 0.000 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one teacher head, not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".