ros-rvft · rdinizcal · Mar 14, 2026 · Mar 14, 2026 · Mar 14, 2026 · Mar 14, 2026
diff --git a/guidelines/guideline-mta2.html b/guidelines/guideline-mta2.html
@@ -259,9 +259,16 @@ <h4 style="text-indent: 25px;">Test case selection</h4>
         </p>
 
 
+        <h4 style="text-indent: 25px;">Automated monitor generation: the FRET + Ogma + Copilot pipeline</h4>
+
+        <p>
+          A key automation opportunity is the generation of runtime monitors directly from requirements. The FRET + Ogma + Copilot pipeline [9, 10, 11] provides an end-to-end workflow: the QA team writes safety requirements in FRETISH (see <a href="https://ros-rvft.github.io/guidelines/guideline-sdb1">SDB1</a>), which FRET translates to temporal logic; Ogma (<a href="https://github.com/nasa/ogma">https://github.com/nasa/ogma</a>) reads the exported specifications and generates monitor code in Copilot, a stream-based runtime verification language; the Copilot compiler (<a href="https://github.com/Copilot-Language/copilot">https://github.com/Copilot-Language/copilot</a>) produces constant-time, constant-memory C99 monitors; and Ogma wraps these into a self-contained ROS 2 monitoring node that subscribes to relevant topics, re-evaluates monitors when new data arrives, and publishes requirement violations [9]. The generated package integrates into larger ROS 2 systems as a black box. This pipeline is part of the Space ROS ecosystem [12].
+        </p>
+
+
         <p class="strengths" style="text-indent: 25px;">Strengths:</p>
-        <p> 
-          Automation in testing activities can be executed repeatedly with low effort and cost. Moreover, it brings benefits in terms of efficiency, effectiveness, and reliability. 
+        <p>
+          Automation in testing activities can be executed repeatedly with low effort and cost. Moreover, it brings benefits in terms of efficiency, effectiveness, and reliability.
         </p>
 
 
@@ -282,7 +289,11 @@ <h4 style="text-indent: 25px;">Test case selection</h4>
                   <p>[6] A. Santos, A. Cunha et al., “Property-based testing for the robot operating system,” in Proceedings of the 9th ACM SIGSOFT International Workshop on Automating TEST Case Design, Selection, and Evaluation, 2018, pp. 56–62. </p>
                   <p>[7] A. Ortega, N. Hochgeschwender et al., “Testing service robots in the field: An experience report,” in 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE, 2022, pp. 165–172.    </p>
                   <p>[8] C. Hildebrandt, S. Elbaum et al., “Feasible and stressful trajectory generation for mobile robots,” in Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2020, pp. 349–362. 4</p>
-
+                  <p>[9] I. Perez, A. Mavridou, T. Pressburger, A. Will, and P. J. Martin, “Monitoring ROS2: from Requirements to Autonomous Robots,” in Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 371, pp. 200–215, 2022. </p>
+                  <p>[10] I. Perez, A. Mavridou, T. Pressburger, A. Goodloe, and D. Giannakopoulou, “Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 13244, Springer, 2022, pp. 379–395. </p>
+                  <p>[11] I. Perez and A. Goodloe, “Copilot 3,” NASA Technical Memorandum TM-2020-220587, 2020. </p>
+                  <p>[12] Space ROS Documentation, “Ogma - Runtime Monitor Generation,” https://space-ros.github.io/docs/rolling/Related-Projects/Ogma.html, accessed March 2026. </p>
+
           </blockquote> 
 
 

diff --git a/guidelines/guideline-sdb1.html b/guidelines/guideline-sdb1.html
@@ -264,8 +264,15 @@ <h4 style="text-indent: 25px;">Patterns-based specification</h4>
 
 
 
+        <h4 style="text-indent: 25px;">Structured Natural Language with FRET</h4>
+
+        <p>
+          An alternative approach to specifying properties in logic is to use structured natural language that automatically translates to temporal logic. NASA's Formal Requirements Elicitation Tool (FRET) [14, 15] allows the QA team to write requirements in FRETISH, a restricted English language with precise, unambiguous semantics. For each requirement, FRET automatically generates formalizations in both future-time and past-time metric temporal logic. FRETISH requirements follow a structured template; for example, a safety requirement can be expressed as: "When in_mission, the UAV shall always satisfy (current_consumption &lt; max_current)". FRET translates such requirements into temporal logic formulae that can be exported for use in analysis and monitor generation tools (see <a href="https://ros-rvft.github.io/guidelines/guideline-mta2">MTA2</a> for the automated monitor generation pipeline). FRET v3.0 further supports probabilistic requirement specification and automated test case generation [16]. FRET has been applied to robotics domains with a dedicated focus on ROS 2 applications [17] and is open-source at <a href="https://github.com/NASA-SW-VnV/fret">https://github.com/NASA-SW-VnV/fret</a>.
+        </p>
+
+
         <p class="strengths" style="text-indent: 25px;">Strengths:</p>
-        <p> 
+        <p>
           Using logic-based languages to specifying properties offers a standardized approach to validation in compliance with well-adopted specification pattern.
         </p>
 
@@ -290,7 +297,11 @@ <h4 style="text-indent: 25px;">Patterns-based specification</h4>
         <p>[11] R. Halder, J. Proen¸ca et al., “Formal verification of ros-based robotic applications using timed-automata,” in 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE). IEEE, 2017, pp. 44–50. </p>
         <p>[12] C. Menghi, C. Tsigkanos et al., “Specification patterns for robotic missions,” IEEE Transactions on Software Engineering, vol. 47, no. 10, pp. 2208–2224, oct 2021. </p>
         <p>[13] ——, “Mission specification patterns for mobile robots: Providing support for quantitative properties,” IEEE Trans. Softw. Eng., vol. 49, no. 4, p. 2741–2760, dec 2022. </p>
