From 8c70ff7dbf5648a5dfb6d609ab8c37b179cafb86 Mon Sep 17 00:00:00 2001 From: Split Date: Tue, 17 Mar 2026 17:44:51 -0400 Subject: [PATCH] Fix Pressburger citation: soften claim to match source (describes manual integration, not 'significant source of errors') --- 3-research-approach/approach.tex | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index 6718d78..4d3c7fe 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -672,12 +672,13 @@ deployment requirements. \addedprose{A critical integration concern is maintaining formal guarantees through the implementation pipeline. Pressburger et -al.~\cite{pressburger_using_2023} identify manual translation from formal -specifications to executable code as a significant source of -implementation errors. To mitigate this risk, the ARCADE interface will -support automated code generation from the synthesized automaton, ensuring -that the controller deployed on Ovation hardware preserves the verified -behavior without manual re-implementation of control logic.} +al.~\cite{pressburger_using_2023} describe manual integration of +formally specified monitors into executable systems, noting +opportunities for automation to reduce this gap. To mitigate this risk, +the ARCADE interface will support automated code generation from the +synthesized automaton, ensuring that the controller deployed on Ovation +hardware preserves the verified behavior without manual re-implementation +of control logic.} %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration