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