-
+        <p>[14] D. Giannakopoulou, T. Pressburger, A. Mavridou, J. Rhein, J. Schumann, and N. Shi, “Formal Requirements Elicitation with FRET,” in Joint Proceedings of REFSQ-2020 Workshops, CEUR Workshop Proceedings, vol. 2584, 2020. </p>
+        <p>[15] D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann, “Automated formalization of structured natural language requirements,” Information and Software Technology, vol. 137, p. 106590, 2021. </p>
+        <p>[16] A. Katis, A. Mavridou, D. Giannakopoulou, T. Pressburger, and J. Schumann, “Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET,” in Computer Aided Verification (CAV), LNCS, vol. 13372, Springer, 2022, pp. 484–495. </p>
+        <p>[17] G. Vazquez, A. Mavridou, M. Farrell, T. Pressburger, and R. Calinescu, “Robotics: A New Mission for FRET Requirements,” in NASA Formal Methods (NFM), 2024. </p>
+
       </blockquote>
 
 

diff --git a/index.html b/index.html
@@ -149,9 +149,9 @@ <h1 class="post-title" itemprop="name">Guidelines for Developers and QA Teams</h
             <div style="border: 1px solid #ddd; border-radius: 6px; padding: 20px 24px; margin: 24px 0; background-color: #f9f9f9;">
               <h2 id="whats-new" style="margin-top: 0;">What's New</h2>
               <ul style="list-style: none; padding-left: 0;">
-                <li style="margin-bottom: 10px;"><strong>March 2026</strong> — New contribution templates: you can now suggest tools, report gaps, or request updates directly via <a href="https://github.com/ros-rvft/ros-rvft.github.io/issues/new/choose">GitHub Issues</a> — no Git required.</li>
+                <li style="margin-bottom: 10px;"><strong>March 2026</strong> — New exemplars added: FRET for structured natural language specification (<a href="guidelines/guideline-sdb1">SDB1</a>) and the FRET+Ogma+Copilot automated monitor generation pipeline (<a href="guidelines/guideline-mta2">MTA2</a>).</li>
                 <li style="margin-bottom: 10px;"><strong>March 2026</strong> — Website refresh: updated contact info, copyright, and contribution guidelines.</li>
-                <li style="margin-bottom: 10px;"><strong>July 2024</strong> — Initial release of the guideline catalog accompanying the TSE paper.</li>
+                <li style="margin-bottom: 10px;"><strong>March 2026</strong> — New guideline tools coming soon: FRET + Copilot monitor generation pipeline, updated ROSMonitoring references, and more. <a href="https://github.com/ros-rvft/ros-rvft.github.io/issues">Follow progress on GitHub Issues</a>.</li>
               </ul>
             </div>